proposition: Lemma inj_Q_zring : forall n, inj_Q (zring n) [=] zring (R:=R1) n.
proof: Proof. intros [|n|n]. simpl. rational. simpl. apply inj_Q_pring. change (inj_Q ([--](pring _ n))[=][--](pring _ n)). stepl ([--](inj_Q (zring (R:=Q_as_COrdField) n))). apply un_op_wd_unfolded. simpl. apply inj_Q_pring. apply eq_symmetric. apply inj_Q_inv. Qed.
imports: CoRN.model.reals.Cauchy_IR CoRN.model.monoids.Nmonoid CoRN.model.rings.Zring CoRN.algebra.CRing_Homomorphisms CoRN.algebra.Expon Coq.QArith.Qpower CoRN.tactics.CornTac