proposition: Lemma bitseq_of_nat_inj n i j : i < 2 ^ n -> j < 2 ^ n -> bitseq_of_nat i n = bitseq_of_nat j n -> i = j.
proof: Proof. move=> Hi Hj. case/boolP : (i == 0) => [/eqP -> | /eqP Hi0]. rewrite bitseq_of_nat_0 => abs. apply/eqP/negPn/negP. rewrite eq_sym => /eqP. move/(@bitseq_of_nat_nseq_false j n); by apply. case/boolP : (j == 0) => [/eqP -> | /eqP Hj0]. rewrite bitseq_of_nat_0 => abs. apply/eqP/negPn/negP. move/eqP/(@bitseq_of_nat_nseq_false i n); by apply. move=> H. by rewrite -(N_of_bitseq_bitseq_of_nat Hi0 Hi) -(N_of_bitseq_bitseq_of_nat Hj0 Hj) H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext