proposition: Lemma toNatCat m n (p : BITS m) (q: BITS n) : toNat (p ## q) = toNat p * 2^n + toNat q.
proof: Proof. elim: n q; first by move=> q; rewrite (tuple0 q) addn0 expn0 muln1. move=> n IHn; case/tupleP => [b q]. rewrite /catB catCons !toNatCons IHn expnS -!muln2; ring. 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