Fix src/Solution.lean

Author: monadius

src/Solution.lean

@@ -1,5 +1,4 @@
 import Preloaded tactic
-open classical
 
 -- Task 1: Prove that n + m = n + m
 theorem immediate : ∀ n m : ℕ, n + m = n + m :=
@@ -10,4 +9,4 @@ theorem plus_comm : ∀ n m : ℕ, n + m = m + n :=
   by intros; apply add_comm
 
 -- Task 3: Prove excluded middle
-theorem excluded_middle : ∀ p : Prop, p ∨ ¬p := em
+theorem excluded_middle : ∀ p : Prop, p ∨ ¬p := classical.em