proposition: Lemma bigmin_eq_arg i0 (P : pred I) F : P i0 -> \min_(i | P i) F i = F [arg min_(i < i0 | P i) F i].
proof: Proof. move=> Pi0; case: arg_minnP => //= i Pi minFi. by apply/val_inj/eqP; rewrite eqn_leq geq_bigmin_cond //=; apply/bigmin_geqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect)