proposition: Lemma bitseq_of_nat_nseq_false i r : i <> O -> i < 2 ^ r -> bitseq_of_nat i r <> nseq r false.
proof: Proof. move=> Hi Hin. rewrite /bitseq_of_nat /pad_seqL. have : size (bitseq_of_N (bin_of_nat i)) <= r by exact/size_bitseq_of_N_ub. rewrite leq_eqVlt. case/orP => X. - move/eqP : X => X. rewrite {1}size_rev {1}X leqnn -X -{1}size_rev subnn /=. have Y : bitseq_of_N (bin_of_nat i) <> rev (nseq (size (bitseq_of_N (bin_of_nat i))) false). rewrite rev_nseq. exact: bitseq_of_N_nseq_false. contradict Y. by rewrite -Y revK. - rewrite {1}size_rev leq_eqVlt X orbC /= size_rev => abs. move: (nseq_cat abs) => {}abs. have W : bitseq_of_N (bin_of_nat i) = nseq (size (rev (bitseq_of_N (bin_of_nat i)))) false. by rewrite -[LHS]revK abs rev_nseq !size_nseq. exact: bitseq_of_N_nseq_false Hi W. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext