proposition: Lemma cinde_rv_unit : inde_rv <-> cinde_rv X Y (unit_RV P).
proof: Proof. split => [H a b []|H a b]; first by rewrite !cpr_eq_unit_RV H. by have := H a b tt; rewrite !cpr_eq_unit_RV. 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