proposition: Lemma Q_can_den_spec : forall q q', q [=] q' -> Q_can_den q = Q_can_den q'.
proof: Proof. intros q q'. unfold Q_can_den. destruct q as [qn qd]; destruct q' as [q'n q'd]. simpl; unfold Qeq; simpl. intro Heq. apply (Zmult_reg_l _ _ (Zgcd qn qd * Zgcd q'n q'd)). intro; destruct (Zmult_integral _ _ H); destruct (Zgcd_zero _ _ H0); discriminate. rewrite -> (Zmult_comm (Zgcd qn qd)) at 1. rewrite <- Zmult_assoc, <- Zmult_assoc. rewrite -> (Zmult_comm (Zgcd qn qd)) at 1. rewrite (Zmult_comm (Zgcd q'n q'd) (q'd / Zgcd q'n q'd)). rewrite <- Zgcd_div_mult_rht, <- Zgcd_div_mult_rht; try (intro H; destruct (Zgcd_zero _ _ H); discriminate). rewrite Zmult_comm, (Zmult_comm _ q'd). rewrite <- (Zabs_Zsgn qd) at 1; rewrite <- (Zabs_Zsgn q'd) at 2. rewrite (Zmult_comm (Z.abs qd)), (Zmult_comm (Z.abs q'd)). rewrite <- Zmult_assoc, <- Zmult_assoc. rewrite Zgcd_lin, Zgcd_lin. rewrite (Zmult_comm qd q'n), (Zmult_comm q'd qn). rewrite Heq. rewrite (Zmult_comm qd q'd). reflexivity. Qed.
imports: CRings Qring Zring Zlcm