proposition: Lemma getUpdateSlice n1 n2 n3 (p: BITS (n1+n2+n3)) (q: BITS n2) : slice n1 n2 n3 (updateSlice _ _ _ p q) = q.
proof: Proof. rewrite /slice/updateSlice/split3/split2. by rewrite low_catB high_catB. 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