less_equal_pow_log: (all n:Nat. n ≤ pow2(log(n)))

auto lit_expt_suc

lit_expt_suc: (all n:Nat, m:Nat. n ^ lit(suc(m)) = n * n ^ lit(m))

auto lit_expt_zero

lit_expt_zero: (all n:Nat. n ^ ℕ0 = ℕ1)

pow_add_r: (all n:Nat, m:Nat, o:Nat. m ^ (n + o) = m ^ n * m ^ o)

pow_le_mono_l: (all c:Nat, a:Nat, b:Nat. (if a ≤ b then a ^ c ≤ b ^ c))

pow_log2_greater: (all n:Nat. n < ℕ2 * ℕ2 ^ log2(n))

pow_log2_less_equal: (all n:Nat. (if ℕ0 < n then ℕ2 ^ log2(n) ≤ n))

pow_mul_l: (all o:Nat, m:Nat, n:Nat. (m * n) ^ o = m ^ o * n ^ o)

pow_mul_r: (all o:Nat, m:Nat, n:Nat. (m ^ n) ^ o = m ^ (n * o))