proposition: Lemma bitsP p : Pos.to_nat p = \sum_(i < size (bits p [::])) nth false (bits p [::]) (size (bits p [::]) - 1 - i) * 2 ^ i.
proof: Proof. have body_simp p' b: forall i : 'I_(size (bits p' [::])), true -> nth false (bits p' [::] ++ [:: b]) (size (bits p' [::]) - bump 0 i) * 2 ^ bump 0 i = 2 * (nth false (bits p' [::]) (size (bits p' [::]) - 1 - i) * 2 ^ i). move=> i _; rewrite /bump leq0n add1n (mulnC 2) -mulnA -expnSr -subnDA. rewrite add1n nth_cat. set e := (X in if X then _ else _). have -> // : e. rewrite /e {e}; case: i => [ i] /=; case: (size _) => // n _. by rewrite subSS ltnS leq_subr. elim:p => [ p IH | p IH | ]. rewrite /= Pos2Nat.inj_xI multE bits_cat size_cat /= addn1. rewrite [RHS]big_ord_recl subSS 2!subn0 expn0 muln1. rewrite nth_cat ltnn subnn /= add1n; congr (_.+1). rewrite (eq_bigr _ (body_simp p true)). by rewrite IH -big_distrr. rewrite /= Pos2Nat.inj_xO multE bits_cat size_cat /= addn1. rewrite [RHS]big_ord_recl subSS 2!subn0 expn0 muln1. rewrite nth_cat ltnn subnn /=. rewrite (eq_bigr _ (body_simp p false)). by rewrite IH -big_distrr. by rewrite /= big_ord_recl big_ord0. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)