∀ n m p, O < p ⇒ n ≡ m [p] ⇒ p | (n - m)

Theorem congruent_to_divides : forall (n:nat.nat), forall (m:nat.nat), forall (p:nat.nat), (nat.lt nat.O p) -> (congruent n m p) -> primes.divides p (nat.minus n m).

theorem congruent_to_divides : \forall (n:nat). \forall (m:nat). \forall (p:nat). ((lt) (O) p) -> ((congruent) n m p) -> (divides) p ((minus) n m).

theorem congruent_to_divides : forall (n:nat.nat) , forall (m:nat.nat) , forall (p:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (p)) -> (((((cong.congruent) ) (n)) (m)) (p)) -> (((primes.divides) ) (p)) ((((nat.minus) ) (n)) (m)).

congruent_to_divides : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m: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)(m)(p) => primes_sttfa_th.sttfa_divides(p)(nat_sttfa_th.minus(n)(m)))))))

Printing for OpenTheory is not working at the moment.