nat.lt_to_le_to_lt_times
∀ n m p q, n < m ⇒ p ≤ q ⇒ O < q ⇒ (n × p) < (m × q)
Theorem lt_to_le_to_lt_times : forall (n:nat), forall (m:nat), forall (p:nat), forall (q:nat), (lt n m) -> (le p q) -> (lt O q) -> lt (times n p) (times m q).
theorem lt_to_le_to_lt_times : \forall (n:nat). \forall (m:nat). \forall (p:nat). \forall (q:nat). ((lt) n m) -> ((le) p q) -> ((lt) (O) q) -> (lt) ((times) n p) ((times) m q).
theorem lt_to_le_to_lt_times : forall (n:nat.nat) , forall (m:nat.nat) , forall (p:nat.nat) , forall (q:nat.nat) , ((((nat.lt_) ) (n)) (m)) -> ((((nat.le_) ) (p)) (q)) -> ((((nat.lt_) ) ((nat.O) )) (q)) -> (((nat.lt_) ) ((((nat.times) ) (n)) (p))) ((((nat.times) ) (m)) (q)).
lt_to_le_to_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.le(p)(q) => (nat_sttfa.lt(nat_sttfa.sttfa_O)(q) => nat_sttfa.lt(nat_sttfa.times(n)(p))(nat_sttfa.times(m)(q)))))))))
Printing for OpenTheory is not working at the moment.