proposition: Lemma process_eval_rec5_loss_draw_win ht (res : estate) l : Hiv l -> ht_valid ht -> \smin_(i <- l) f1 i = win -> drawwin <= res -> process_eval_rec5 f2 eloss edraw ht res l <= lossdraw.
proof: Proof. elim: l ht res => [|i l IH] ht res HHiv Hv. by rewrite big_nil /= (esflip_le _ drawwin). rewrite big_cons [process_eval_rec5 _ _ _ _ _ _]/= => H1 H2. 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 [H3 H4] : f1 i = win /\ \smin_(j <- l) f1 j = win. have [E1|/ltnW E1] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite smin_lel // in H1 *; split => //. by apply: ge_winE; rewrite -{1}H1. rewrite smin_ler // in H1 *; split => //. by apply: ge_winE; rewrite -{1}H1. have [E1|E1] := leqP res (f2 _ _ _ _). by apply: IH => //; apply: (H5loss_draw_table HHiv). have [E2|E2] := leqP _ (f2 _ _ _ _). apply: IH => //; first by apply: (H5loss_draw_table HHiv). by apply: (H5loss_draw_win HHiv). rewrite ifN. rewrite ltnNge in E2; case/negP: E2. by apply: leq_trans (H5loss_draw_win HHiv _ _). rewrite -ltnNge. by apply: leq_trans (H5loss_draw_win HHiv _ _). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)