Idris2Doc : Data.Nat.Order.Properties

Data.Nat.Order.Properties

GTIsnotlte : (a : Nat) -> (b : Nat) -> LTba -> lteab = False
Totality: total
LTESuccInjectiveMonotone : (m : Nat) -> (n : Nat) -> Reflects (LTEmn) b -> Reflects (LTE (Sm) (Sn)) b
Totality: total
LteIslte : (a : Nat) -> (b : Nat) -> LTEab -> lteab = True
Totality: total
ltIsLT : (a : Nat) -> (b : Nat) -> ltab = True -> LTab
Totality: total
ltReflection : (a : Nat) -> (b : Nat) -> Reflects (LTab) (ltab)
Totality: total
lteIsLTE : (a : Nat) -> (b : Nat) -> lteab = True -> LTEab
Totality: total
lteReflection : (a : Nat) -> (b : Nat) -> Reflects (LTEab) (lteab)
Totality: total
minusLTE : (a : Nat) -> (b : Nat) -> LTE (minusba) b
Subtracting a number gives a smaller number
Totality: total
minusPosLT : (a : Nat) -> (b : Nat) -> LTZa -> LTEab -> LT (minusba) b
Subtracting a positive number gives a strictly smaller number
Totality: total
multLteMonotoneLeft : (a : Nat) -> (b : Nat) -> (r : Nat) -> LTEab -> LTE (a*r) (b*r)
Totality: total
multLteMonotoneRight : (l : Nat) -> (a : Nat) -> (b : Nat) -> LTEab -> LTE (l*a) (l*b)
Totality: total
notLteIsnotlte : (a : Nat) -> (b : Nat) -> Not (LTEab) -> lteab = False
Totality: total
notltIsGTE : (a : Nat) -> (b : Nat) -> ltab = False -> GTEab
Totality: total
notltIsNotLT : (a : Nat) -> (b : Nat) -> ltab = False -> Not (LTab)
Totality: total
notlteIsLT : (a : Nat) -> (b : Nat) -> lteab = False -> LTba
Totality: total
notlteIsNotLTE : (a : Nat) -> (b : Nat) -> lteab = False -> Not (LTEab)
Totality: total