[ O ⇒ O
| S n' ⇒ minus n' m']].
+interpretation "natural minus" 'minus x y = (minus x y).
+
naxiom le_minus: ∀n,m,p. le n m → le (minus n p) m.
-naxiom lt_minus: ∀n,m,p. lt n m → lt (minus n p) m.
\ No newline at end of file
+naxiom lt_minus: ∀n,m,p. lt n m → lt (minus n p) m.