proposition: Lemma eval_loss t b1 : ieval t b1 = None -> (forall b, b \in moves t b1 -> eval (flip t) b = win) -> eval t b1 = loss.
proof: Proof. rewrite evalE => ->. elim: moves => /= [|b2 bs IH H]; first by rewrite big_nil. rewrite big_cons sflip_min H ?IH ?in_cons ?eqxx // => b Hb. by rewrite H // in_cons Hb orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)