proposition: Lemma inj_Q_nring : forall n, inj_Q (nring n) [=] nring (R:=R1) n.
proof: Proof. intro. simpl in |- *. induction n as [| n Hrecn]. simpl in |- *. rational. change (inj_Q (nring n[+][1]) [=] nring (R:=R1) n[+][1]) in |- *. astepr (inj_Q (nring n)[+]inj_Q [1]). apply inj_Q_plus. apply bin_op_wd_unfolded. assumption. simpl in |- *. unfold pring in |- *; simpl in |- *. rational. 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