proposition: Lemma gcd_greatest : forall a b p, (p|a) -> (p|b) -> (p|gcd a b).
proof: Proof. intros. apply gcdn_greatest; auto. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef