proposition: Lemma le_eval t b1 b2 : b2 \in moves t b1 -> sflip (eval (flip t) b2) <= eval t b1.
proof: Proof. move=> b2I. rewrite [X in _ <= s2n X]evalE. case: ieval (liveness t b1) => [a /(@sym_equal _ _ _) /negbT| _]. by rewrite negbK => /eqP H; rewrite H in b2I. by lazy zeta; rewrite sflip_le le_bigsmin. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)