proposition: Lemma big_nat1_cond_eq (F : nat -> R) (P : pred nat) i m n : \big[op/idx]_(m <= j < n | P j && (j == i)) F j = if (m <= i < n) && P i then F i else idx.
proof: Proof. by rewrite big_mkcondl big_nat1_eq -if_and. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)