proposition: Theorem G1_G2_close : | Pr[G1] - Pr[G2] | <= (q / 1) * k.
proof: Proof. rewrite G1_eq_Gi_q. rewrite G2_eq_Gi_0. rewrite ratDistance_comm. specialize (distance_le_prod_f (fun i => Pr[Gi i])); intuition. Qed.
imports: FCF.FCF FCF.RndInList