proposition: Lemma zring_Q : forall z, zring (R:=Q_as_CRing) z[=]inject_Z z.
proof: Proof. destruct z; simpl; try reflexivity. rewrite -> pring_convert. rewrite -> nring_Q. now rewrite convert_is_POS. rewrite -> pring_convert. rewrite -> nring_Q. unfold Qeq. simpl. ring_simplify. rewrite min_convert_is_NEG. now rewrite Pmult_comm. Qed.
imports: CoRN.model.abgroups.Qabgroup CoRN.algebra.CRings CoRN.model.rings.Zring