proposition: Lemma ggcd_greatest : forall a b, let (aa,bb) := snd (ggcd a b) in forall p, (p|aa) -> (p|bb) -> p=1.
proof: Proof. intros a b **. generalize (gcd_greatest a b) (ggcd_correct_divisors a b). rewrite <- ggcd_gcd. destruct ggcd as (g,(aa,bb)); simpl. intros H (EQa,EQb) p Hp1 Hp2; subst. assert (H' : (g*p | g)). { apply H. - destruct Hp1 as (r,Hr). exists r. now rewrite mul_assoc, (mul_comm r g), <- mul_assoc, <- Hr. - destruct Hp2 as (r,Hr). exists r. now rewrite mul_assoc, (mul_comm r g), <- mul_assoc, <- Hr. } destruct H' as (q,H'). rewrite (mul_comm g p), mul_assoc in H'. apply mul_eq_1 with q; rewrite mul_comm. now apply mul_reg_r with g. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef