proposition: Lemma exp2K x : log (exp2 x) = x.
proof: Proof. by rewrite /exp2 -/(Exp 2 x) /log -/(Log 2 _) ExpK. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext