proposition: Lemma Rle_exp2_log2_R b c : 0 < b -> (b <= exp2 c)%mcR = (log b <= c)%mcR.
proof: Proof. move=> Hb; move H1 : (_ <= _)%mcR => [|] /=. - move/RleP in H1. have {}H1 : log b <= c. rewrite (_ : c = log (exp2 c)); last by rewrite exp2K. apply Log_increasing_le => //; exact: exp2_pos. by move/RleP in H1. - move H2 : (_ <= _ )%mcR => [|] //=. move/RleP in H2. rewrite -(exp2K c) in H2. apply Log_le_inv in H2 => //. move/RleP in H2. by rewrite H2 in H1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext