proposition: Theorem Prob_or_indep_le : forall (c1 c2 : Comp bool), Pr[b1 <-$ c1; b2 <-$ c2; ret (b1 || b2)] <= Pr[c1] + Pr[c2].
proof: Proof. intuition. rewrite bool_Comp_seq. eapply ratAdd_leRat_compat. eapply leRat_trans. eapply ratMult_leRat_compat. eapply leRat_refl. eapply evalDist_le_1. eapply eqRat_impl_leRat. eapply ratMult_1_r. eapply leRat_trans. eapply ratMult_leRat_compat. eapply evalDist_le_1. eapply leRat_refl. rewrite ratMult_1_l. unfold orb. rewrite evalDist_right_ident. intuition. Qed.
imports: FCF.FCF FCF.CompFold