proposition: Theorem TrueSingle_impl_Mult : Pr[TrueMult_G] <= (n / 1) * Pr[TrueSingle_G].
proof: Proof. unfold TrueMult_G, TrueSingle_G. simpl in *. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply sumList_factor_constant_l. } eapply sumList_le. intuition. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. rewrite ratMult_comm. eapply ratMult_assoc. } eapply ratMult_leRat_compat. intuition. specialize (@compMap_Q_eq_compFold _ _ Q n (c a) false); intuition. rewrite H0. rewrite prob_sum_le_mult. rewrite ratMult_comm. eapply ratMult_leRat_compat; intuition. Local Transparent evalDist. simpl. reflexivity. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid