proposition: Lemma Q2R_pow: forall (x : Q) (n : nat), (Q2R x ^ n)%R = Q2R (x ^ Z.of_nat n).
proof: Proof. intros x n. induction n. - cbn. unfold Q2R. cbn. lra. - rewrite Qpower_nat_succ. cbn. rewrite Qreals.Q2R_mult. rewrite IHn. reflexivity. Qed.
imports: Reals ZArith QArith Lra Lia