proposition: Lemma Rle2_exp2_log a b c : 0 < b -> (exp2 a <= b <= exp2 c)%mcR = (a <= log b <= c)%mcR.
proof: Proof. move=> Hb; move H1 : (_ <= _ )%mcR => [|] /=. - rewrite Rle_exp2_log1_L // in H1. by rewrite H1 /= Rle_exp2_log2_R. - move H2 : (_ <= _ )%mcR => [|] //=. rewrite -Rle_exp2_log1_L // 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