Idris2Doc : Data.Nat.Equational

# Data.Nat.Equational

## Definitions

`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
Visibility: export
`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
Visibility: export
`plusLteLeft : (a : Nat) -> LTE b c -> LTE (a + b) (a + c)`
`  Add a number to both sides of an inequality`

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

Totality: total
Visibility: export
`lteZeroIsZero : LTE a 0 -> a = 0`
`  Only 0 is lte 0  Useful when the argument is an open term`

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

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

Totality: total
Visibility: export
`rightFactorLteProduct : (a : Nat) -> (b : Nat) -> LTE b (S a * 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
Visibility: export
`leftFactorLteProduct : (a : Nat) -> (b : Nat) -> LTE a (a * S 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
Visibility: export