Idris2Doc : Data.Nat.Properties

Data.Nat.Properties

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