proposition: Theorem prob_sum_le_mult : forall (n : nat)(c : Comp bool), Pr [compFold _ (fun b a => x <-$ c; ret (b || x)) false (forNats n)] <= n/1 * Pr [c].
proof: Proof. intuition. rewrite prob_sum_le. eapply leRat_trans. eapply eqRat_impl_leRat. eapply sumList_body_eq. intuition. symmetry. eapply ratMult_1_r. rewrite sumList_factor_constant_l. rewrite ratMult_comm. eapply ratMult_leRat_compat; intuition. rewrite sumList_1_mult. rewrite forNats_length. intuition. Qed.
imports: FCF.FCF Permutation