proposition: Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b.
proof: Proof. destruct a as [ |p|p], b as [ |q|q]; simpl; auto; generalize (Pos.ggcd_gcd p q); destruct Pos.ggcd as (g,(aa,bb)); simpl; congruence. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass