proposition: Lemma ge_process_eval_rec1 eval res l : sflip res <= process_eval_rec1 eval res l.
proof: Proof. elim: l res => /= [res|i l IH res]; first by apply: leqnn. apply: leq_trans (IH _). rewrite sflip_le. apply: ge_sminr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)