proposition: Lemma set_infty_eq0 (P : pred V) f x : (forall x, P x -> f x != 0) -> (set_infty P f x == 0) = (f x == 0).
proof: Proof. by move=> /(_ x); rewrite ffunE; case: P => // /(_ isT)/negPf->. Qed.
imports: mathcomp(all_ssreflect) bigmin extra