∀ p q n, q ≤ p ⇒ (q - n) ≤ (p - n)

Theorem monotonic_le_minus_l : forall (p:nat), forall (q:nat), forall (n:nat), (le q p) -> le (minus q n) (minus p n).

theorem monotonic_le_minus_l : \forall (p:nat). \forall (q:nat). \forall (n:nat). ((le) q p) -> (le) ((minus) q n) ((minus) p n).

theorem monotonic_le_minus_l : forall (p:nat.nat) , forall (q:nat.nat) , forall (n:nat.nat) , ((((nat.le_) ) (q)) (p)) -> (((nat.le_) ) ((((nat.minus) ) (q)) (n))) ((((nat.minus) ) (p)) (n)).

monotonic_le_minus_l : LEMMA (FORALL(p:nat_sttfa.sttfa_nat):(FORALL(q:nat_sttfa.sttfa_nat):(FORALL(n:nat_sttfa.sttfa_nat):(nat_sttfa.le(q)(p) => nat_sttfa.le(nat_sttfa.minus(q)(n))(nat_sttfa.minus(p)(n))))))

Printing for OpenTheory is not working at the moment.