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