diff --git a/tests/lean/induction1.lean b/tests/lean/induction1.lean
new file mode 100644
index 000000000..8db848fc3
--- /dev/null
+++ b/tests/lean/induction1.lean
@@ -0,0 +1,37 @@
+import macros -- loads the take, assume, obtain macros
+
+using Nat     -- using the Nat namespace (it allows us to suppress the Nat:: prefix)
+
+axiom Induction : ∀ P : Nat → Bool, P 0 ⇒ (∀ n, P n ⇒ P (n + 1)) ⇒ ∀ n, P n.
+
+-- induction on n
+
+theorem Comm1 : ∀ n m, n + m = m + n
+:= Induction
+     ◂ _          -- I use a placeholder because I do not want to write the P
+     ◂ (take m,   -- Base case
+         calc 0 + m  = m      :  add::zerol m
+                 ... = m + 0  :  symm (add::zeror m))
+     ◂ (take n,   -- Inductive case
+          assume (iH : ∀ m, n + m = m + n),
+            take m,
+               calc n + 1 + m  = (n + m) + 1  : add::succl n m
+                          ...  = (m + n) + 1  : { iH ◂ m }
+                          ...  = m + (n + 1)  : symm (add::succr m n))
+
+-- indunction on m
+
+theorem Comm2 : ∀ n m, n + m = m + n
+:= take n,
+     Induction
+        ◂ _
+        ◂ (calc n + 0  = n      :  add::zeror n
+                   ... = 0 + n  :  symm (add::zerol n))
+        ◂ (take m,
+             assume (iH : n + m = m + n),
+               calc n + (m + 1)  = (n + m) + 1  : add::succr n m
+                            ...  = (m + n) + 1  : { iH }
+                            ...  = (m + 1) + n  : symm (add::succl m n))
+
+
+print environment 1
\ No newline at end of file
diff --git a/tests/lean/induction1.lean.expected.out b/tests/lean/induction1.lean.expected.out
new file mode 100644
index 000000000..0106c05a2
--- /dev/null
+++ b/tests/lean/induction1.lean.expected.out
@@ -0,0 +1,16 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'macros'
+  Using: Nat
+  Assumed: Induction
+  Proved: Comm1
+  Proved: Comm2
+theorem Comm2 : ∀ n m : ℕ, n + m = m + n :=
+    forall::intro
+        (λ n : ℕ,
+           Induction ◂ (λ x : ℕ, n + x == x + n) ◂ (Nat::add::zeror n ⋈ symm (Nat::add::zerol n)) ◂
+           forall::intro
+               (λ m : ℕ,
+                  discharge
+                      (λ iH : n + m = m + n,
+                         Nat::add::succr n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add::succl m n))))