proposition: Lemma log_exp1_Rle_0 : 0 <= log (exp 1).
proof: Proof. rewrite logexp1E. apply/RleP. rewrite RinvE ?ln2_neq0// invr_ge0. exact/ltW/RltP/ln2_gt0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext