proposition: Theorem DRBG_P_secure : | Pr[DRBG_P DRBG_GA] - Pr[DRBG_P DRBG_GB] | <= xLogAdvantage + @DDH_Advantage _ groupOp ident inverse _ g order A.
proof: Proof. eapply leRat_trans. eapply ratTriangleInequality. eapply ratAdd_leRat_compat. eapply eqRat_impl_leRat. eapply eqRat_refl. eapply eqRat_impl_leRat. eapply DRBG_P_DH. Qed.
imports: FCF DiffieHellman RndNat