proposition: Lemma big_prod_ord [R' : Type] [idx : R'] (op : Monoid.com_law idx) [m n : nat] (P : pred 'I_(m * n)) (F : 'I_(m * n) -> R') : \big[op/idx]_(i | P i) F i = \big[op/idx]_i \big[op/idx]_(j | P (unsplit_prod (i, j))) F (unsplit_prod (i, j)).
proof: Proof. elim: m =>[|m IHm] in P F *; first by rewrite 2!big_ord0. rewrite big_ord_recl big_split_ord; congr (op _ _). - apply congr_big => //=. by move=> i/=; congr P; exact: val_inj. by move=> i/= _; congr F; exact: val_inj. - rewrite IHm; apply eq_bigr => i _. have e j : rshift n (unsplit_prod (i, j)) = Ordinal (unsplit_prodp (lift ord0 i) j). by apply val_inj => /=; rewrite /bump leq0n addnA. by apply: eq_big => // j; rewrite e. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist