proposition: Lemma Qred_identity2 : forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z.
proof: Proof. intros (a,b) H; simpl in *. generalize (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)). rewrite <- Z.ggcd_gcd. destruct Z.ggcd as (g,(aa,bb)); simpl in *. injection H as [= <- <-]. intros H (_,H'). destruct g as [|g|g]; [ discriminate | | now elim H ]. destruct bb as [|b|b]; simpl in *; try discriminate. injection H' as [= H']. f_equal. apply Pos.mul_reg_r with b. now rewrite Pos.mul_1_l. Qed.
imports: Field QArith Znumtheory Eqdep_dec