Theorem Nat.sub_self_add

Modification history