proposition: Lemma bigop_simpl1 (n m : nat) (F : nat -> R): (forall j, (m <= j)%N -> F j = idx) -> \big[op/idx]_(j < n) F j = \big[op/idx]_(j < m | (j < n)%N) F j.
proof: Proof. set s := (n + m)%N => h. rewrite (big_ord_widen s F (leq_addr m n)). rewrite (big_ord_widen_cond s (fun j => (j < n)%N) F (leq_addl n m)). rewrite (bigID (fun i0:ordinal s => (i0 < m)%N) _ F) /=. rewrite [X in op _ X] big1 ? Monoid.mulm1 //. by move => j; rewrite -leqNgt; case/andP => _; by apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)