proposition: Lemma leB_bounded_weaken {n} : forall (p:BITS n) m1 m2 m3, m3 < 2^n -> m1 <= m2 -> m2 <= m3 -> leB p (p +# m3) -> leB (p +# m1) (p +# m2).
proof: Proof. move => p m1 m2 m3 BOUND LE1 LE2. move => H. assert (H1 := leB_bounded BOUND H). rewrite leB_nat. rewrite /adcB !adcBmain_nat add0n 2!splitmsb_fromNat. assert (m2 < 2^n) by apply (leq_ltn_trans LE2 BOUND). rewrite (toNat_fromNatBounded H0). assert (m1 < 2^n) by apply (leq_ltn_trans (leq_trans LE1 LE2) BOUND). rewrite (toNat_fromNatBounded H2). rewrite !toNat_fromNatBounded. by rewrite leq_add2l. assert (toNat p + m2 <= toNat p + m3). by rewrite leq_add2l. apply (leq_ltn_trans H3 H1). assert (toNat p + m1 <= toNat p + m3). rewrite leq_add2l. apply (leq_trans LE1 LE2). apply (leq_ltn_trans H3 H1). 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)