proposition: Lemma getBit_catB n1 n2 (p:BITS n1) (q:BITS n2) : forall i, getBit (p ## q) i = if i < n2 then getBit q i else getBit p (i-n2).
proof: Proof. induction n2 => // i. rewrite (tuple0 q). destruct i => //. case/tupleP: q => [b q] //. destruct i => //. apply IHn2. 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