Theorem Nat.succ_sub

Modification history