0 + 1 <= n by NAT_1:13;
hence n succ n in PrimRec by Th69; :: according to COMPUT_1:def 16 :: thesis: verum