proposition: Lemma log2_mul_exp a n: a != 0 -> log2 (a* 2^n) = n + log2 a.
proof: Proof. move=> ap;elim: n => [|n H]; rewrite ?muln1 // expnS mulnCA mul2n addSn -H. have h: 0 < a * 2 ^ n by rewrite muln_gt0 expn_gt0 lt0n (negbTE ap). by rewrite -(prednK h) log2_double. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)