proposition: Theorem evalDist_le_1_gen : forall (A : Set)(eqd : EqDec A)(c : Comp A)(ls : list A), NoDup ls -> sumList ls (evalDist c) <= 1.
proof: Proof. intuition. eapply leRat_trans. eapply eqRat_impl_leRat. eapply (sumList_filter_partition (fun a => if (in_dec (EqDec_dec _) a (getSupport c)) then true else false)). eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply ratAdd_0_r. } eapply ratAdd_leRat_compat. eapply leRat_trans. eapply sumList_subset_le. intuition. eapply filter_NoDup. trivial. eapply (getSupport_NoDup c). intuition. eapply filter_In in H0. intuition. destruct (in_dec (EqDec_dec eqd) a (getSupport c)); intuition. discriminate. eapply evalDist_sum_le_1. eapply eqRat_impl_leRat. eapply sumList_0. intuition. eapply filter_In in H0. intuition. destruct (in_dec (EqDec_dec eqd) a (getSupport c)). simpl in *. discriminate. eapply getSupport_not_In_evalDist. trivial. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec