∀ p, prime p ⇒ ∀ n, n < p ⇒ ¬(p | (!n))

Theorem prime_to_not_divides_fact : forall (p:nat.nat), (primes.prime p) -> forall (n:nat.nat), (nat.lt n p) -> connectives.Not (primes.divides p (fact.fact n)).

theorem prime_to_not_divides_fact : \forall (p:nat). ((prime) p) -> \forall (n:nat). ((lt) n p) -> (Not) ((divides) p ((fact) n)).

theorem prime_to_not_divides_fact : forall (p:nat.nat) , (((primes.prime) ) (p)) -> forall (n:nat.nat) , ((((nat.lt_) ) (n)) (p)) -> ((connectives.Not) ) ((((primes.divides) ) (p)) (((fact.fact) ) (n))).

prime_to_not_divides_fact : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):(primes_sttfa_th.prime(p) => (FORALL(n:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(n)(p) => connectives_sttfa_th.sttfa_Not(primes_sttfa_th.sttfa_divides(p)(fact_sttfa_th.sttfa_fact(n)))))))

Printing for OpenTheory is not working at the moment.