Theorem Nat.sub_one_dvd_pow_sub_one

Modification history