proposition: Lemma cinde_rv_events : cinde_rv <-> (forall x y z, cinde_events P (finset (X @^-1 x)) (finset (Y @^-1 y)) (finset (Z @^-1 z))).
proof: Proof. split=> [H /= x y z|/= H x y z]. - rewrite /cinde_events -2!cpr_eqE' -H cpr_eqE'; congr cPr. by apply/setP => /= ab; rewrite !inE. - rewrite (cpr_eqE' _ x) (cpr_eqE' _ y) -H cpr_eqE'; congr cPr. by apply/setP => /= ab; rewrite !inE. 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