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