proposition: Lemma exchange_big_dep_nat : forall m1 n1 m2 n2 (P : pred nat) (Q : rel nat) (xQ : pred nat) F, (forall i j, m1 <= i < n1 -> m2 <= j < n2 -> P i -> Q i j -> xQ j) -> \big[*%M/1]_(m1 <= i < n1 | P i) \big[*%M/1]_(m2 <= j < n2 | Q i j) F i j === \big[*%M/1]_(m2 <= j < n2 | xQ j) \big[*%M/1]_(m1 <= i < n1 | P i && Q i j) F i j.
proof: Proof. move=> m1 n1 m2 n2 P Q xQ F PQxQ. transitivity (\big[*%M/1]_(i < n1 - m1| P (i + m1)) \big[*%M/1]_(j < n2 - m2 | Q (i + m1) (j + m2)) F (i + m1) (j + m2)). - rewrite -{1}[m1]add0n; rewrite -> big_addn; rewrite -> big_mkord; apply eq_bigr=> i _. by rewrite -{1}[m2]add0n; rewrite -> big_addn; rewrite -> big_mkord; reflexivity. rewrite -> (exchange_big_dep (I:=ordinal_finType (n1 - m1)) (J:=ordinal_finType (n2 - m2)) (P:=fun i => P (i + m1)) (Q:=fun i j => Q (i + m1) (j + m2)) (xQ:=fun j: 'I__ => xQ (j + m2)))=> [|i j]; last first. by apply: PQxQ; rewrite leq_addl addnC -subn_gt0 -subn_sub subn_gt0 ltn_ord. symmetry; rewrite -{1}[m2]add0n; rewrite -> big_addn; rewrite -> big_mkord; apply eq_bigr=> j _. by rewrite -{1}[m1]add0n; rewrite -> big_addn; rewrite -> big_mkord; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops