:: deftheorem defines addnat MONOID_0:def 29 :
addnat = the multF of <NAT,+>;