proposition: Theorem PRF_DRBG_G3_bad_4_small : Pr[PRF_DRBG_G3_bad_4] <= (l ^ 2 / 2 ^ eta).
proof: Proof. unfold PRF_DRBG_G3_bad_4. rewrite dupProb_const. destruct l. lia. simpl. rewrite forNats_length. rewrite Nat.mul_1_r. reflexivity. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF