proposition: Lemma Q2R_pow_N : forall q n, Q2R (pow_N 1%Q Qmult q n) = pow_N 1 Rmult (Q2R q) n.
proof: Proof. destruct n ; simpl. - apply Q2R_1. - apply Q2R_pow_pos. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant