proposition: Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b.
proof: Proof. destruct a as [|p], b as [|q]; simpl; auto. assert (H := Pos.ggcd_gcd p q). destruct Pos.ggcd as (g,(aa,bb)); simpl; now f_equal. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties