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