proposition: Lemma toNat_incB n : forall (p: BITS n), toNat (incB p) = if p == ones _ then 0 else (toNat p).+1.
proof: Proof. induction n. + move => p. by rewrite (tuple0 p). + case/tupleP => [b p]. rewrite /= theadCons beheadCons toNatCons. destruct b => //. rewrite toNat_joinlsb add0n add1n IHn. case E: (p == ones n). + by replace (_ == _) with true. + by rewrite ones_decomp/= bitsEq_decomp doubleS E. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations