Li-Fan Chen says to YSITD HA ├ suc zero + suc zero = suc (zero + suc zero) 且 suc (zero + suc zero) = suc (suc zero)