proposition: Lemma pp_gcd_is_divisor : forall ab : pp, let (a, b) := ab in Zdivides (Zpos (p_gcd a b)) (Zpos a) /\ Zdivides (Zpos (p_gcd a b)) (Zpos b).
proof: Proof. apply (well_founded_ind pp_lt_wf (fun y : pp => let (u, v) := y in Zdivides (Zpos (p_gcd u v)) (Zpos u) /\ Zdivides (Zpos (p_gcd u v)) (Zpos v))). intro 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'. split. rewrite (Z_div_mod_eq_full (Zpos a) (Zpos b)). rewrite Hr. apply Zdivides_plus_elim. apply Zdivides_mult_elim_rht. tauto. tauto. tauto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)