∀ x y, (x - y) ≤ x

Theorem minus_le : forall (x:nat), forall (y:nat), le (minus x y) x.

theorem minus_le : \forall (x:nat). \forall (y:nat). (le) ((minus) x y) x.

theorem minus_le : forall (x:nat.nat) , forall (y:nat.nat) , (((nat.le_) ) ((((nat.minus) ) (x)) (y))) (x).

minus_le : LEMMA (FORALL(x:nat_sttfa.sttfa_nat):(FORALL(y:nat_sttfa.sttfa_nat):nat_sttfa.le(nat_sttfa.minus(x)(y))(x)))

Printing for OpenTheory is not working at the moment.