proposition: Lemma inj_Q_power : forall q1 (n:nat), inj_Q (q1^n)%Q [=] (inj_Q q1[^]n).
proof: Proof. intros q. induction n. apply inj_Q_One. rewrite inj_S. unfold Z.succ. stepr (inj_Q (q^n*q)%Q). apply inj_Q_wd. simpl. apply Qpower_plus'. auto with *. stepr (inj_Q (q^n)%Q[*]inj_Q q). apply inj_Q_mult. simpl. apply mult_wdl. assumption. 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