proposition: Lemma big_ord1_eq (F : nat -> R) i n : \big[op/idx]_(j < n | j == i :> nat) F j = if i < n then F i else idx.
proof: Proof. case: ltnP => [i_lt|i_ge]; first by rewrite (big_pred1_eq (Ordinal _)). by rewrite big_pred0// => j; apply: contra_leqF i_ge => /eqP <-. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)