proposition: Lemma evalDist_Bind_1_le_l : forall (A B : Set) (b : Comp B) (a : B -> Comp A) (y : A) (v : Rat), well_formed_comp b -> (forall x : B, In x (getSupport b) -> evalDist (a x) y <= v) -> evalDist (x <-$ b; a x) y <= v.
proof: Proof. intuition. simpl. eapply leRat_trans. eapply sumList_le; intuition. eapply ratMult_leRat_compat. eapply leRat_refl. eapply H0. trivial. rewrite sumList_factor_constant_r. rewrite evalDist_lossless. rewrite ratMult_1_l. intuition. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia