proposition: Lemma leqn_log m n: m <= n -> log2 m <= log2 n.
proof: Proof. case:m => //; case:n=> // m n le1. move: (log2_bnd n) (log2_bnd m) => /andP[e1 _]/andP[_ e4]. by move: (leq_ltn_trans (leq_trans e1 le1) e4); rewrite ltn_exp2l //-{1}log2S_k. 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)