Theorem Nat.add_one_pos

Modification history