proposition: Lemma ltB_incL n q (p: BITS n.+1) : leB #1 q -> ltB p (q -#1) -> ltB (p +#1) q.
proof: Proof. rewrite leB_nat !ltB_nat toNat_addB toNat_fromNat. rewrite modn_small; last apply pow2_gt1. rewrite subB1. rewrite toNat_decB. case E: (q == #0). + by rewrite (eqP E) toNat_fromNat0. + move => E1 E2. rewrite -(ltn_add2r 1) in E2. rewrite 2!addn1 in E2. rewrite prednK in E2 => //. rewrite addn1. rewrite modn_small => //. have B:= toNatBounded q. by apply (ltn_trans E2). 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)