proposition: Lemma getBit_joinmsb : forall n (bs: BITS n) k, k <= n -> getBit (joinmsb (false , bs)) k = getBit bs k.
proof: Proof. elim=> [|n IHn] bs k leq_k_n. - rewrite leqn0 in leq_k_n. move/eqP: leq_k_n=> ->. by rewrite !tuple0. - case/tupleP: bs=> [b bs]. case: k leq_k_n => [|k leq_k_n]. + by trivial. + rewrite /joinmsb/splitlsb tuple.beheadCons tuple.theadCons -/joinmsb /joinlsb //=. by apply: IHn; assumption. 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