proposition: Lemma inj_Q_One : inj_Q [1] [=] [1].
proof: Proof. rstepr ((nring 1):R1). apply (inj_Q_nring 1). 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