proposition: Lemma ge_process_eval_rec3 eval alpha beta res l : sflip res <= process_eval_rec3 eval alpha beta res l.
proof: Proof. elim: l alpha beta res => /= [_ _ res |i l IH alpha beta res]. by apply: leqnn. 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 _. apply: leq_trans (IH _ _ _). by rewrite sflip_le. have [E3|E3] := leqP _ alpha; first by case: (eval _ _) E1; case: res. apply: leq_trans (IH _ _ _). by rewrite sflip_le. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)