proposition: Lemma preim_inter (T S : eqType) (e : U -> T) (g : U -> S) (A : T) (C : S) : finset (preim (fun x => (e x, g x)) (pred1 (A, C))) = finset (preim e (pred1 A)) :&: finset (preim g (pred1 C)).
proof: Proof. apply/setP => u; rewrite !inE. apply/andP => /=. by case: ifPn => [/andP | /negP H /andP /H]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba