proposition: Lemma Q2RpowerRZ : forall q z (DEF : not (q == 0)%Q \/ (z >= Z0)%Z), Q2R (q ^ z) = powerRZ (Q2R q) z.
proof: Proof. intros. destruct Qpower_theory. destruct R_power_theory. unfold Qpower, powerRZ. destruct z. - apply Q2R_1. - change (Qpower_positive q p) with (Qpower q (Zpos p)). rewrite <- N2Z.inj_pos. rewrite <- positive_N_nat. rewrite rpow_pow_N. rewrite rpow_pow_N0. apply Q2R_pow_N. - rewrite Q2R_inv. + unfold Qpower_positive. rewrite <- positive_N_nat. rewrite rpow_pow_N0. unfold pow_N. rewrite Q2R_pow_pos. auto. + intro. apply Qpower_positive_eq_zero in H. destruct DEF ; auto with arith. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant