proposition: Lemma big_seq_fset1 (a : I) (F : I -> R) : \big[op/idx]_(i <- [fset a]) F i = F a.
proof: Proof. by rewrite big_seq_fsetE big_fset1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)