proposition: Theorem PRF_DRBG_G3_2_3_close : | Pr[x <-$ PRF_DRBG_G3_2; ret (fst x)] - Pr[x <-$ PRF_DRBG_G3_3; ret (fst x)] | <= Pr[x <-$ PRF_DRBG_G3_3; ret (snd x)].
proof: Proof. rewrite ratDistance_comm. fcf_fundamental_lemma. symmetry. apply PRF_DRBG_G3_2_3_badness_same. intuition. symmetry. apply PRF_DRBG_G3_2_3_eq_until_bad. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF