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