proposition: Lemma inde_rv_events : inde_rv <-> (forall x y, inde_events P (finset (X @^-1 x)) (finset (Y @^-1 y))).
proof: Proof. split => [/cinde_rv_unit/cinde_rv_events H a b|H]. exact/cinde_events_unit/(H _ _ tt). by apply/cinde_rv_unit/cinde_rv_events => a b []; exact/cinde_events_unit/H. 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