proposition: Lemma bitseq_of_N_2 x : x <> N0 -> bitseq_of_N (2 * x) = false :: bitseq_of_N x.
proof: Proof. by case : x. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext