proposition: Lemma splitmsb_msb n (p:BITS n.+1) : (splitmsb p).1 = msb p.
proof: Proof. induction n. + case/tupleP: p => b q. by rewrite (tuple0 q)/= theadCons. + case/tupleP: p => b q. rewrite /= beheadCons theadCons. case E: (splitmsb q) => [b' q']. specialize (IHn q). rewrite E/= in IHn. simpl. rewrite (msbNonNil q b) in IHn. by subst. 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