proposition: Theorem RPS_G_1_2_close : | Pr[x <-$ RPS_G_1; ret fst x] - Pr[x <-$ RPS_G_2; ret fst x] | <= (A2_queries / 1) * badProb A2_queries.
proof: Proof. intuition. eapply leRat_trans. eapply fundamental_lemma_h. eapply RPS_G_1_2_bad_same. eapply RPG_G_1_2_eq_until_bad. eapply RPS_G_1_bad_small. Qed.
imports: FCF PRF RndInList