proposition: Lemma gcd_divide_l : forall a b, (gcd a b | a).
proof: Proof. intros a b. rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b). destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa. now rewrite mul_comm. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef