proposition: Lemma eval_recE n t b : eval_rec n t b = if ieval t b is some v then v else if n is n1.+1 then let t1 := flip t in sflip (\smin_(i <- moves t b) eval_rec n1 t1 i) else draw.
proof: Proof. by case: n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)