Theorem rpow_one_add_le_one_add_mul_self

Modification history