proposition: Lemma p_gcd_duv_symm : forall a b : positive, a <> b -> p_gcd_duv a b = (p_gcd b a, (p_gcd_coeff_b b a, p_gcd_coeff_a b a)).
proof: Proof. intros a b Hdiff. unfold p_gcd, p_gcd_coeff_a, p_gcd_coeff_b in |- *. set (rel := (Zpos a ?= Zpos b)%Z) in *. cut ((Zpos a ?= Zpos b)%Z = rel). case rel. intro Hegal. assert (Heq : Zpos a = Zpos b). apply Zle_antisymm. intro H; rewrite H in Hegal; discriminate. apply Z.le_ge; intro H; rewrite H in Hegal; discriminate. inversion Heq. tauto. intro Hlt. rewrite (p_gcd_duv_rec a b a). elim (p_gcd_duv b a); intros d uv; elim uv; intros u v. cut ((Zpos a / Zpos b)%Z = 0%Z). intros H0; rewrite H0. rewrite Zmult_0_l. unfold Zminus in |- *. simpl in |- *. rewrite Zplus_0_r. reflexivity. apply (Zdiv_lt_POS a b Hlt). apply (Zmod_lt_POS a b Hlt). intro Hgt. rewrite (p_gcd_duv_rec b a b). elim (p_gcd_duv a b); intros d uv; elim uv; intros u v. cut ((Zpos b / Zpos a)%Z = 0%Z). intros H0; rewrite H0. rewrite Zmult_0_l. unfold Zminus in |- *; simpl in |- *. rewrite Zplus_0_r. reflexivity. apply (Zdiv_lt_POS b a); apply Z.gt_lt; assumption. apply (Zmod_lt_POS b a); apply Z.gt_lt; assumption. auto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)