proposition: Lemma process_eval_rec5_loss_draw_valid ht (res : estate) l : Hiv l -> ht_valid ht -> ht_valid (process_eval_rec5 f2 eloss edraw ht res l).
proof: Proof. elim: l ht res => // i l IH ht res HHiv Hv. have HHiv1 := Hiv_cons HHiv. rewrite [process_eval_rec5 _ _ _ _ _ _]/=. case E : f2 => [ht1 res1]. have -> : res1 = f2 eloss edraw ht i by rewrite E. have -> : ht1 = f2 eloss edraw ht i by rewrite E. have [E1|E1] := leqP res (f2 _ _ _ _). by apply: IH => //; apply: (H5loss_draw_table HHiv). have [E2|E2] := leqP edraw (f2 _ _ _ _). by apply: IH => //; apply: (H5loss_draw_table HHiv). have [E3|E3] := leqP (f2 _ _ _ _) eloss. case: pres2state => //=; try by apply: (H5loss_draw_table HHiv). by case: (l) => *; apply: (H5loss_draw_table HHiv). case E4 : (f1 i). - rewrite ltnNge in E2; case/negP: E2. by apply: leq_trans (H5loss_draw_win HHiv Hv E4). - by rewrite (H5loss_draw_loss HHiv) // ltnn in E3. rewrite ltnNge in E2; case/negP: E2. by have /andP[] := H5loss_draw_draw HHiv Hv E4. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)