proposition: Lemma eval_win t b1 b2 : b2 \in moves t b1 -> eval (flip t) b2 = loss -> eval t b1 = win.
proof: Proof. move=> b2I H2; rewrite evalE; case: ieval (liveness t b1) => [v|_]. move/(@sym_equal _ _ _)=> /negbT; rewrite negbK => /eqP H. by rewrite H in b2I. elim: moves b2I => //= b3 bs IH. rewrite big_cons sflip_min in_cons => /orP[/eqP<-|/IH->]. by rewrite H2 smaxwn. by rewrite smaxnw. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)