proposition: Lemma ge_process_eval_rec4 eval alpha beta res l : esflip res <= process_eval_rec4 eval alpha beta res l.
proof: Proof. elim: l alpha beta res => /= [_ _ res |i l IH alpha beta res] //. have [E1|E1] := leqP res _; first by apply: IH. have {}E1 : eval alpha beta i <= res by case: (eval _ _) E1; case: res. have [E2|E2] := leqP beta _. by apply: leq_trans (IH _ _ _); rewrite esflip_le. have [E3|E3] := leqP _ alpha. by case: (eval _ _) E1; case: res; case: (l). by apply: leq_trans (IH _ _ _); rewrite esflip_le. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)