proposition: Lemma N_of_bitseq_false : forall l, N_of_bitseq (false :: l) = N_of_bitseq l.
proof: Proof. by case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext