proposition: Lemma Ind_bigcup_incl_excl (n : nat) (S : 'I_n -> {set A}) (x : A) : Ind (\bigcup_(i < n) S i) x = (\sum_(1 <= k < n.+1) (-1) ^ (k - 1) * SumIndCap S k x).
proof: Proof. case: n S => [|n] S; first by rewrite big_ord0 big_geq // Ind_set0. set Efull := \bigcup_(i < n.+1) S i. have Halg : \prod_(i < n.+1) (Ind Efull x - Ind (S i) x) = 0. case Ex : (x \in Efull); last first. { have /Ind_notinP Ex0 := Ex. erewrite eq_bigr. 2: by rewrite Ex0. have Ex00 : forall i : 'I_n.+1, Ind (S i) x = 0. move=> i; apply/Ind_notinP. by move/negbT: Ex; rewrite -!in_setC setC_bigcup; move/bigcapP; apply. erewrite eq_bigr. 2: by move=> i _; rewrite Ex00. rewrite subR0. by apply/prodR_eq0; exists ord0. } { rewrite /Efull in Ex. have /bigcupP [i Hi Hi0] := Ex. apply/prodR_eq0; exists i =>//. by rewrite /Efull (Ind_inP _ _ Ex) (Ind_inP _ _ Hi0) subRR. } rewrite bigA_distr in Halg. do [erewrite eq_bigr; last by move=> k _; erewrite eq_bigr; last by move=> J _; rewrite bigID2] in Halg. rewrite big_ltn //= in Halg. rewrite -> addR_eq0 in Halg. rewrite cardT size_enum_ord (big_pred1 set0) in Halg; last first. by move=> i; rewrite pred1E [RHS]eq_sym; apply: cards_eq0. rewrite [in X in _ * X = _]big_pred0 in Halg; last by move=> i; rewrite inE. do [erewrite eq_bigl; last by move=> j; rewrite !inE /negb /= ] in Halg. rewrite mulR1 -Ind_bigcap big_const_ord iterSr iter_fix setIT ?setIid // in Halg. rewrite {}Halg big_morph_oppR big_nat [RHS]big_nat. apply: eq_bigr => i Hi; rewrite /SumIndCap /Efull. rewrite m1powD; last first. by case/andP: Hi => Hi _ K0; rewrite K0 in Hi. rewrite mulNR. rewrite [in RHS](big_morph _ (morph_mulRDr _) (mulR0 _)). congr Ropp; apply: eq_bigr => j Hj. rewrite prodRN (eqP Hj). rewrite (_ : ?[a] * ((-1)^i * ?[b]) = (-1)^i * (?a * ?b)); last by ring. congr Rmult. have [Hlt|Hn1] := ltnP i n.+1; last first. { rewrite big1; last first. { move=> k Hk; rewrite inE in Hk. rewrite (_: j = [set: 'I_n.+1]) ?inE // in Hk. apply/setP/subset_cardP =>//. rewrite (eqP Hj) cardsT /= card_ord. by apply/anti_leq/andP; split; first by case/andP: Hi =>//. } by rewrite mul1R Ind_bigcap. } rewrite -!Ind_bigcap big_const. rewrite cardsCs card_ord setCK (eqP Hj). have [m ->] : exists m, (n.+1 - i)%nat = m.+1. by exists (n.+1 - i).-1; rewrite prednK // subn_gt0. rewrite iterSr iter_fix ?setIT ?setIid //. rewrite -Ind_cap -/Efull. suff : \bigcap_(j0 in j) S j0 \subset Efull by move/setIidPr->. rewrite /Efull. pose i0 := odflt ord0 (pick (mem j)). have Hi0 : i0 \in j. { rewrite /i0; case: pickP =>//. move=> /pred0P K; exfalso. rewrite /pred0b (eqP Hj) in K. by rewrite (eqP K) /= in Hi. } apply: (subset_trans (bigcap_inf i0 Hi0)). exact: (bigcup_sup i0). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct reals) Reals Lra ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist