proposition: Lemma pp_gcd_lin_comb : forall x : pp, let (a, b) := x in Zpos (p_gcd a b) = (p_gcd_coeff_a a b * Zpos a + p_gcd_coeff_b a b * Zpos b)%Z.
proof: Proof. apply (well_founded_ind pp_lt_wf (fun x : pp => let (a, b) := x in Zpos (p_gcd a b) = (p_gcd_coeff_a a b * Zpos a + p_gcd_coeff_b a b * Zpos b)%Z)). intros x; elim x; intros a b. unfold p_gcd, p_gcd_coeff_a, p_gcd_coeff_b in |- *. intros Hind. case (rem_dec a b). intros Hr. rewrite (p_gcd_duv_rec_zero a b Hr). auto with zarith. intros Hr. elim Hr; clear Hr; intros r Hr. generalize (Hind (b, r) (rem_lt a b r Hr)). rewrite (p_gcd_duv_rec a b r Hr). elim (p_gcd_duv b r); intros d' uv'; elim uv'; intros u' v'. intro Hd'; rewrite Hd'. set (q := (Zpos a / Zpos b)%Z) in *. rewrite (Z_div_mod_eq_full (Zpos a) (Zpos b)). fold q in |- *. rewrite Hr. rewrite Zmult_plus_distr_r. rewrite BinInt.Zmult_minus_distr_r. rewrite (Zmult_assoc v' (Zpos b) q). rewrite (Zmult_comm (v' * Zpos b) q). rewrite (Zmult_assoc q v' (Zpos b)). lia. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)