proposition: Lemma Qred_identity : forall q:Q, Z.gcd (Qnum q) (QDen q) = 1%Z -> Qred q = q.
proof: Proof. intros (a,b) H; simpl in *. rewrite <- Z.ggcd_gcd in H. generalize (Z.ggcd_correct_divisors a (Zpos b)). destruct Z.ggcd as (g,(aa,bb)); simpl in *; subst. rewrite !Z.mul_1_l. now intros (<-,<-). Qed.
imports: Field QArith Znumtheory Eqdep_dec