proposition: Lemma bigop_trivIseq (S : seq {set T}) F : all (fun s => s != set0) S -> trivIseq S -> \big[op/idx]_(i in [set x in S]) F i = \big[op/idx]_(i <- S) F i.
proof: Proof. Proof using. elim: S => [// _| S0 S IHS] /=. - rewrite set_nil big_nil big_pred0 //=. by move => i /=; rewrite in_set0. - move/andP => [HS0 Hall]; rewrite /trivIseq => Htriv. rewrite set_cons big_cons big_setU1. + by rewrite (IHS Hall (trivIseq_consK Htriv)). + move: HS0 => /set0Pn [x Hx]. rewrite negbT //=; apply/negP. rewrite inE => HS; have:= HS; rewrite -index_mem => HS1. set j := index S0 S; have H : 0 < j.+1 < size (S0 :: S) by []. move/(_ 0 j.+1 H): Htriv. rewrite /= /j nth_index //= -setI_eq0 => /eqP; apply/setP => HH. by move/(_ x): HH; rewrite !inE Hx. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast