proposition: Lemma ggcdn_correct_divisors : forall n a b, let '(g,(aa,bb)) := ggcdn n a b in a = g*aa /\ b = g*bb.
proof: Proof. intro n; induction n as [|n IHn]. - simpl; auto. - intros a b; destruct a, b; simpl; auto; try case compare_spec; try destr_pggcdn IHn. + intros ->. now rewrite mul_comm. + intros (H',H) LT; split; auto. rewrite mul_add_distr_l, mul_xO_r, <- H, <- H'. simpl. f_equal. symmetry. rewrite add_comm. now apply sub_add. + intros (H',H) LT; split; auto. rewrite mul_add_distr_l, mul_xO_r, <- H, <- H'. simpl. f_equal. symmetry. rewrite add_comm. now apply sub_add. + intros (H,H'); split; auto. rewrite mul_xO_r, H'; auto. + intros (H,H'); split; auto. rewrite mul_xO_r, H; auto. + intros (H,H'); split; subst; auto. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef