proposition: Lemma process_eval_rec5_loss_win_lt ht (a res : estate) l : Hiv l -> ht_valid ht -> a <= res -> a < \smin_(i <- l) f1 i -> process_eval_rec5 f2 eloss ewin ht res l <= esflip a.
proof: Proof. elim: l ht res => [|i l IH] ht res HHiv Hv aLr. by rewrite big_nil esflip_le. rewrite big_cons => /= aLs. case E : f2 => [ht1 res1]. have -> : res1 = f2 eloss ewin ht i by rewrite E. have -> : ht1 = f2 eloss ewin ht i by rewrite E. have HHiv1 := Hiv_cons HHiv. rewrite (H5loss_win HHiv) //. have [E1|E1] := leqP res _. apply: IH => //; first by apply: (H5loss_win_table HHiv). by apply: leq_trans aLs (ge_sminr _ _). have [E2|E2] := leqP ewin _. apply: IH => //; first by apply: (H5loss_win_table HHiv). 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_rec5_loss_draw_le HHiv1 _ _ _) _ => //. by apply: (H5loss_win_table HHiv). rewrite (esflip_le edraw). by apply: ltnW. rewrite smin_ler // in aLs *; last by apply: ltnW. suff -> : f1 i = win. apply: IH => //; first by apply: (H5loss_win_table HHiv). by apply: le_ewin. by case: f1 E3 aLs => //; case: (\smin_(_ <- _) _) => //; case: (a). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)