Theorem Nat.le_nth_of_lt_nth_succ

Modification history