proposition: Lemma Qred_correct : forall q, (Qred q) == q.
proof: Proof. unfold Qred, Qeq; intros (n,d); simpl. generalize (Z.ggcd_gcd n (Zpos d)) (Z.gcd_nonneg n (Zpos d)) (Z.ggcd_correct_divisors n (Zpos d)). destruct (Z.ggcd n (Zpos d)) as (g,(nn,dd)); simpl. Open Scope Z_scope. intros Hg LE (Hn,Hd). rewrite Hd, Hn. rewrite <- Hg in LE; clear Hg. assert (0 <> g) by (intro; subst; discriminate). rewrite Z2Pos.id. - ring. - now rewrite <- (Z.mul_pos_cancel_l g); [ rewrite <- Hd | apply Z.le_neq ]. Close Scope Z_scope. Qed.
imports: QArith_base Znumtheory