Theorem Nat.self_add_sub_one

Modification history