proposition: Theorem in_support_marginal_r : forall (A B : Set){eqd: EqDec B}(c1 : Comp (A * B))(c2 : Comp B), (forall b, evalDist c2 b == marginal_r c1 b) -> forall p, In p (getSupport c1) -> In (snd p) (getSupport c2).
proof: Proof. intuition. eapply getSupport_In_evalDist. intuition. rewrite H in H1. clear H. unfold marginal_r 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