proposition: Lemma process_eval_rec1_correct f res l l1 : res = \smin_(i <- l1) f i -> process_eval_rec1 f res l = sflip (\smin_(i <- l ++ l1) f i).
proof: Proof. elim: l l1 res => /= [|i l IH] l1 res resE; first by rewrite resE. have /IH-> : smin (f i) res = \smin_(i <- (i :: l1)) f i. by rewrite big_cons //= -resE. rewrite !(big_cat, big_cons) /=. by rewrite sminC -!sminA [X in smin _ X]sminC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)