From 8255712e9fcf4884fc8743e3dd92eb1c590ac48a Mon Sep 17 00:00:00 2001
From: Archie <94995351+archiebrowne@users.noreply.github.com>
Date: Thu, 2 Nov 2023 20:17:20 +0000
Subject: [PATCH] new prime def is good

---
 Game/Levels/Prime/Level_1.lean | 28 ++++++++++++++++++----------
 1 file changed, 18 insertions(+), 10 deletions(-)

diff --git a/Game/Levels/Prime/Level_1.lean b/Game/Levels/Prime/Level_1.lean
index ebbd6af..2cf9281 100644
--- a/Game/Levels/Prime/Level_1.lean
+++ b/Game/Levels/Prime/Level_1.lean
@@ -1,4 +1,5 @@
 import Game.Levels.Multiplication
+import Game.Levels.AdvMultiplication.all_levels
 import Game.MyNat.Division
 import Game.MyNat.Prime
 
@@ -12,14 +13,22 @@ namespace MyNat
 
 Introduction
 "
-  In this level, we will prove that 2 is a prime number. For reference the defition of
+  In this level, we will prove that 2 is a prime number. For reference the definition of
   `Prime n` is that \"n ≥ 2 and if a ∣ n, then a = 1 or a = n.\"
 "
 
-LemmaDoc MyNat.prime_two as "two_prime" in "Prime" "
+LemmaDoc MyNat.prime_two as "prime_two" in "Prime" "
 `prime_two` is a proof that 2 is prime.
 "
 
+example (a n : ℕ) (h : a ∣ n) : a ≤ n := by
+  rcases h with ⟨b, hb⟩
+  have : 1 ≤ b := by {
+    by_contra h
+    have : b = 0 := by
+  }
+  sorry
+
 Statement prime_two :
   Prime 2 := by
   unfold Prime
@@ -28,14 +37,13 @@ Statement prime_two :
   rw [add_zero]
   rfl
   intros a ha
-  have : a ≤ n := by sorry
+  have : a ≤ 2 := by sorry
   have h : a = 0 ∨ a = 1 ∨ a = 2 := by sorry
-  cases h
-  rcases ha with ⟨b, hb⟩
-  rw [h] at ha
-  
-
-
-
+  rcases h with ⟨h1, h2⟩
+  · exfalso
+    rcases ha with ⟨b, hb⟩
+    rw [zero_mul] at hb
+    cases hb
+  · exact h
 
 end MyNat