proposition: Lemma le_bigsmax (A : eqType) (f : A -> state) c l : c \in l -> f c <= \smax_(i <- l) f i.
proof: Proof. elim: l => // a l IH; rewrite big_cons in_cons => /orP[/eqP<-| /IH /leq_trans H]. by case: (f) (\smax_(_ <- _) _) => // [] []. by apply: H; case: (f) (\smax_(_ <- _) _) => // [] []. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)