proposition: Lemma getBit_low n1: forall n2 (p: BITS (n1+n2)) i, getBit (low n1 p) i = if i < n1 then getBit p i else false.
proof: Proof. induction n1 => // n2 p i. destruct i => //. case/tupleP: p => [b p]. rewrite /getBit/joinlsb/= beheadCons theadCons. destruct i => //. apply IHn1. 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