proposition: Lemma Rle_exp2_log1_L a b : 0 < b -> (exp2 a <= b)%mcR = (a <= log b)%mcR.
proof: Proof. move=> Hb; move H1 : (_ <= _ )%mcR => [|] /=. - move/RleP in H1. have {}H1 : a <= log b. rewrite (_ : a = log (exp2 a)); last by rewrite exp2K. exact: Log_increasing_le. by move/RleP : H1 => ->. - move H2 : (_ <= _ )%mcR => [|] //=. move/RleP in H2. rewrite -(@ExpK 2 a _) // 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