∀ n m n1 m1 p, O < p ⇒ n ≡ n1 [p] ⇒ m ≡ m1 [p] ⇒ (n × m) ≡ (n1 × m1) [p]

Theorem congruent_times : forall (n:nat.nat), forall (m:nat.nat), forall (n1:nat.nat), forall (m1:nat.nat), forall (p:nat.nat), (nat.lt nat.O p) -> (congruent n n1 p) -> (congruent m m1 p) -> congruent (nat.times n m) (nat.times n1 m1) p.

theorem congruent_times : \forall (n:nat). \forall (m:nat). \forall (n1:nat). \forall (m1:nat). \forall (p:nat). ((lt) (O) p) -> ((congruent) n n1 p) -> ((congruent) m m1 p) -> (congruent) ((times) n m) ((times) n1 m1) p.

theorem congruent_times : forall (n:nat.nat) , forall (m:nat.nat) , forall (n1:nat.nat) , forall (m1:nat.nat) , forall (p:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (p)) -> (((((cong.congruent) ) (n)) (n1)) (p)) -> (((((cong.congruent) ) (m)) (m1)) (p)) -> ((((cong.congruent) ) ((((nat.times) ) (n)) (m))) ((((nat.times) ) (n1)) (m1))) (p).

congruent_times : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(n1:nat_sttfa_th.sttfa_nat):(FORALL(m1:nat_sttfa_th.sttfa_nat):(FORALL(p:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(p) => (cong_sttfa.congruent(n)(n1)(p) => (cong_sttfa.congruent(m)(m1)(p) => cong_sttfa.congruent(nat_sttfa_th.times(n)(m))(nat_sttfa_th.times(n1)(m1))(p)))))))))

Printing for OpenTheory is not working at the moment.