fact: Definition N_of_bitseq s : N := match rem_lea_false s with | [::] => N0 | true :: t => Npos (pos_of_bitseq (rev t)) | _ => N0 end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext