Idris2Doc : Data.Nat.Equational

Data.Nat.Equational

leftFactorLteProduct : (a : Nat) -> (b : Nat) -> LTEa (a*Sb)
  If one of the factors of a product is greater than 0, then the other factor
is less than or equal to the product..

Totality: total
lteZeroIsZero : LTEa0 -> a = 0
  Only 0 is lte 0
Useful when the argument is an open term

Totality: total
plusLteLeft : (a : Nat) -> LTEbc -> LTE (a+b) (a+c)
  Add a number to both sides of an inequality

Totality: total
plusLteRight : (c : Nat) -> LTEab -> LTE (a+c) (b+c)
  Add a number to both sides of an inequality

Totality: total
rightFactorLteProduct : (a : Nat) -> (b : Nat) -> LTEb (Sa*b)
  If one of the factors of a product is greater than 0, then the other factor
is less than or equal to the product..

Totality: total
subtractEqLeft : (a : Nat) -> a+b = a+c -> b = c
  Subtract a number from both sides of an equation.
Due to partial nature of subtraction in natural numbers, an equation of
special form is required in order for subtraction to be total.

Totality: total
subtractEqRight : (c : Nat) -> a+c = b+c -> a = b
  Subtract a number from both sides of an equation.
Due to partial nature of subtraction in natural numbers, an equation of
special form is required in order for subtraction to be total.

Totality: total
subtractLteLeft : (a : Nat) -> LTE (a+b) (a+c) -> LTEbc
  Subtract a number from both sides of an inequality.
Due to partial nature of subtraction, we require an inequality of special form.

Totality: total
subtractLteRight : (c : Nat) -> LTE (a+c) (b+c) -> LTEab
  Subtract a number from both sides of an inequality.
Due to partial nature of subtraction, we require an inequality of special form.

Totality: total