proposition: Theorem TwoWorlds_equiv_f : negligible (fun eta => (| Pr[f eta false] - Pr[f eta true] |)) -> negligible (fun eta => | Pr[StandardDef_G eta] - 1 / 2 |).
proof: Proof. unfold negligible. intuition. destruct (H c). exists x. intuition. eapply H0. intuition. rewrite H2. rewrite Def_equiv_2W. rewrite ratMult_comm. eapply ratMult_small_le. eapply rat_le_1. simpl. lia. Qed.
imports: FCF.FCF FCF.Crypto FCF.Asymptotic