Data.Nat.Properties

Additional properties/lemmata of Nats

Definitions

unfoldDouble : 2 * n = n + n

Totality: total
Visibility: export

unfoldDoubleS : 2 * S n = 2 + (2 * n)

Totality: total
Visibility: export

multRightCancel : (a : Nat) -> (b : Nat) -> (r : Nat) -> (0 _ : NonZero r) -> a * r = b * r -> a = b

Totality: total
Visibility: export