proposition: Lemma process_eval_rec4_draw_win_ge (res : estate) l : lossdraw <= res -> draw <= \smin_(i <- l) f1 i -> process_eval_rec4 f2 edraw ewin res l <= drawwin.
proof: Proof. elim: l res => [|i l IH] res; first by rewrite big_nil (esflip_le _ lossdraw). rewrite big_cons [process_eval_rec4 _ _ _ _ _]/= => H1 H2. have [E1|E1] := leqP res (f2 _ _ _). apply: IH => //. by apply: leq_trans H2 (ge_sminr _ _). have [E2|E2] := leqP ewin (f2 _ _ _). apply: IH => //. apply: H4draw_win_ge. by apply: leq_trans H2 (ge_sminl _ _). by apply: leq_trans H2 (ge_sminr _ _). have [E3|E3] := leqP (f2 edraw ewin i) edraw. have : lossdraw <= (f2 edraw ewin i). apply: H4draw_win_ge (leq_trans H2 (ge_sminl _ _)). by case: f2 => //=; case: (l). have [E4|E4] := leqP (f1 i) draw. rewrite ltnNge in E3; case/negP: E3. by apply: H4draw_win_le. rewrite H4draw_win_win // in E2. apply: ge_winE. by case: f1 E4. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)