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

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

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

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

monotonic_le_minus_r : 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(n)(p))(nat_sttfa.minus(n)(q))))))

Printing for OpenTheory is not working at the moment.