proposition: Lemma joinmsbK n : cancel (@joinmsb n) (@splitmsb n).
proof: Proof. induction n. + move => [b p]. by rewrite !(tuple0 p) /= theadCons beheadCons. + move => [c p]. case/tupleP: p => [b p]. by rewrite /= !theadCons !beheadCons IHn. 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