proposition: Lemma fbig_pred1_inj (I : choiceType) (T : eqType) f (k : I -> T) (d : {fset I}) i : i \in d -> injective k -> \big[op/idx]_(j <- d | k j == k i) f j = f i.
proof: Proof. move=> di kinj. rewrite big_fset_condE -(big_seq_fset1 op); apply eq_fbig => // j. rewrite !inE /=; apply/idP/idP => [|/eqP ->]; last by rewrite eqxx andbT. by case/andP => _ /eqP /kinj ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)