quick fix: use import from basics on proofs

Author: von-steinkirch

README.md

@@ -114,8 +114,31 @@ theorem double_add (n m : Nat) : double (n + m) = double n + double m := by
 
 <br>
 
+run all `*.lean` files with:
+
 ```shell
 make build
+
+info: src/Basics.lean:8:0: 43 : ℕ
+info: src/Basics.lean:9:0: 44
+info: src/Basics.lean:12:0: Bool.true : Bool
+info: src/Basics.lean:13:0: false
+info: src/Basics.lean:16:0: "gm, anon" : String
+info: src/Basics.lean:17:0: "gm, anon"
+info: src/Basics.lean:27:0: 666
+info: src/Basics.lean:32:0: true
+info: src/Basics.lean:33:0: false
+ℹ [2853/2855] Built src.SimpleProofs_I
+info: src/SimpleProofs_I.lean:21:0: 10
+info: src/SimpleProofs_I.lean:22:0: 0
+info: src/SimpleProofs_I.lean:23:0: 6
+info: src/SimpleProofs_I.lean:26:0: true
+info: src/SimpleProofs_I.lean:27:0: false
+info: src/SimpleProofs_I.lean:28:0: true
+info: src/SimpleProofs_I.lean:31:0: double_add (n m : ℕ) : double (n + m) = double n + double m
+info: src/SimpleProofs_I.lean:34:0: 14
+info: src/SimpleProofs_I.lean:35:0: 14
+Build completed successfully.
 ```
 
 <br>

src/SimpleProofs_I.lean

@@ -1,13 +1,9 @@
+import src.Basics
+
 /-!
 ## simple proofs I
 -/
 
--- takes a natural number and returns its double
-def double (n : Nat) : Nat := n + n
-
--- checks if a number is even by seeing if it's divisible by 2
-def isEven (n : Nat) : Bool := n % 2 = 0
-
 -- this theorem proves that doubling the sum of two numbers is the same as
 -- adding their doubles --> 2(n + m) = 2n + 2m