proposition: Theorem hybrid_incr_close : forall i, | Pr[G_hybrid i] - Pr[G_hybrid (S i)] | == DistSingle_Adv c1 c2 (B1 i) B2.
proof: Proof. intuition. unfold DistSingle_Adv. rewrite G_hybrid_DistSingle_eq. rewrite G_hybrid_DistSingle_S_eq. eapply ratDistance_comm. Qed.
imports: FCF.FCF FCF.CompFold