∀ n m, ((gcd n m) | m) ∧ ((gcd n m) | n)

Theorem divides_gcd_nm : forall (n:nat.nat), forall (m:nat.nat), connectives.And (primes.divides (gcd n m) m) (primes.divides (gcd n m) n).

theorem divides_gcd_nm : \forall (n:nat). \forall (m:nat). (And) ((divides) ((gcd) n m) m) ((divides) ((gcd) n m) n).

theorem divides_gcd_nm : forall (n:nat.nat) , forall (m:nat.nat) , (((connectives.And) ) ((((primes.divides) ) ((((gcd.gcd) ) (n)) (m))) (m))) ((((primes.divides) ) ((((gcd.gcd) ) (n)) (m))) (n)).

divides_gcd_nm : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.sttfa_And(primes_sttfa_th.sttfa_divides(gcd_sttfa.gcd(n)(m))(m))(primes_sttfa_th.sttfa_divides(gcd_sttfa.gcd(n)(m))(n))))

Printing for OpenTheory is not working at the moment.