proposition: Lemma xchange : forall (T : Type) (idx : T) (op : Monoid.com_law idx) (m n : nat) (F : nat -> nat -> T), \big[op/idx]_(m <= i < n) (\big[op/idx]_(m <= j < i.+1) F i j) = \big[op/idx]_(m <= h < n) \big[op/idx]_(h <= j < n) (F j h).
proof: Proof. move=> T idx op m n F. elim : n => [ | n Hn ]. case : (leqP 0 m)=> Hm0 //. by rewrite !big_geq. case : (ltnP n m) => Hmn. by rewrite !big_geq. rewrite (big_cat_nat op (n:=n)) // big_nat1 Hn [x in (op _ x = _)](big_cat_nat op (n:=n)) // big_nat1 [x in (op _ _ = x)](big_cat_nat op (n:=n)) // big_nat1 big_nat1 (Monoid.mulmA op). congr (op _ _). rewrite -big_split big_nat [x in (_ = x)]big_nat. apply: eq_bigr => i Hi. rewrite [x in (_ = x)](big_cat_nat op (n:=n)) // ?big_nat1 // ltnW//. by case/andP: Hi=> _ ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)