From 77b73d6a6f2657e7fad648e9f01a48feda844a41 Mon Sep 17 00:00:00 2001
From: David Renshaw <dwrenshaw@gmail.com>
Date: Wed, 20 Nov 2024 15:40:10 -0500
Subject: [PATCH] [Usa1992P1] a bit shorter

---
 Compfiles/Usa1992P1.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Compfiles/Usa1992P1.lean b/Compfiles/Usa1992P1.lean
index 09207b7..5e34b7f 100644
--- a/Compfiles/Usa1992P1.lean
+++ b/Compfiles/Usa1992P1.lean
@@ -584,9 +584,7 @@ problem usa1992_p1 (n : ℕ) :
       have h47 : Even (10 ^ 2 ^ (n + 1) - 1 - b n) := Nat.Odd.sub_odd h45 (h9 n)
       rw [Nat.even_iff] at h47
       rw [Nat.odd_iff] at H1
-      rw [←Nat.not_odd_iff] at h47
-      rw [Nat.odd_iff] at h47
-      contradiction
+      simp [H1] at h47
     apply_fun (· + 1) at h12
     rw [←lemma3 h15] at h12
     have h17 : 10 ^ 2 ^ (n + 1) - 1 - b n + 1 = 10 ^ 2 ^ (n + 1) - b n := by omega