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 : LTEaZ -> a = Z
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