proposition: Lemma getBit_dropmsb: forall n (bs : BITS n.+1) k, k < n -> getBit (dropmsb bs) k = getBit bs k.
proof: Proof. elim=> // n /= IHn /tupleP[b bs] k le_k. rewrite /dropmsb /splitmsb /= tuple.theadCons tuple.beheadCons /= -/splitmsb. set cr := splitmsb bs; rewrite (surjective_pairing cr). have ->: ((cr.1, joinlsb (cr.2, b))).2 = joinlsb (dropmsb bs, b) by rewrite /dropmsb. case: k le_k => // k le_k. + have H: forall bs', getBit (joinlsb (bs', b)) k.+1 = getBit bs' k by compute. by rewrite !H; auto with arith. 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