proposition: Lemma process_eval_rec4_loss_draw_ge (res : estate) l : \smin_(i <- l) f1 i <= draw -> lossdraw <= process_eval_rec4 f2 eloss edraw res l.
proof: Proof. elim: l res => [|i l IH] res; first by rewrite big_nil. rewrite big_cons [process_eval_rec4 _ _ _ _ _]/= => H. have [E1|E1] := leqP res (f2 _ _ _). have [E2|/ltnW E2] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite smin_lel // in H. apply: leq_trans (ge_process_eval_rec4 _ _ _ _ _). rewrite (esflip_le drawwin). by apply: leq_trans E1 (H4loss_draw_le _). rewrite smin_ler // in H. by apply: IH. have [E2|E2] := leqP edraw (f2 _ _ _). have [E3|/ltnW E3] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite smin_lel // in H. apply: leq_trans (ge_process_eval_rec4 _ _ _ _ _). rewrite (esflip_le drawwin). by apply: leq_trans _ (H4loss_draw_le _). rewrite smin_ler // in H. by apply: IH. have [E3|E3] := leqP (f2 eloss edraw i) eloss. by rewrite (le_elossE E3). apply: leq_trans (ge_process_eval_rec4 _ _ _ _ _). rewrite (esflip_le drawwin). by apply: leq_trans (ltnW E2) _. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)