proposition: Lemma bin_invert_p1 n: 2^((log2 n).-1) < n -> n + (bin_invert n) = 3* 2^ ((log2 n).-1).
proof: Proof. case: n => // n; case: (elogn2P n) => k q ->. case: q; [ by rewrite muln1 log2_pow // succnK // ltnn | move => q _]. elim: {n} k q; last first. move => n Hrec q. rewrite expnS - mulnA mul2n bin_invert_double - doubleD Hrec // doubleMr. set x := 2^n *_; have: 0 < x by rewrite lt0n muln_eq0 expn_eq0. by move/prednK => <-; rewrite log2_double -expn2S -log2S_k succnK. move => q. rewrite mul1n /bin_invert /log2 - {1} (bin_of_natK ((q.+1).*2.+1)). rewrite - {1} (list_of_numK (bin_of_nat (q.+1).*2.+1)). set l := list_of_num _; have [u [s ->]]: exists u s, l = true::u::s. rewrite /l bin_of_nato /list_of_num /list_of_pos -/list_of_pos. case(pos_of_nat' q) => [ p | p |]. + by exists true,(list_of_pos p). + by exists false,(list_of_pos p). + by exists true, nil. rewrite /bin_invert_aux map_cons /size -/size succnK expnS. rewrite /num_of_list /pos_of_list -/(pos_of_list (u::s)) -/(pos_of_list (_::_)). rewrite /nat_of_bin /nat_of_pos -/nat_of_pos !natTrecE addSn addnS - doubleD. rewrite -doubleS mulnCA mul2n; apply/eqP; rewrite eqn_double; apply /eqP. elim: s u => // a s Hrec. rewrite /size -/size expnS mulnCA mul2n. by case;rewrite /= !natTrecE ?addSn ?addnS - doubleD - doubleS Hrec. 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)