proposition: Lemma process_eval_rec4_draw_win_win (res : estate) l : res = win -> \smin_(i <- l) f1 i = win -> process_eval_rec4 f2 edraw ewin res l = eloss.
proof: Proof. elim: l res => [|i l IH] res; first by rewrite big_nil => ->. rewrite big_cons [process_eval_rec4 _ _ _ _ _]/= => H1 H2. 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 H2; split => //. by apply: ge_winE; rewrite -{1}H2. rewrite smin_ler // in H2; split => //. by apply: ge_winE; rewrite -{1}H2. rewrite H4draw_win_win // H1 /=. by apply: IH. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)