∀ n, n | n

Theorem divides_n_n : forall (n:nat.nat), divides n n.

theorem divides_n_n : \forall (n:nat). (divides) n n.

theorem divides_n_n : forall (n:nat.nat) , (((primes.divides) ) (n)) (n).

divides_n_n : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):primes_sttfa.sttfa_divides(n)(n))

Printing for OpenTheory is not working at the moment.