proposition: Lemma getBit_ones: forall n k, k < n -> getBit (ones n) k = true.
proof: Proof. move=> n k le_k. by rewrite /getBit nth_nseq le_k. Qed.
imports: Coq(ZArith.ZArith) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg) ssrextra.nat ssrextra.tuple spec.spec