proposition: Lemma Q2R_pow_pos : forall q p, Q2R (pow_pos Qmult q p) = pow_pos Rmult (Q2R q) p.
proof: Proof. induction p ; simpl;auto; rewrite <- IHp; repeat rewrite Q2R_mult; reflexivity. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant