proposition: Lemma pow_le_compat : forall x y, 0 <= x -> x <= y -> forall n, x ^ n <= y ^ n.
proof: Proof. intros x y x_pos x_lt_y n. induction n. simpl ; apply Req_le ; reflexivity. simpl ; apply Rmult_le_compat ; [| apply pow_le | |] ; assumption. Qed.
imports: Reals MyRIneq Fourier Lia Lra Rsequence_usual_facts