proposition: Lemma bitseq_of_pos_true : forall p, bitseq_of_pos p = [:: true] -> p = xH.
proof: Proof. by case => //; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext