proposition: Lemma evalDist_le_1 : forall (A : Set)(c : Comp A) a, evalDist c a <= 1.
proof: Proof. intuition. eapply leRat_trans. 2:{ eapply (@evalDist_sum_le_1 _ c). } pose proof (comp_EqDec c). destruct (in_dec (EqDec_dec _) a (getSupport c)). eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. rewrite (sumList_partition (eqb a)). eapply ratAdd_eqRat_compat. eapply sumList_exactly_one. eapply getSupport_NoDup. eauto. intuition. case_eq (eqb a b); intuition. exfalso. eapply H1. eapply eqb_leibniz. trivial. eapply ratMult_0_r. eapply eqRat_refl. } eapply leRat_trans. eapply eqRat_impl_leRat. eapply ratAdd_0_r. eapply ratAdd_leRat_compat. rewrite eqb_refl. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply ratMult_1_r. } intuition. eapply rat0_le_all. apply getSupport_not_In_evalDist in n. rewrite n. eapply rat0_le_all. Qed.
imports: FCF.Comp FCF.Rat FCF.Fold List FCF.Blist micromega.Lia FCF.StdNat FCF.NotationV1 FCF.EqDec