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