Idris2Doc : Data.Nat.Order

Data.Nat.Order

Implementation of ordering relations for `Nat`ural numbers
decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTEnm)
Totality: total
lte : (m : Nat) -> (n : Nat) -> Dec (LTEmn)
Totality: total
ltesuccinjective : Not (LTEnm) -> Not (LTE (Sn) (Sm))
Totality: total
shift : (m : Nat) -> (n : Nat) -> LTEmn -> LTE (Sm) (Sn)
Totality: total
zeroAlwaysSmaller : LTE0n
Totality: total
zeroNeverGreater : Not (LTE (Sn) 0)
Totality: total