Theorem Nat.rec_one

Modification history