proposition: Lemma process_eval_rec4_draw_win_loss (res : estate) l : \smin_(i <- l) f1 i = loss -> drawwin <= process_eval_rec4 f2 edraw ewin res l.
proof: Proof. elim: l res => [|i l IH] res; first by rewrite big_nil. rewrite big_cons [process_eval_rec4 _ _ _ _ _]/= => H. have [E1|E1] := leqP res (f2 _ _ _). have [E2|/ltnW E2] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite smin_lel // in H. apply: leq_trans (ge_process_eval_rec4 _ _ _ _ _). rewrite (esflip_le lossdraw). apply: leq_trans E1 _. by apply: H4draw_win_loss. rewrite smin_ler // in H. by apply: IH. have [E2|E2] := leqP ewin (f2 _ _ _). have [E3|/ltnW E3] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite smin_lel // in H. have := H4draw_win_loss H. by rewrite leqNgt (leq_trans _ E2). rewrite smin_ler // in H. by apply: IH. have [E3|E3] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite smin_lel // in H. by case: f2 (H4draw_win_loss H). rewrite smin_ler // in H; last by apply: ltnW. have [E4|E4] := leqP (f2 _ _ _) edraw. have : lossdraw <= f2 edraw ewin i. apply: H4draw_win_ge. by move: E3; rewrite H; case: f1. case: f2 E4 => //=. by case: (l) H => //; rewrite big_nil. move: E3 E2; rewrite H. case: f1 (@H4draw_win_draw i) (@H4draw_win_win i) => //. by move=> _ -> //. move=> /(_ (refl_equal _)). by rewrite [_ <= edraw]leqNgt E4 andbF. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)