proposition: Lemma process_eval_rec5_draw_win_ge ht (res : estate) l : Hiv l -> ht_valid ht -> lossdraw <= res -> draw <= \smin_(i <- l) f1 i -> process_eval_rec5 f2 edraw ewin ht res l <= drawwin.
proof: Proof. elim: l ht res => [|i l IH] ht res HHiv Hv. by rewrite big_nil (esflip_le _ lossdraw). rewrite big_cons [process_eval_rec5 _ _ _ _ _ _]/= => H1 H2. case E : f2 => [ht1 res1]. have -> : res1 = f2 edraw ewin ht i by rewrite E. have -> : ht1 = f2 edraw ewin ht i by rewrite E. have HHiv1 := Hiv_cons HHiv. have [E1|E1] := leqP res (f2 _ _ _ _). apply: IH => //; first by apply: (H5draw_win_table HHiv). by apply: leq_trans H2 (ge_sminr _ _). have [E2|E2] := leqP ewin (f2 _ _ _ _). apply: IH => //; first by apply: (H5draw_win_table HHiv). apply: (H5draw_win_ge HHiv) => //. by apply: leq_trans H2 (ge_sminl _ _). by apply: leq_trans H2 (ge_sminr _ _). have [E3|E3] := leqP (f2 edraw ewin ht i) edraw. have : lossdraw <= (f2 edraw ewin ht i). apply: (H5draw_win_ge HHiv) (leq_trans H2 (ge_sminl _ _)) => //. by case: pres2state => //= _; case: (l). have [E4|E4] := leqP (f1 i) draw. rewrite ltnNge in E3; case/negP: E3. by apply: (H5draw_win_le HHiv). rewrite (H5draw_win_win HHiv) // in E2. apply: ge_winE. by case: f1 E4. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)