proposition: Lemma ltB_leB n (p q: BITS n.+1) : ltB p q -> leB (p +# 1) q.
proof: Proof. move => H. rewrite leB_nat toNat_addB toNat_fromNat. rewrite (@modn_small 1). rewrite modn_small. rewrite addn1. by rewrite ltB_nat in H. have LTB := ltB_bound H. rewrite -(ltn_add2r 1) in LTB. rewrite addn1. rewrite !addn1 in LTB. rewrite prednK in LTB. apply LTB. apply expn_gt0. apply pow2_gt1. 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)