proposition: Lemma telescope_big (f : nat -> nat -> R) (n m : nat) : (forall k, n < k < m -> op (f n k) (f k k.+1) = f n k.+1) -> \big[op/idx]_(n <= i < m) f i i.+1 = if n < m then f n m else idx.
proof: Proof. elim: m => [//| m IHm]; first by rewrite ltn0 big_geq. move=> tm; rewrite ltnS; case: ltnP=> // mn; first by rewrite big_geq. rewrite big_nat_recr// IHm//; last first. by move=> k /andP[nk /ltnW nm]; rewrite tm// nk. by case: ltngtP mn=> //= [nm|<-]; rewrite ?mul1m// tm// nm leqnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)