proposition: Lemma eval_rec1_correct n t b : eval_rec1 n t b = eval_rec n t b.
proof: Proof. elim: n t b => //= n IH t b. case: ieval => //. rewrite -{2}[moves t b]cats0. have H : win= \smin_(i <- [::]) eval_rec n (flip t) i by rewrite big_nil. rewrite {1}H. elim: (moves t b) [::]=> //= i l1 IH1 l2. have := IH1 (i :: l2). rewrite IH big_cons // => ->; congr sflip. by rewrite !(big_cat, big_cons) /= sminC -sminA [X in smin _ X = _]sminC sminA. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)