I remember when I was trying to figure out how to do <= with naturals that I tried the inductive definition (x <= x, if x <= y then x <= y + 1) and found it really difficult to prove all the standard results about <= with it :-) Maybe I should revisit this?
I remember when I was trying to figure out how to do <= with naturals that I tried the inductive definition (x <= x, if x <= y then x <= y + 1) and found it really difficult to prove all the standard results about <= with it :-) Maybe I should revisit this?