proposition: Lemma process_eval_rec3_correct_a res (beta : state) l : alpha < beta -> \smin_(i <- l) f1 i <= alpha -> sflip alpha <= process_eval_rec3 f2 alpha beta res l.
proof: Proof. elim: l res beta => [|i l IH] res beta aLb. by rewrite big_nil // => /ge_winE->; apply: ge_loss. rewrite big_cons /= => H. have [E1|E1] := leqP res (f2 _ _ _). have [E2|E2] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite smin_lel // in H. apply: leq_trans (ge_process_eval_rec3 _ _ _ _ _) => //. rewrite sflip_le. by apply: leq_trans E1 (f1Ha _); rewrite H. rewrite smin_ler in H; last by apply: ltnW. by apply: IH. have [E2|E2] := leqP beta (f2 _ _ _). have [E3|E3] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite smin_lel // in H. apply: leq_trans (ge_process_eval_rec3 _ _ _ _ _) => //. rewrite sflip_le. by apply: f1Ha; rewrite H. rewrite smin_ler in H; last by apply: ltnW. by apply: IH. have [E3|E3] := leqP (f2 _ _ _) alpha; first by rewrite sflip_le. apply: IH => //. have [E4|/ltnW E4] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite ltnNge in E3; case/negP: E3. apply: f1Ha; rewrite aLb andbT. by move: H; rewrite smin_lel. by move: H; rewrite smin_ler. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)