proposition: Lemma process_eval_rec5_draw_win_draw ht (res : estate) l : Hiv l -> ht_valid ht -> \smin_(i <- l) f1 i = draw -> lossdraw <= res -> edraw <= process_eval_rec5 f2 edraw ewin ht res l <= drawwin.
proof: Proof. move=> HHiv Hv H1 H2. rewrite process_eval_rec5_draw_win_ge ?H1 //. by rewrite process_eval_rec5_draw_win_le ?H1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)