proposition: Lemma big_rcons_idx (R : Type) (idx : R) (op : R -> R -> R) (I : Type) (i : I) (r : seq I) (P : pred I) (F : I -> R) (idx' := if P i then op (F i) idx else idx) : \big[op/idx]_(j <- rcons r i | P j) F j = \big[op/idx']_(j <- r | P j) F j.
proof: Proof. by elim: r => /= [|j r]; rewrite ?(big_nil, big_cons)// => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)