fact: Fixpoint 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 .
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)