proposition: Lemma Zgcd_duv_divisor : forall a b : Z, a <> 0%Z -> Zdivides b a -> Zgcd_duv a b = (Z.abs b, (0%Z, Z.sgn b)).
proof: Proof. intros a b Ha. case b. intros Hdiv. replace a with 0%Z; simpl in |- *; auto. symmetry in |- *. auto with zarith. intros pb Hdiv. simpl in |- *. rewrite Zgcd_duv_rec_subcase. replace (Z.abs a mod Zpos pb)%Z with 0%Z. rewrite Zgcd_duv_zero_rht. rewrite Zmult_0_r. rewrite Zmult_0_r. simpl in |- *. reflexivity. symmetry in |- *. auto with zarith. intros pb Hdiv. simpl in |- *. fold (- Zpos pb)%Z in |- *. rewrite Zgcd_duv_Zopp_r. rewrite Zgcd_duv_rec_subcase. replace (Z.abs a mod Zpos pb)%Z with 0%Z. rewrite Zgcd_duv_zero_rht. rewrite Zmult_0_r. rewrite Zmult_0_r. simpl in |- *. reflexivity. symmetry in |- *. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)