proposition: Lemma bitseq_of_pos_not_false a : bitseq_of_pos a <> [:: false].
proof: Proof. exact: bitseq_of_pos_not_nseq_false a 1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext