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