proposition: Theorem PRF_DRBG_Adv_small : DRBG_Advantage RndKey RndOut PRF_DRBG A <= PRF_Advantage RndKey ({ 0 , 1 }^eta) f D_EqDec (Bvector_EqDec eta) PRF_A + l ^ 2 / 2 ^ eta.
proof: Proof. intuition. unfold DRBG_Advantage. rewrite PRF_DRBG_G1_equiv. rewrite PRF_DRBG_G1_G2_equiv. rewrite <- PRF_DRBG_G4_DRBG_equiv. eapply ratDistance_le_trans. apply PRF_DRBG_G2_G3_close. apply PRF_DRBG_G3_G4_close. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF