Idris2Doc
: Data.Nat.Properties
Index
Default
Alternative
Black & White
Data.Nat.Properties
Additional properties/lemmata of Nats
multRightCancel
: (a :
Nat
) -> (b :
Nat
) -> (r :
Nat
) -> (0 _ :
NonZero
r) -> a
*
r = b
*
r -> a = b
Totality
: total
unfoldDouble
:
2
*
n = n
+
n
Totality
: total
unfoldDoubleS
:
2
*
S
n =
2
+
(
2
*
n)
Totality
: total