proposition: Lemma process_eval_rec4_draw_win_draw (res : estate) l : \smin_(i <- l) f1 i = draw -> lossdraw <= res -> edraw <= process_eval_rec4 f2 edraw ewin res l <= drawwin.
proof: Proof. move=> H1 H2. rewrite process_eval_rec4_draw_win_ge ?H1 //. by rewrite process_eval_rec4_draw_win_le ?H1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)