proposition: Lemma Q_can_num_spec : forall q q', q [=] q' -> Q_can_num q = Q_can_num q'.
proof: Proof. intros q q'. unfold Q_can_num. 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'n / Zgcd q'n q'd)). rewrite <- Zgcd_div_mult_lft, <- Zgcd_div_mult_lft; try (intro H; destruct (Zgcd_zero _ _ H); discriminate). rewrite Zmult_comm, (Zmult_comm _ q'n). rewrite <- (Zabs_Zsgn qn) at 1; rewrite <- (Zabs_Zsgn q'n) at 2. rewrite (Zmult_comm (Z.abs qn)), (Zmult_comm (Z.abs q'n)). rewrite <- Zmult_assoc, <- Zmult_assoc. rewrite Zgcd_lin, Zgcd_lin. rewrite Heq. rewrite (Zmult_comm qn q'n). cut (Z.sgn qn = Z.sgn q'n). intro H; rewrite H; reflexivity. destruct qn; destruct q'n; reflexivity||discriminate. Qed.
imports: CRings Qring Zring Zlcm