proposition: Lemma Ind_bigcap I (e : I -> {set A}) (r : seq.seq I) (p : pred I) x : Ind (\bigcap_(j <- r | p j) e j) x = \prod_(j <- r | p j) (Ind (e j) x).
proof: Proof. apply (big_ind2 (R1 := {set A}) (R2 := R)); last by []. - by rewrite /Ind inE. - by move=> sa a sb b Ha Hb; rewrite -Ha -Hb; apply: Ind_cap. 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