proposition: Lemma count_ones: forall n, (count_mem true (ones n)) = n.
proof: Proof. elim=> //=. auto with arith. 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