proposition: Corollary toNat_ones n : toNat (ones n) = (2^n).-1.
proof: Proof. by rewrite -toNat_ones_succ succnK. 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