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

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

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

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

divides_to_congruent : 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) => (nat_sttfa_th.le(m)(n) => (primes_sttfa_th.sttfa_divides(p)(nat_sttfa_th.minus(n)(m)) => cong_sttfa.congruent(n)(m)(p)))))))

Printing for OpenTheory is not working at the moment.