proposition: Lemma big_pred1_eqz m n F j: \big[op/idx]_(m <= i < n :> int | i == j) F i = if m <= j < n then F j else idx.
proof: Proof. case: ifP=> hj; last first. apply: big_hasC; apply/hasPn => k. by rewrite mem_index_iotaz => hk; move/negbT: hj; apply: contra; move/eqP<-. case/andP: hj => hmj hjn. rewrite (@big_cat_int _ _ _ _ _ hmj) /=; last by exact: ltW. rewrite big_hasC; last first. by apply/hasPn => k; rewrite mem_index_iotaz; case/andP=> _; apply: ltr_neq. rewrite Monoid.Theory.mul1m. rewrite big_ltz_cond // eqxx big_hasC; last first. apply/hasPn => k. rewrite mem_index_iotaz; case/andP=> hkj _. suff : j < k by rewrite lt_def eq_sym; case/andP. by apply: lt_le_trans hkj; rewrite cprD. by rewrite Monoid.Theory.mulm1. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp