proposition: Theorem sumList_filter_complement : forall (A : Set){eqd : EqDec A}(c : Comp A)(a : A), well_formed_comp c -> sumList (filter (fun x => negb (eqb a x)) (getSupport c)) (evalDist c) == ratSubtract 1 (evalDist c a).
proof: Proof. intuition. eapply (eqRat_ratAdd_same_r (evalDist c a)). symmetry. rewrite ratAdd_comm. rewrite ratSubtract_ratAdd_inverse_2. rewrite <- (evalDist_lossless H). rewrite (sumList_filter_partition (eqb a)). rewrite ratAdd_comm. eapply ratAdd_eqRat_compat; intuition. destruct (eq_Rat_dec (evalDist c a) 0). rewrite e. eapply sumList_0; intuition. apply filter_In in H0. intuition. rewrite eqb_leibniz in H2; subst. trivial. rewrite (@sumList_exactly_one _ a); intuition. eapply filter_NoDup. eapply getSupport_NoDup. eapply filter_In; intuition. eapply getSupport_In_evalDist; intuition. eapply eqb_refl. apply filter_In in H0; intuition. rewrite eqb_leibniz in H3; subst. intuition. eapply evalDist_le_1. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1