Commit 2021-02-10 17:50 83118da7
View on Github →feat(data/nat/basic): prove an inequality of natural numbers (#6155)
Add lemma mul_lt_mul_pow_succ, proving the inequality n * q < a * q ^ (n + 1).
Reference: Liouville PR #4301.
feat(data/nat/basic): prove an inequality of natural numbers (#6155)
Add lemma mul_lt_mul_pow_succ, proving the inequality n * q < a * q ^ (n + 1).
Reference: Liouville PR #4301.