proposition: Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> Rpower a c <= Rpower b c.
proof: Proof. intros [c0 | c0]; [ | intros; rewrite <- c0, !Rpower_O; [apply Rle_refl | |] ]. - intros [a0 [ab|ab]]. + now apply Rlt_le, Rlt_Rpower_l;[ | split]; lra. + rewrite ab; apply Rle_refl. - apply Rlt_le_trans with a; tauto. - tauto. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra