proposition: Lemma process_eval_rec4_loss_win_lt (a res : estate) l : a <= res -> a < \smin_(i <- l) f1 i -> process_eval_rec4 f2 eloss ewin res l <= esflip a.
proof: Proof. elim: l res => [|i l IH] res aLr; first by rewrite big_nil esflip_le. rewrite big_cons => /= aLs; rewrite H4loss_win. have [E1|E1] := leqP res _. apply: IH => //. by apply: leq_trans aLs (ge_sminr _ _). have [E2|E2] := leqP ewin _. apply: IH => //. by rewrite (ge_ewinE E2) // le_ewin. by apply: leq_trans aLs (ge_sminr _ _). rewrite ifN; last first. rewrite -ltnNge es2ns2esK. apply: leq_ltn_trans _ (leq_trans aLs (ge_sminl _ _)). by case: (a). have [E3|E3] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite smin_lel // in aLs *. have H : f1 i = draw. by case: f1 E2 E3 aLs => //; case: (\smin_(_ <- _) _) => //; case: (a). rewrite H in E1 E3 aLs *. apply: leq_trans (process_eval_rec4_loss_draw_le _ _) _ =>//. rewrite (esflip_le edraw). by apply: ltnW. rewrite smin_ler // in aLs *; last by apply: ltnW. suff -> : f1 i = win. by apply: IH => //; apply: le_ewin. by case: f1 E3 aLs => //; case: (\smin_(_ <- _) _) => //; case: (a). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)