Data.Nat.Exponentiation

Definitions

pow : Nat -> Nat -> Nat

Totality: total
Visibility: public export

lpow : Nat -> Nat -> Nat

Totality: total
Visibility: public export

pow2 : Nat -> Nat

Totality: total
Visibility: public export

lpow2 : Nat -> Nat

Totality: total
Visibility: public export

modularCorrect : (v : Nat) -> pow v n = lpow v n

Totality: total
Visibility: export

pow2Correct : pow2 n = lpow2 n

Totality: total
Visibility: export

unfoldLpow2 : lpow2 (S n) = lpow2 n + lpow2 n

Totality: total
Visibility: export

unfoldPow2 : pow2 (S n) = pow2 n + pow2 n

Totality: total
Visibility: export

lteLpow2 : LTE 1 (lpow2 m)

Totality: total
Visibility: export

ltePow2 : LTE 1 (pow2 m)

Totality: total
Visibility: export

pow2Increasing : LT (pow2 m) (pow2 (S m))

Totality: total
Visibility: export