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