proposition: Theorem TrueRepeat_G2_bad_small : Pr[TrueRepeat_G3_bad] <= expRat failProb n.
proof: Proof. unfold TrueRepeat_G3_bad. comp_irr_l. rewrite prob_fold_and_eq_exp. eapply expRat_leRat_compat. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid