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|p], b as [ |q|q]; simpl; rewrite ?Pos.mul_1_r; auto; generalize (Pos.ggcd_correct_divisors p q); destruct Pos.ggcd as (g,(aa,bb)); simpl; destruct 1; now subst. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass