Idris2Doc : Data.Nat.Equational

Data.Nat.Equational

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

lteZeroIsZero : LTE a 0 -> a = 0

  Only 0 is lte 0
  Useful when the argument is an open term

Totality: total

plusLteLeft : (a : Nat) -> LTE b c -> LTE (a + b) (a + c)

  Add a number to both sides of an inequality

Totality: total

plusLteRight : (c : Nat) -> LTE a b -> LTE (a + c) (b + c)

  Add a number to both sides of an inequality

Totality: total

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

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) -> 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

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