let a, b, m be Nat; :: thesis: ( a <= b implies Ackermann (m,a) <= Ackermann (m,b) )
assume a <= b ; :: thesis: Ackermann (m,a) <= Ackermann (m,b)
then ( a < b or a = b ) by XXREAL_0:1;
hence Ackermann (m,a) <= Ackermann (m,b) by Th18; :: thesis: verum