Idris2Doc : Data.Nat.Order.Properties

Data.Nat.Order.Properties

Additional properties/lemmata of Nats involving order
GTIsnotlte : (a : Nat) -> (b : Nat) -> LT b a -> lte a b = False
Totality: total
LTESuccInjectiveMonotone : (m : Nat) -> (n : Nat) -> Reflects (LTE m n) b -> Reflects (LTE (S m) (S n)) b
Totality: total
LteIslte : (a : Nat) -> (b : Nat) -> LTE a b -> lte a b = True
Totality: total
ltIsLT : (a : Nat) -> (b : Nat) -> lt a b = True -> LT a b
Totality: total
ltReflection : (a : Nat) -> (b : Nat) -> Reflects (LT a b) (lt a b)
Totality: total
lteIsLTE : (a : Nat) -> (b : Nat) -> lte a b = True -> LTE a b
Totality: total
lteReflection : (a : Nat) -> (b : Nat) -> Reflects (LTE a b) (lte a b)
Totality: total
minusLTE : (a : Nat) -> (b : Nat) -> LTE (minus b a) b
  Subtracting a number gives a smaller number

Totality: total
minusPosLT : (a : Nat) -> (b : Nat) -> LT 0 a -> LTE a b -> LT (minus b a) b
  Subtracting a positive number gives a strictly smaller number

Totality: total
multLteMonotoneLeft : (a : Nat) -> (b : Nat) -> (r : Nat) -> LTE a b -> LTE (a * r) (b * r)
Totality: total
multLteMonotoneRight : (l : Nat) -> (a : Nat) -> (b : Nat) -> LTE a b -> LTE (l * a) (l * b)
Totality: total
notLteIsnotlte : (a : Nat) -> (b : Nat) -> Not (LTE a b) -> lte a b = False
Totality: total
notltIsGTE : (a : Nat) -> (b : Nat) -> lt a b = False -> GTE a b
Totality: total
notltIsNotLT : (a : Nat) -> (b : Nat) -> lt a b = False -> Not (LT a b)
Totality: total
notlteIsLT : (a : Nat) -> (b : Nat) -> lte a b = False -> LT b a
Totality: total
notlteIsNotLTE : (a : Nat) -> (b : Nat) -> lte a b = False -> Not (LTE a b)
Totality: total