proposition: Lemma big_rcons T R idx (op : Monoid.law idx) i r (P : pred T) (F : T -> R) : let x := \big[op/idx]_(j <- r | P j) F j in \big[op/idx]_(j <- rcons r i | P j) F j = if P i then op x (F i) else x.
proof: Proof. rewrite -cats1 big_cat /= [in X in op _ X]big_mkcond big_seq1. by case: ifP=> //; rewrite Monoid.mulm1. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)