Idris2Doc : Data.Nat.Properties

Data.Nat.Properties

multRightCancel : (a : Nat) -> (b : Nat) -> (r : Nat) -> (0 _ : NonZeror) -> a*r = b*r -> a = b
Totality: total
unfoldDouble : fromInteger 2 *n = n+n
Totality: total
unfoldDoubleS : fromInteger 2 *Sn = fromInteger 2 + (fromInteger 2 *n)
Totality: total