proposition: Lemma Zgcd_duv_symm : forall a b : Z, Z.abs a <> Z.abs b -> Zgcd_duv a b = (Zgcd b a, (Zgcd_coeff_b b a, Zgcd_coeff_a b a)).
proof: Proof. intros a b. unfold Zgcd, Zgcd_coeff_a, Zgcd_coeff_b in |- *. cut (forall p q : positive, Zpos p <> Zpos q -> p <> q). case a; case b; simpl in |- *; intros; unfold p_gcd, p_gcd_coeff_a, p_gcd_coeff_b in |- *; try rewrite p_gcd_duv_symm; auto. intros p q Hneq; intro Hfalse. apply Hneq; rewrite Hfalse; auto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)