start of proof 2 is prime - changed prime def

Game/Levels/Division/Level_6.lean

@@ -29,12 +29,11 @@ Statement dvd_add_right
     rw [zero_add] at he
     exact he
   · have : 1 ≤ succ d := by sorry
-
     sorry
 
 
 example (a b c d : ℕ) (h : a * c + b = a * d) : a ∣ b := by
-
+  sorry
 
 
 --    obtain ⟨n, rfl⟩ := Nat.le.dest (Nat. le_of_mul_le_mul_left (Nat. le.intro hm) this) use n

Game/Levels/Prime/Level_1.lean

@@ -4,7 +4,7 @@ import Game.MyNat.Prime
 
 World "Prime"
 Level 1
-Title "two_prime"
+Title "prime_two"
 
 LemmaTab "Prime"
 
@@ -13,14 +13,29 @@ namespace MyNat
 Introduction
 "
   In this level, we will prove that 2 is a prime number. For reference the defition of
-  `Prime n` is that \"n ≥ 2 and if n ∣ a * b then n ∣ a or n ∣ b."
+  `Prime n` is that \"n ≥ 2 and if a ∣ n, then a = 1 or a = n.\"
 "
 
-LemmaDoc MyNat.two_prime as "two_prime" in "Prime" "
-`one_div x` is a proof that `1 ∣ x`.
+LemmaDoc MyNat.prime_two as "two_prime" in "Prime" "
+`prime_two` is a proof that 2 is prime.
 "
 
-Statment two_prime
-  Prime 2 := by sorry
+Statement prime_two :
+  Prime 2 := by
+  unfold Prime
+  constructor
+  use 0
+  rw [add_zero]
+  rfl
+  intros a ha
+  have : a ≤ n := by sorry
+  have h : a = 0 ∨ a = 1 ∨ a = 2 := by sorry
+  cases h
+  rcases ha with ⟨b, hb⟩
+  rw [h] at ha
+
+
+
+
 
 end MyNat

Game/MyNat/Prime.lean

@@ -5,8 +5,6 @@ import Game.MyNat.LE
 
 namespace MyNat
 
-def Prime (n : ℕ) := (2 ≤ n) ∧ ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
-
-
+def Prime (n : ℕ) := (2 ≤ n) ∧ ∀ (a : ℕ), a ∣ n → a = 1 ∨ a = n
 
 end MyNat