proposition: Lemma process_eval_rec5_loss_win ht (res : estate) l : Hiv l -> ht_valid ht -> \smin_(i <- l) f1 i <= res -> process_eval_rec5 f2 eloss ewin ht res l = sflip (\smin_(i <- l) f1 i) :> estate.
proof: Proof. elim: l ht res => [|i l IH] ht res HHiv Hv. by rewrite big_nil /= => /ge_ewinE ->. rewrite big_cons [process_eval_rec5 _ _ _ _ _ _]/= => H. case E : f2 => [ht1 res1]. have -> : res1 = f2 eloss ewin ht i by rewrite E. have -> : ht1 = f2 eloss ewin ht i by rewrite E. have HHiv1 := Hiv_cons HHiv. rewrite (H5loss_win HHiv) // !es2ns2esK. have [E1|E1] := leqP res (f1 i). have [E2|E2] := leqP (\smin_(j <- l) f1 j) (f1 i). rewrite smin_ler // in H *. by apply: IH => //; apply: (H5loss_win_table HHiv). rewrite smin_lel // in H *; last by apply: ltnW. apply: esle_antisym; last first. apply: leq_trans (ge_process_eval_rec5 _ _ _ _ _ _). by rewrite es2ns2esK es2n_flip esflip_le es2ns2esK. rewrite es2ns2esK es2n_flip. apply: process_eval_rec5_loss_win_lt; rewrite ?es2ns2esK //. by apply: (H5loss_win_table HHiv). rewrite ifN; last first. by rewrite -leqNgt -ltnS (leq_trans E1) // le_ewin. have [E2|E2] := leqP (f1 i) loss. by rewrite (le_lossE E2) /= sminln. have H3 : f1 i = draw. apply: sle_antisym. by case: f1 E1; case: (res). by case: f1 E2. rewrite H3 in H E1 *. have [E3|E3] := leqP draw (\smin_(j <- l) f1 j). rewrite smin_lel // in H *. apply: esle_antisym; rewrite es2ns2esK es2n_flip. apply: process_eval_rec5_loss_draw_le => //. by apply: (H5loss_win_table HHiv). by apply: ge_process_eval_rec5. suff H4 : \smin_(j <- l) f1 j = loss. rewrite H4. apply: process_eval_rec5_loss_draw_loss => //. by apply: (H5loss_win_table HHiv). apply: sle_antisym. by case: (\smin_(_ <- _) _) E3. by apply: ge_loss. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)