proposition: Lemma Zgcd_div_gcd_1 : forall a b : Z, Zgcd a b <> 0%Z -> Zgcd (a / Zgcd a b) (b / Zgcd a b) = 1%Z.
proof: Proof. intros a b Hab. apply Zdivides_antisymm; auto with zarith. apply Z.lt_gt. apply Zgcd_pos. generalize (Zgcd_nonzero a b); intro Hnz; elim Hnz; auto. intro Ha; left; intro Hfalse; generalize (Zgcd_div_mult_lft a b); rewrite Hfalse; simpl in |- *; tauto. intro Hb; right; intro Hfalse; generalize (Zgcd_div_mult_rht a b); rewrite Hfalse; simpl in |- *; tauto. cut (1%Z = (Zgcd_coeff_a a b * (a / Zgcd a b) + Zgcd_coeff_b a b * (b / Zgcd a b))%Z). intro H1; rewrite H1. apply Zdivides_plus_elim. apply Zdivides_mult_elim_lft. apply Zgcd_is_divisor_lft. apply Zdivides_mult_elim_lft. apply Zgcd_is_divisor_rht. generalize (Zgcd_lin_comb a b); intro Hlincomb; generalize (Zgcd_is_divisor_lft a b); intro Hdivb; elim Hdivb; intros y Hy; generalize (Zgcd_is_divisor_rht a b); intro Hdiva; elim Hdiva; intros x Hx; set (d := Zgcd a b). move d after Hy. fold d in Hx; fold d in Hy. replace 1%Z with (Zgcd a b / d)%Z; auto with zarith. rewrite Hlincomb. set (u := Zgcd_coeff_a a b); set (v := Zgcd_coeff_b a b). rewrite Zdiv_plus_elim; auto with zarith. rewrite <- Hx; rewrite <- Hy. repeat rewrite Zmult_assoc. repeat rewrite Zdiv_mult_cancel_rht; auto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)