proposition: Theorem sumList_support_bool : forall (c : Comp bool), sumList (getSupport c) (evalDist c) == evalDist c true + evalDist c false.
proof: Proof. intuition. rewrite (sumList_filter_partition (eqb true)). eapply ratAdd_eqRat_compat. destruct (eq_Rat_dec (Pr[c]) 0). rewrite e. eapply sumList_0. intuition. apply filter_In in H. intuition. rewrite eqb_leibniz in H1. subst. trivial. eapply sumList_exactly_one. eapply filter_NoDup. eapply getSupport_NoDup. eapply filter_In. intuition. eapply getSupport_In_evalDist. intuition. eapply eqb_leibniz. trivial. intuition. eapply filter_In in H. intuition. rewrite eqb_leibniz in H2. subst. intuition. destruct (eq_Rat_dec (evalDist c false) 0). rewrite e. eapply sumList_0. intuition. eapply filter_In in H. intuition. destruct a. rewrite eqb_refl in H1. simpl in *. discriminate. trivial. eapply sumList_exactly_one. eapply filter_NoDup. eapply getSupport_NoDup. eapply filter_In. intuition. eapply getSupport_In_evalDist. intuition. case_eq (eqb true false); intuition. rewrite eqb_leibniz in H. discriminate. intuition. eapply filter_In in H. intuition. destruct b. rewrite eqb_refl in H2. simpl in *. discriminate. intuition. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec