Data.Nat.Order.Properties

Additional properties/lemmata of Nats involving order

Definitions

LTESuccInjectiveMonotone : (m : Nat) -> (n : Nat) -> Reflects (LTE m n) b -> Reflects (LTE (S m) (S n)) b

Totality: total
Visibility: export

lteReflection : (a : Nat) -> (b : Nat) -> Reflects (LTE a b) (lte a b)

Totality: total
Visibility: export

ltReflection : (a : Nat) -> (b : Nat) -> Reflects (LT a b) (lt a b)

Totality: total
Visibility: export

lteIsLTE : (a : Nat) -> (b : Nat) -> lte a b = True -> LTE a b

Totality: total
Visibility: export

ltIsLT : (a : Nat) -> (b : Nat) -> lt a b = True -> LT a b

Totality: total
Visibility: export

notlteIsNotLTE : (a : Nat) -> (b : Nat) -> lte a b = False -> Not (LTE a b)

Totality: total
Visibility: export

notltIsNotLT : (a : Nat) -> (b : Nat) -> lt a b = False -> Not (LT a b)

Totality: total
Visibility: export

notlteIsLT : (a : Nat) -> (b : Nat) -> lte a b = False -> LT b a

Totality: total
Visibility: export

notltIsGTE : (a : Nat) -> (b : Nat) -> lt a b = False -> GTE a b

Totality: total
Visibility: export

LteIslte : (a : Nat) -> (b : Nat) -> LTE a b -> lte a b = True

Totality: total
Visibility: export

notLteIsnotlte : (a : Nat) -> (b : Nat) -> Not (LTE a b) -> lte a b = False

Totality: total
Visibility: export

GTIsnotlte : (a : Nat) -> (b : Nat) -> LT b a -> lte a b = False

Totality: total
Visibility: export

minusLTE : (a : Nat) -> (b : Nat) -> LTE (minus b a) b

  Subtracting a number gives a smaller number

Totality: total
Visibility: export

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
Visibility: export

multLteMonotoneRight : (l : Nat) -> (a : Nat) -> (b : Nat) -> LTE a b -> LTE (l * a) (l * b)

Totality: total
Visibility: export

multLteMonotoneLeft : (a : Nat) -> (b : Nat) -> (r : Nat) -> LTE a b -> LTE (a * r) (b * r)

Totality: total
Visibility: export

lteNotLtEq : (a : Nat) -> (b : Nat) -> LTE a b -> Not (LT a b) -> a = b

Totality: total
Visibility: export

decomposeLte : (a : Nat) -> (b : Nat) -> LTE a b -> Either (LT a b) (a = b)

Totality: total
Visibility: export