start on dvd

Game/MyNat/DecidableDvd.lean

@@ -0,0 +1,30 @@
+import Game.MyNat.DecidableLe
+import Game.Levels.LessOrEqual
+import Game.Levels.Multiplication
+
+namespace MyNat
+
+instance : Dvd MyNat where
+  dvd a b := ∃ c, a * c = b
+
+instance instDecidableDvd : DecidableRel (α := ℕ) (· ∣ ·)
+| _, 0 => isTrue <| by
+  show _ ∣ 0
+  use 0
+  rw [mul_zero]
+  rfl
+| 0, succ m => isFalse <| by
+  rintro ⟨a, ha⟩
+  rw [zero_mul] at ha
+  apply zero_ne_succ at ha
+  exact ha
+| succ m, succ n =>
+  show Decidable (succ m ∣ succ n) by
+  -- idea : just show m ∣ n iff n % m = 0 and show that n % m is computable
+  sorry
+
+example : (2 : ℕ) ≤ 3 := by
+  MyDecide
+
+example : ¬ ((30 : ℕ) ≤ 20) := by
+  MyDecide

Game/MyNat/DecidableEq.lean

@@ -61,10 +61,6 @@ example : (2 : ℕ) * 2 ≠ 5 := by
 example : (3 : ℕ) ^ 2 ≠ 37 := by
   MyDecide
 
--- **TODO** uncomment test when decidableLE instance is created
--- example : (2 : ℕ) ≤ 3 := by
---   MyDecide
-
 -- **TODO** uncomment test when Divisibility World hits and decidableDvd instance is created
 -- example : (2 : ℕ) ∣ 4 := by MyDecide
 --

Game/MyNat/DecidableLe.lean

@@ -0,0 +1,38 @@
+import Game.MyNat.DecidableEq
+import Game.Levels.LessOrEqual
+
+namespace MyNat
+
+instance instDecidableLe : DecidableRel (α := ℕ) (· ≤ ·)
+| 0, _ => isTrue <| by
+  show 0 ≤ _
+  apply MyNat.zero_le
+| succ m, 0 => isFalse <| by
+  show ¬ succ m ≤ 0
+  rintro ⟨a, ha⟩
+  symm at ha
+  apply eq_zero_of_add_right_eq_zero at ha
+  apply succ_ne_zero at ha
+  exact ha
+| succ m, succ n =>
+  match instDecidableLe m n with
+  | isTrue (h : m ≤ n) => isTrue <| by
+    show succ m ≤ succ n
+    rcases h with ⟨a, rfl⟩
+    use a
+    rw [succ_add]
+    rfl
+  | isFalse (h : ¬ m ≤ n) => isFalse <| by
+    show ¬ succ m ≤ succ n
+    contrapose! h
+    rcases h with ⟨a, ha⟩
+    use a
+    rw [succ_add] at ha
+    apply succ_inj at ha
+    exact ha
+
+example : (2 : ℕ) ≤ 3 := by
+  MyDecide
+
+example : ¬ ((30 : ℕ) ≤ 20) := by
+  MyDecide