proposition: Theorem distro_irr_le : forall (A B : Set) (c : Comp A) (f : A -> Comp B) (y : B) (v : Rat), (forall x : A, In x (getSupport c) -> (evalDist (f x) y) <= v) -> (evalDist (x <-$ c; f x) y) <= v.
proof: Proof. intuition. simpl. rewrite sumList_le. 2:{ intuition. rewrite H at 1. eapply leRat_refl. trivial. } rewrite sumList_factor_constant_r. eapply leRat_trans. eapply ratMult_leRat_compat. eapply evalDist_sum_le_1. eapply leRat_refl. rewrite ratMult_1_l. intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms