proposition: Lemma Qred_complete : forall p q, p==q -> Qred p = Qred q.
proof: Proof. intros (a,b) (c,d). unfold Qred, Qeq in *; simpl in *. Open Scope Z_scope. intros H. generalize (Z.ggcd_gcd a (Zpos b)) (Zgcd_is_gcd a (Zpos b)) (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)). destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)). simpl. intros <- Hg1 Hg2 (Hg3,Hg4). assert (Hg0 : g <> 0) by (intro; now subst g). generalize (Z.ggcd_gcd c (Zpos d)) (Zgcd_is_gcd c (Zpos d)) (Z.gcd_nonneg c (Zpos d)) (Z.ggcd_correct_divisors c (Zpos d)). destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)). simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4). assert (Hg'0 : g' <> 0) by (intro; now subst g'). elim (rel_prime_cross_prod aa bb cc dd). - congruence. - constructor. * exists aa; auto using Z.mul_1_r. * exists bb; auto using Z.mul_1_r. * intros x Ha Hb. destruct Hg1 as (Hg11,Hg12,Hg13). destruct (Hg13 (g*x)) as (x',Hx). { rewrite Hg3. destruct Ha as (xa,Hxa); exists xa; rewrite Hxa; ring. } { rewrite Hg4. destruct Hb as (xb,Hxb); exists xb; rewrite Hxb; ring. } exists x'. apply Z.mul_reg_l with g; auto. rewrite Hx at 1; ring. - constructor. * exists cc; auto using Z.mul_1_r. * exists dd; auto using Z.mul_1_r. * intros x Hc Hd. inversion Hg'1 as (Hg'11,Hg'12,Hg'13). destruct (Hg'13 (g'*x)) as (x',Hx). { rewrite Hg'3. destruct Hc as (xc,Hxc); exists xc; rewrite Hxc; ring. } { rewrite Hg'4. destruct Hd as (xd,Hxd); exists xd; rewrite Hxd; ring. } exists x'. apply Z.mul_reg_l with g'; auto. rewrite Hx at 1; ring. - apply Z.lt_gt. rewrite <- (Z.mul_pos_cancel_l g); [ now rewrite <- Hg4 | apply Z.le_neq; intuition ]. - apply Z.lt_gt. rewrite <- (Z.mul_pos_cancel_l g'); [now rewrite <- Hg'4 | apply Z.le_neq; intuition ]. - apply Z.mul_reg_l with (g*g'). * rewrite Z.mul_eq_0. now destruct 1. * rewrite Z.mul_shuffle1, <- Hg3, <- Hg'4. now rewrite Z.mul_shuffle1, <- Hg'3, <- Hg4, H, Z.mul_comm. Close Scope Z_scope. Qed.
imports: QArith_base Znumtheory