Theorem Real.exists_natCast_add_one_lt_pow_of_one_lt

Modification history