proposition: Lemma msbNonNil n (p: BITS n.+1) b : msb p = last b p.
proof: Proof. by case/tupleP: p => b' q. 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