proposition: Lemma big_set1E j F : \big[op/x]_(i in [set j]) F i = op (F j) x.
proof: Proof. by rewrite -big_pred1_eq_id; apply: eq_bigl => i; apply: in_set1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)