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