proposition: Theorem in_support_marginal_l : forall (A B : Set){eqd: EqDec A}(c1 : Comp (A * B))(c2 : Comp A), (forall a, evalDist c2 a == marginal_l c1 a) -> forall p, In p (getSupport c1) -> In (fst p) (getSupport c2).
proof: Proof. intuition. eapply getSupport_In_evalDist. intuition. rewrite H in H1. clear H. unfold marginal_l in *. simpl in *. eapply sumList_0 in H1; eauto. eapply ratMult_0 in H1. intuition. eapply getSupport_In_evalDist; eauto. dist_compute. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1