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