proposition: Lemma leq_bigmin (A : finType) (C : {set A}) (cnot0 : {c0 | c0 \in C}) a (Ha : a \in C) (h : A -> nat) : (\min^ (sval cnot0) _(c in C) h c <= h a)%nat.
proof: Proof. by case: arg_minnP; [case: cnot0|move=> a0 a0C; exact]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)