proposition: Lemma big_set1 a F : \big[op/idx]_(i in [set a]) F i = F a.
proof: Proof. by apply: big_pred1 => i; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)