∀ p n m, prime p ⇒ p | (n × m) ⇒ (p | n) ∨ (p | m)

Theorem divides_times_to_divides : forall (p:nat.nat), forall (n:nat.nat), forall (m:nat.nat), (primes.prime p) -> (primes.divides p (nat.times n m)) -> connectives.Or (primes.divides p n) (primes.divides p m).

theorem divides_times_to_divides : \forall (p:nat). \forall (n:nat). \forall (m:nat). ((prime) p) -> ((divides) p ((times) n m)) -> (Or) ((divides) p n) ((divides) p m).

theorem divides_times_to_divides : forall (p:nat.nat) , forall (n:nat.nat) , forall (m:nat.nat) , (((primes.prime) ) (p)) -> ((((primes.divides) ) (p)) ((((nat.times) ) (n)) (m))) -> (((connectives.Or) ) ((((primes.divides) ) (p)) (n))) ((((primes.divides) ) (p)) (m)).

divides_times_to_divides : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(primes_sttfa_th.prime(p) => (primes_sttfa_th.sttfa_divides(p)(nat_sttfa_th.times(n)(m)) => connectives_sttfa_th.sttfa_Or(primes_sttfa_th.sttfa_divides(p)(n))(primes_sttfa_th.sttfa_divides(p)(m)))))))

Printing for OpenTheory is not working at the moment.