proposition: Lemma shorten_sum (f: nat -> R) (n m : nat): (n <= m)%N -> (forall i, (n <= i < m)%N -> f i = idx) -> \big[op/idx]_(i < m) f i = \big[op/idx]_(i < n) f i.
proof: Proof. move => nm fz. rewrite - (big_mkord xpredT) (big_cat_nat _ _ _ (leq0n n) nm) /= big_mkord. rewrite [X in (op _ X)]big1_seq ? Monoid.mulm1 // => i; case /andP => _. by rewrite mem_index_iota; apply: fz. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)