proposition: Lemma bigsmin_ex (A : eqType) (f : A -> _) l : l != nil -> exists2 c, c \in l & \smin_(i <- l) f i = f c.
proof: Proof. elim: l => // a [ _ _|b l /(_ isT) [c H1c H2c] _]. exists a; first by rewrite in_cons eqxx. by rewrite big_cons big_nil; case: f. have [faE|] := f a =P \smin_(i <- [:: a, b & l]) f i. by exists a; rewrite // in_cons eqxx. rewrite big_cons H2c => faNE; exists c; first by rewrite in_cons H1c orbT. by case: (f a) faNE; case: (f c). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)