proposition: Lemma inj_Q_power_Z : forall q1 (n:Z) H, inj_Q (q1^n)%Q [=] ((inj_Q q1)[//]H)[^^]n.
proof: Proof. intros q [|n|n] H. change (inj_Q (q ^ 0)%Q[=][1]). apply inj_Q_One. simpl. change (inj_Q (q ^ n)%Q[=]inj_Q q[^]n). csetoid_rewrite_rev (inj_Q_power q n). rewrite inject_nat_convert. apply eq_reflexive. change ((inj_Q (/q ^ n))%Q[=]([1][/]inj_Q q[//]H)[^]n). stepl (inj_Q ((1/q)^n)%Q). stepr ((inj_Q (1/q)%Q)[^]n). csetoid_rewrite_rev (inj_Q_power (1/q)%Q n). rewrite inject_nat_convert. apply eq_reflexive. apply nexp_wd. stepr (inj_Q 1%Q[/]_[//]H). apply inj_Q_div. apply div_wd. rstepr (nring 1:R1). apply (inj_Q_nring 1). apply eq_reflexive. apply inj_Q_wd. change (((1 * / q) ^ n)%Q==(/ q ^ n))%Q. rewrite <- Qinv_power. rewrite -> Qmult_1_l. reflexivity. 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