proposition: Lemma sliceEq n1 n2 n3 (p q: BITS (n1+n2+n3)) : (forall i, n1 <= i < n1+n2 -> getBit p i = getBit q i) <-> slice n1 n2 n3 p = slice n1 n2 n3 q.
proof: Proof. rewrite /slice/split3/split2. rewrite <-highBitsEq. split. move => H1 i LE. rewrite 2!getBit_low. case LT: (i < (n1+n2)) => //. - apply H1. by rewrite LE LT. move => H i. move/andP => [LE LT]. specialize (H i LE). by rewrite 2!getBit_low LT in H. 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