proposition: Lemma log2_pr1 n (q := 2^ (log2 n).-1) : n !=0 -> n = q + (n %% q).
proof: Proof. rewrite /q {q};case: n => // n _;apply/eqP;move:(log2_bnd n) => /=. rewrite {2}(log2S_k n) expn2S -addnn; set q := 2^ _;case/andP => [ea]. rewrite - {1 2 3}(subnKC ea) ltn_add2l eqn_add2l => /modn_small <-. by rewrite modnDl modn_mod. 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)