proposition: Lemma ggcd_correct_divisors a b : let '(g,(aa,bb)) := ggcd a b in a=g*aa /\ b=g*bb.
proof: Proof. destruct a as [|p], b as [|q]; simpl; auto. - now rewrite Pos.mul_1_r. - now rewrite Pos.mul_1_r. - generalize (Pos.ggcd_correct_divisors p q). destruct Pos.ggcd as (g,(aa,bb)); simpl. destruct 1; split; now f_equal. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties