proposition: Lemma pow_Rle_r_1 : forall (y: R) (n : nat), - 1 <= y -> y <= 1 -> pow y n <= 1.
proof: Proof. intros y n H1 H2; rewrite <- pow1 with n; apply pow_Rle_r; assumption. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)