proposition: Lemma big_change_idx (R : Type) (idx : R) (op : Monoid.law idx) (I : Type) (x : R) (r : seq I) (P : pred I) (F : I -> R) : op (\big[op/idx]_(j <- r | P j) F j) x = \big[op/x]_(j <- r | P j) F j.
proof: Proof. elim: r => [|i r]; rewrite ?(big_nil, big_cons, Monoid.mul1m)// => <-. by case: ifP => // Pi; rewrite Monoid.mulmA. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)