∀ n m p q, n < m ⇒ p < q ⇒ (n × p) < (m × q)

Theorem lt_times : forall (n:nat), forall (m:nat), forall (p:nat), forall (q:nat), (lt n m) -> (lt p q) -> lt (times n p) (times m q).

theorem lt_times : \forall (n:nat). \forall (m:nat). \forall (p:nat). \forall (q:nat). ((lt) n m) -> ((lt) p q) -> (lt) ((times) n p) ((times) m q).

theorem lt_times : forall (n:nat.nat) , forall (m:nat.nat) , forall (p:nat.nat) , forall (q:nat.nat) , ((((nat.lt_) ) (n)) (m)) -> ((((nat.lt_) ) (p)) (q)) -> (((nat.lt_) ) ((((nat.times) ) (n)) (p))) ((((nat.times) ) (m)) (q)).

lt_times : LEMMA (FORALL(n:nat_sttfa.sttfa_nat):(FORALL(m:nat_sttfa.sttfa_nat):(FORALL(p:nat_sttfa.sttfa_nat):(FORALL(q:nat_sttfa.sttfa_nat):(nat_sttfa.lt(n)(m) => (nat_sttfa.lt(p)(q) => nat_sttfa.lt(nat_sttfa.times(n)(p))(nat_sttfa.times(m)(q))))))))

Printing for OpenTheory is not working at the moment.