proposition: Lemma bitseq_of_N_leading_bit n : n <> N0 -> exists k, rev (bitseq_of_N n) = true :: k.
proof: Proof. case : n => //. elim => [i IH _ | i IH _ | _ /=]. - have : Npos i <> 0%N by []. case/IH => k /= Hk. exists (rcons k true); by rewrite rev_cons Hk. - have : Npos i <> 0%N by []. case/IH => k /= Hk. exists (rcons k false); by rewrite rev_cons Hk. - by exists nil. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext