proposition: Lemma process_eval_rec5_loss_draw_loss ht (res : estate) l : Hiv l -> ht_valid ht -> \smin_(i <- l) f1 i = loss -> process_eval_rec5 f2 eloss edraw ht res l = ewin :> estate.
proof: Proof. elim: l ht res => [|i l IH] ht res HHiv Hv; first by rewrite big_nil. rewrite big_cons [process_eval_rec5 _ _ _ _ _ _]/= => H. case E : f2 => [ht1 res1]. have -> : res1 = f2 eloss edraw ht i by rewrite E. have -> : ht1 = f2 eloss edraw ht i by rewrite E. have HHiv1 := Hiv_cons HHiv. have [E1|E1] := leqP res (f2 _ _ _ _). have [E2|/ltnW E2] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite smin_lel // in H. apply: ge_ewinE; rewrite -[ewin]/(esflip eloss). have -> : res = eloss. by apply: le_elossE => //; rewrite -(H5loss_draw_loss HHiv Hv H). by apply: ge_process_eval_rec5. rewrite smin_ler // in H. by apply: IH => //; apply: (H5loss_draw_table HHiv). have [E2|E2] := leqP _ (f2 _ _ _ _). have [E3|/ltnW E3] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite smin_lel // in H. rewrite (H5loss_draw_loss HHiv) //. apply: ge_ewinE; rewrite -[ewin]/(esflip eloss). by apply: ge_process_eval_rec5. rewrite smin_ler // in H. by apply: IH => //; apply: (H5loss_draw_table HHiv). rewrite (H5loss_draw_loss HHiv) //=. by case: f1 (@H5loss_draw_draw ht i l HHiv Hv) (@H5loss_draw_win ht i l HHiv Hv) => // [_|]; move=> /(_ (refl_equal _)); case: f2 E2 => h; case. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)