proposition: Lemma Zis_gcd_rel_prime : forall a b g:Z, b > 0 -> g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g).
proof: Proof. intros a b g; intros H H0 H1. assert (H2 : g <> 0) by (intro H2; elim H1; intros ? H4 ?; elim H4; intros ? H6; rewrite H2 in H6; subst b; contradict H; rewrite Z.mul_0_r; discriminate). assert (H3 : g > 0) by (apply Z.lt_gt, Z.le_neq; split; try apply Z.ge_le; auto). unfold rel_prime. destruct H1 as [Ha Hb Hab]. destruct Ha as [a' Ha']. destruct Hb as [b' Hb']. replace (a/g) with a'; [|rewrite Ha'; rewrite Z_div_mult; auto with zarith]. replace (b/g) with b'; [|rewrite Hb'; rewrite Z_div_mult; auto with zarith]. constructor. - exists a'; rewrite ?Z.mul_1_r; auto with zarith. - exists b'; rewrite ?Z.mul_1_r; auto with zarith. - intros x (xa,H5) (xb,H6). destruct (Hab (x*g)) as (x',Hx'). + exists xa; rewrite Z.mul_assoc; rewrite <- H5; auto. + exists xb; rewrite Z.mul_assoc; rewrite <- H6; auto. + replace g with (1*g) in Hx'; auto with zarith. do 2 rewrite Z.mul_assoc in Hx'. apply Z.mul_reg_r in Hx'; trivial. rewrite Z.mul_1_r in Hx'. exists x'; auto with zarith. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat