proposition: Lemma ln_increasing_le a b : 0 < a -> a <= b -> ln a <= ln b.
proof: Proof. move=> Ha. case/Rle_lt_or_eq_dec; last first. by move=> ->; by apply/RleP; rewrite lexx. by move/(ln_increasing _ _ Ha)/ltRW. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext