proposition: Lemma big_fset0_cond (P : pred _) (F : _ -> R) : \big[op/idx]_(i : @fset0 I | P i) F i = idx :> R.
proof: Proof. by apply: big_pred0 => -[j hj]; have := hj; rewrite in_fset0. Qed.
imports: mathcomp(all_ssreflect all_algebra)