proposition: Lemma ggcdn_gcdn : forall n a b, fst (ggcdn n a b) = gcdn n a b.
proof: Proof. intro n; induction n as [|n IHn]. - simpl; auto. - intros a b; destruct a, b; simpl; auto; try case compare_spec; simpl; trivial; rewrite <- IHn; destruct ggcdn as (g,(u,v)); simpl; auto. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef