proposition: Lemma process_eval_rec4_loss_draw_le (res : estate) l : draw <= res -> draw <= \smin_(i <- l) f1 i -> process_eval_rec4 f2 eloss edraw res l <= draw.
proof: Proof. elim: l res => [|i l IH] res; first by rewrite big_nil (esflip_le _ edraw). rewrite big_cons [process_eval_rec4 _ _ _ _ _]/= => H1 H2. have [E1|E1] := leqP res (f2 _ _ _). by apply: IH => //; apply: leq_trans H2 (ge_sminr _ _). rewrite ifT; last first. by apply: H4loss_draw_ge; apply: leq_trans H2 (ge_sminl _ _). apply: IH => //. by apply: H4loss_draw_ge; apply: leq_trans H2 (ge_sminl _ _). by apply: leq_trans H2 (ge_sminr _ _). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)