// This prints the left floatting menu

### Theoremgcd.divides_to_gcd_aux

Statement

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

Main Dependencies

Statement

Theorem divides_to_gcd_aux : forall (p:nat.nat), forall (m:nat.nat), forall (n:nat.nat), (nat.lt nat.O p) -> (nat.lt nat.O n) -> (primes.divides n m) -> logic.eq (nat.nat) (gcd_aux p m n) n.

Statement

theorem divides_to_gcd_aux : \forall (p:nat). \forall (m:nat). \forall (n:nat). ((lt) (O) p) -> ((lt) (O) n) -> ((divides) n m) -> (eq) (nat) ((gcd_aux) p m n) n.

Statement

theorem divides_to_gcd_aux : forall (p:nat.nat) , forall (m:nat.nat) , forall (n:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (p)) -> ((((nat.lt_) ) ((nat.O) )) (n)) -> ((((primes.divides) ) (n)) (m)) -> (((logic.eq_) (nat.nat)) (((((gcd.gcd_aux) ) (p)) (m)) (n))) (n).

Statement

divides_to_gcd_aux : 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)(p) => (nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(n) => (primes_sttfa_th.sttfa_divides(n)(m) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](gcd_sttfa.gcd_aux(p)(m)(n))(n)))))))

Printing for OpenTheory is not working at the moment.