proposition: Lemma injZ_spec2 : forall p : Z_as_CRing, p = Q_can_num p.
proof: Proof. intro p. unfold Q_can_num, inject_Z; simpl. rewrite Zgcd_one_rht, Zdiv_1_r; reflexivity. Qed.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg