`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