proposition: Lemma bitseq_of_N_bin_of_nat_expn2 : forall m : nat, bitseq_of_N (bin_of_nat (2 ^ m)) = nseq m false ++ [:: true].
proof: Proof. elim => // m0 IH. rewrite [in X in _ = X]/= -IH bin_of_nat_expn2 bitseq_of_N_2 //. suff [i Hi] : exists i, 2 ^ m0 = nat_of_pos i. rewrite Hi. by apply bin_of_nat_nat_of_pos_not_0. exists (Pos.of_nat (2 ^ m0)). rewrite -BinPos_nat_of_P_nat_of_pos Nat2Pos.id //. apply/eqP; by rewrite -lt0n expn_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext