proposition: Theorem TwoWorlds_equiv_b : negligible (fun eta => | Pr[StandardDef_G eta] - 1 / 2 |) -> negligible (fun eta => (| Pr[f eta false] - Pr[f eta true] |)).
proof: Proof. unfold negligible. intuition. edestruct (H (1 + c)%nat). exists (S x)%nat. intuition. eapply H0. lia. assert ((RatIntro (S O) (@natToPosnat (expnat x0 (plus (S O) c)) (@expnat_nz (plus (S O) c) x0 pf_nz))) == (1 / x0) * (1 / (expnat x0 c))). simpl. rewrite <- ratMult_denom. eapply eqRat_terms; intuition. rewrite H3. clear H3. rewrite H2. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply Def_equiv_2W. } eapply ratMult_leRat_compat; intuition. unfold leRat. eapply leRat_terms; intuition. unfold natToPosnat, posnatToNat. lia. Qed.
imports: FCF.FCF FCF.Crypto FCF.Asymptotic