proposition: Lemma toNat_joinmsb n : forall c (p: BITS n), toNat (joinmsb (c, p)) = c * 2^n + toNat p.
proof: Proof. induction n. + move => c p. by rewrite /joinmsb (tuple0 p) expn0 muln1. + move => c. case/tupleP => [b p]. rewrite /joinmsb-/joinmsb /splitlsb theadCons beheadCons !toNatCons expnS IHn. by rewrite doubleD addnCA -mul2n mulnCA. 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