proposition: Theorem Single_impl_ListHybrid_sum : ListHybrid_Advantage <= sumList (forNats maxA) (fun i => DistSingle_Adv c1 c2 (B1 i) B2).
proof: Proof. unfold ListHybrid_Advantage. rewrite G_1_hybrid_eq. rewrite G_2_hybrid_eq. rewrite ratDistance_comm. rewrite (@ratDistance_sequence_sum (fun i => Pr[G_hybrid i])); intuition. eapply sumList_le. intuition. eapply eqRat_impl_leRat. eapply hybrid_incr_close. Qed.
imports: FCF.FCF FCF.CompFold