∀ n, n | O

Theorem divides_n_O : forall (n:nat.nat), divides n nat.O.

theorem divides_n_O : \forall (n:nat). (divides) n (O) .

theorem divides_n_O : forall (n:nat.nat) , (((primes.divides) ) (n)) ((nat.O) ).

divides_n_O : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):primes_sttfa.sttfa_divides(n)(nat_sttfa_th.sttfa_O))

Printing for OpenTheory is not working at the moment.