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