proposition: Lemma msb0Bounded n (p: BITS n.+1) : msb p == false <-> toNat p < 2^n.
proof: Proof. induction n. case/tupleP: p => [b p]. rewrite (tuple0 p). by destruct b. case/tupleP: p => [b p]. split => H. rewrite toNatCons. rewrite msbCons in H. destruct (IHn p) as [H1 H2]. specialize (H1 H). destruct b. rewrite add1n expnS mul2n. by rewrite ltn_Sdouble. rewrite add0n expnS mul2n. by rewrite ltn_double. rewrite toNatCons in H. destruct (IHn p) as [H1 H2]. rewrite msbCons. apply H2. destruct b. rewrite add1n expnS mul2n in H. by rewrite ltn_Sdouble in H. rewrite add0n expnS mul2n in H. by rewrite ltn_double in H. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)