proposition: Lemma process_eval_rec5_loss_win_valid ht (res : estate) l : Hiv l -> ht_valid ht -> ht_valid (process_eval_rec5 f2 eloss ewin ht res l).
proof: Proof. elim: l ht res => // i l IH ht res HHiv Hv. rewrite [process_eval_rec5 _ _ _ _ _ _]/=. 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. have [E1|E1] := leqP res (f2 _ _ _ _). by apply: IH => //; apply: (H5loss_win_table HHiv). have [E2|E2] := leqP ewin (f2 _ _ _ _). by apply: IH => //; apply: (H5loss_win_table HHiv). have [E3|E3] := leqP (f2 _ _ _ _) eloss. case: pres2state => //=; try by apply: (H5loss_win_table HHiv). by case: (l) => *; apply: (H5loss_win_table HHiv). rewrite (H5loss_win HHiv) // in E E1 E2 E3 *. have -> : f1 i = draw by case: f1 E2 E3. apply: process_eval_rec5_loss_draw_valid => //. by apply: (H5loss_win_table HHiv). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)