Theorem Fin.neg_one_pow_succAbove_add_predAbove

Modification history