proposition: Lemma process_eval_rec3_correct_b (res beta : state) l : alpha < beta <= res -> beta <= \smin_(i <- l) f1 i -> process_eval_rec3 f2 alpha beta res l <= sflip beta.
proof: Proof. elim: l res beta => /= [| i l IH] res beta /andP[aLb bLr]. by rewrite sflip_le. rewrite big_cons /= => H. have [E1|E1] := leqP res _. apply: IH => //; first by rewrite aLb. by apply: leq_trans H (ge_sminr _ _). have [E2|E2] := leqP beta (f2 _ _ _). apply: IH => //; first by rewrite aLb. by apply: leq_trans H (ge_sminr _ _). rewrite ltnNge in E2; case/negP: E2. apply: f1Hb => //; rewrite aLb /=. by apply: leq_trans H (ge_sminl _ _). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)