proposition: Lemma big_rcons (R : Type) (idx : R) (op : Monoid.law idx) (I : Type) i r (P : pred I) F : \big[op/idx]_(j <- rcons r i | P j) F j = op (\big[op/idx]_(j <- r | P j) F j) (if P i then F i else idx).
proof: Proof. by rewrite big_rcons_idx -big_change_idx Monoid.mulm1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)