Idris2Doc : Data.Nat.Order

Data.Nat.Order

LTEIsAntisymmetric : (m : Nat) -> (n : Nat) -> LTEmn -> LTEnm -> m = n
Totality: total
LTEIsReflexive : (n : Nat) -> LTEnn
Totality: total
LTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) -> LTEmn -> LTEno -> LTEmo
Totality: total
decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTEnm)
Totality: total
lte : (m : Nat) -> (n : Nat) -> Dec (LTEmn)
Totality: total
ltesuccinjective : (LTEnm -> Void) -> LTE (Sn) (Sm) -> Void
Totality: total
shift : (m : Nat) -> (n : Nat) -> LTEmn -> LTE (Sm) (Sn)
Totality: total
zeroAlwaysSmaller : LTEZn
Totality: total
zeroNeverGreater : LTE (Sn) Z -> Void
Totality: total