proposition: Lemma injZ_spec : forall q : Q_as_CRing, in_Z q -> q [=] (Q_can_num q).
proof: Proof. unfold in_Z. intros q Hin. destruct q as [qn qd]. unfold inject_Z. simpl; unfold Qeq; simpl. rewrite Zmult_1_r. unfold Q_can_num; simpl. unfold Q_can_den in Hin. simpl in Hin. cut (Zpos qd = Zgcd qn qd). intro H; rewrite H at 2. rewrite Zmult_comm. symmetry; apply Zdivides_spec. apply Zgcd_is_divisor_lft. rewrite (Zgcd_div_mult_rht qn qd) at 1. rewrite Hin; rewrite Zmult_1_l; reflexivity. intro H; destruct (Zgcd_zero _ _ H); discriminate. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg