proposition: Theorem evalDist_orb_le : forall (A : Set)(c : Comp A) f1 f2, Pr [x <-$ c; ret (f1 x || f2 x)] <= Pr[ x <-$ c; ret (f1 x)] + Pr[x <-$ c; ret (f2 x)].
proof: Proof. intuition. simpl. rewrite (sumList_partition f1). eapply ratAdd_leRat_compat. eapply sumList_le. intuition. rewrite ratMult_assoc. eapply ratMult_leRat_compat; intuition. destruct (f1 a); simpl. rewrite ratMult_1_r. reflexivity. rewrite ratMult_0_r. eapply rat0_le_all. eapply sumList_le. intuition. rewrite ratMult_assoc. eapply ratMult_leRat_compat; intuition. destruct (f1 a); simpl. rewrite ratMult_0_r. eapply rat0_le_all. rewrite ratMult_1_r. reflexivity. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms