proposition: Lemma size_bitseq_of_N_lb i n : 2 ^ n <= i -> n < size (bitseq_of_N (bin_of_nat i)).
proof: Proof. move=> Hn; by rewrite size_bitseq_of_N_lb' // bin_of_natK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext