∀ n m p r, O < p ⇒ n = ((r × p) + m) ⇒ n ≡ m [p]

Theorem eq_times_plus_to_congruent : forall (n:nat.nat), forall (m:nat.nat), forall (p:nat.nat), forall (r:nat.nat), (nat.lt nat.O p) -> (logic.eq (nat.nat) n (nat.plus (nat.times r p) m)) -> congruent n m p.

theorem eq_times_plus_to_congruent : \forall (n:nat). \forall (m:nat). \forall (p:nat). \forall (r:nat). ((lt) (O) p) -> ((eq) (nat) n ((plus) ((times) r p) m)) -> (congruent) n m p.

theorem eq_times_plus_to_congruent : forall (n:nat.nat) , forall (m:nat.nat) , forall (p:nat.nat) , forall (r:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (p)) -> ((((logic.eq_) (nat.nat)) (n)) ((((nat.plus) ) ((((nat.times) ) (r)) (p))) (m))) -> ((((cong.congruent) ) (n)) (m)) (p).

eq_times_plus_to_congruent : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(p:nat_sttfa_th.sttfa_nat):(FORALL(r:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(p) => (logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](n)(nat_sttfa_th.plus(nat_sttfa_th.times(r)(p))(m)) => cong_sttfa.congruent(n)(m)(p)))))))

Printing for OpenTheory is not working at the moment.