proposition: Lemma toZp_joinmsb0 n (p: BITS n) : toZp (joinmsb0 p) = toZpAux p.
proof: Proof. apply val_inj. rewrite /toZp/toZpAux/= Zp_cast; last apply pow2_gt1. by rewrite toNat_joinmsb0. 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