∀ p m n, O < n ⇒ n ≤ m ⇒ n ≤ p ⇒ ((gcd_aux p m n) | m) ∧ ((gcd_aux p m n) | n)

Theorem divides_gcd_aux_mn : forall (p:nat.nat), forall (m:nat.nat), forall (n:nat.nat), (nat.lt nat.O n) -> (nat.le n m) -> (nat.le n p) -> connectives.And (primes.divides (gcd_aux p m n) m) (primes.divides (gcd_aux p m n) n).

theorem divides_gcd_aux_mn : \forall (p:nat). \forall (m:nat). \forall (n:nat). ((lt) (O) n) -> ((le) n m) -> ((le) n p) -> (And) ((divides) ((gcd_aux) p m n) m) ((divides) ((gcd_aux) p m n) n).

theorem divides_gcd_aux_mn : forall (p:nat.nat) , forall (m:nat.nat) , forall (n:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (n)) -> ((((nat.le_) ) (n)) (m)) -> ((((nat.le_) ) (n)) (p)) -> (((connectives.And) ) ((((primes.divides) ) (((((gcd.gcd_aux) ) (p)) (m)) (n))) (m))) ((((primes.divides) ) (((((gcd.gcd_aux) ) (p)) (m)) (n))) (n)).

divides_gcd_aux_mn : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(n) => (nat_sttfa_th.le(n)(m) => (nat_sttfa_th.le(n)(p) => connectives_sttfa_th.sttfa_And(primes_sttfa_th.sttfa_divides(gcd_sttfa.gcd_aux(p)(m)(n))(m))(primes_sttfa_th.sttfa_divides(gcd_sttfa.gcd_aux(p)(m)(n))(n))))))))

Printing for OpenTheory is not working at the moment.