dependency for Prime

leanprover-community · Nov 1, 2023 · f424d55 · f424d55
1 parent 90ab940
commit f424d55
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/Game/Levels/Division/Level_6.lean b/Game/Levels/Division/Level_6.lean
@@ -1,4 +1,5 @@
 import Game.Levels.Division.Level_5
+import Game.Levels.AdvMultiplication.all_levels
 
 World "Division"
 Level 6
@@ -33,7 +34,7 @@ Statement dvd_add_right
 
 
 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