proposition: Lemma Rlt_Rpower_l a b c: 0 < c -> 0 < a < b -> Rpower a c < Rpower b c.
proof: Proof. intros c0 [a0 ab]; apply exp_increasing. now apply Rmult_lt_compat_l; auto; apply ln_increasing; lra. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra