Prime definition

Game/Levels/Division/Level_6.lean

@@ -31,5 +31,10 @@ Statement dvd_add_right
 
     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
 --    rw [Nat. mul_add] at hm exact Nat. add_left_cancel hm

Game/Levels/Prime.lean

@@ -1 +1,15 @@
 import GameServer.Commands
+import Game.Levels.Prime.Level_1
+
+
+
+World "Prime"
+Title "Prime World"
+
+Introduction
+"
+  In this world, we provide the definition of a prime, and use it to
+  prove that 2 is pirme.
+
+  Click on \"Start\" to proceed.
+"

Game/Levels/Prime/Level_1.lean

@@ -0,0 +1,9 @@
+import Game.Levels.Multiplication
+import Game.MyNat.Division
+import Game.MyNat.Prime
+
+World "Prime"
+Level 1
+Title "two_prime"
+
+

Game/MyNat/Prime.lean

@@ -0,0 +1,12 @@
+import Mathlib.Init.Core
+import Game.MyNat.Definition
+import Game.MyNat.Division
+import Game.MyNat.LE
+
+namespace MyNat
+
+def Prime (n : ℕ) := (2 ≤ n) ∧ ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
+
+
+
+end MyNat