diff --git a/examples/lean/primes.lean b/examples/lean/primes.lean
new file mode 100644
index 0000000000..79cbb3f6a2
--- /dev/null
+++ b/examples/lean/primes.lean
@@ -0,0 +1,550 @@
+----------------------------------------------------------------------------------------------------
+--
+-- theory primes.lean
+-- author: Jeremy Avigad
+--
+-- Experimenting with Lean.
+--
+----------------------------------------------------------------------------------------------------
+
+import macros
+import tactic
+using Nat
+
+--
+-- could go in kernel
+--
+
+theorem or_imp (p q : Bool) : (p ∨ q) ↔ (¬ p → q)
+:= subst (symm (imp_or (¬ p) q)) (not_not_eq p)
+
+--
+-- fundamental properties of Nat
+--
+
+theorem cases_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat), P (n + 1)) : P a
+:= induction_on a H1 (take n : Nat, assume ih : P n, H2 n)
+
+theorem strong_induction_on {P : Nat → Bool} (a : Nat) (H : ∀ n, (∀ m, m < n → P m) → P n) : P a
+:= @strong_induction P H a
+
+-- in hindsight, now I know I don't need these
+theorem one_ne_zero : 1 ≠ 0 := succ_nz 0
+theorem two_ne_zero : 2 ≠ 0 := succ_nz 1
+
+-- 
+-- observation: the proof of lt_le_trans in Nat is not needed
+--
+
+theorem lt_le_trans2 {a b c : Nat} (H1 : a < b) (H2 : b ≤ c) : a < c
+:= le_trans H1 H2
+
+--
+-- also, contrapos and mt are the same theorem
+--
+
+theorem contrapos2 {a b : Bool} (H : a → b) : ¬ b → ¬ a
+:= mt H
+
+--
+-- properties of lt and le
+--
+
+theorem succ_le_succ {a b : Nat} (H : a + 1 ≤ b + 1) : a ≤ b
+:=
+  obtain (x : Nat) (Hx : a + 1 + x = b + 1), from lt_elim H,
+  have H2 : a + x + 1 = b + 1, from (calc
+    a + x + 1 = a + (x + 1) : add_assoc _ _ _
+          ... = a + (1 + x) : { add_comm x 1 }
+          ... = a + 1 + x : symm (add_assoc _ _ _)
+          ... = b + 1 : Hx),
+  have H3 : a + x = b, from (succ_inj H2),
+  show a ≤ b, from (le_intro H3)
+
+-- should we keep this duplication or < and <=?
+theorem lt_succ {a b : Nat} (H : a < b + 1) : a ≤ b
+:= succ_le_succ H
+
+theorem succ_le_succ_eq (a b : Nat) : a + 1 ≤ b + 1 ↔ a ≤ b
+:= iff_intro succ_le_succ (assume H : a ≤ b, le_add H 1)
+
+theorem lt_succ_eq (a b : Nat) : a < b + 1 ↔ a ≤ b
+:= succ_le_succ_eq a b
+
+theorem le_or_lt (a : Nat) : ∀ b : Nat, a ≤ b ∨ b < a
+:=
+  induction_on a (
+    show ∀b, 0 ≤ b ∨ b < 0, 
+      from take b, or_introl (le_zero b) _
+  ) (
+    take a,
+    assume ih : ∀b, a ≤ b ∨ b < a,
+    show ∀b, a + 1 ≤ b ∨ b < a + 1, 
+      from 
+        take b,
+        cases_on b (
+          show a + 1 ≤ 0 ∨ 0 < a + 1, 
+            from or_intror _ (le_add (le_zero a) 1)
+        ) (
+          take b,
+          have H : a ≤ b ∨ b < a, from ih b,
+          show a + 1 ≤ b + 1 ∨ b + 1 < a + 1, 
+            from or_elim H (
+              assume H1 : a ≤ b,
+                or_introl (le_add H1 1) (b + 1 < a + 1)
+            ) (
+              assume H2 : b < a,
+                or_intror (a + 1 ≤ b + 1) (le_add H2 1)
+            )
+        )
+  )
+
+theorem not_le_lt {a b : Nat} : ¬ a ≤ b → b < a
+:= (or_imp _ _) ◂ le_or_lt a b
+
+theorem not_lt_le {a b : Nat} : ¬ a < b → b ≤ a
+:= (or_imp _ _) ◂ (or_comm _ _ ◂ le_or_lt b a)
+
+theorem lt_not_le {a b : Nat} (H : a < b) : ¬ b ≤ a
+:= not_intro (take H1 : b ≤ a, absurd (lt_le_trans H H1) (lt_nrefl a))
+
+theorem le_not_lt {a b : Nat} (H : a ≤ b) : ¬ b < a
+:= not_intro (take H1 : b < a, absurd H (lt_not_le H1))
+
+theorem not_le_iff {a b : Nat} : ¬ a ≤ b ↔ b < a
+:= iff_intro (@not_le_lt a b) (@lt_not_le b a)
+
+theorem not_lt_iff {a b : Nat} : ¬ a < b ↔ b ≤ a
+:= iff_intro (@not_lt_le a b) (@le_not_lt b a)
+
+theorem le_iff {a b : Nat} : a ≤ b ↔ a < b ∨ a = b
+:= 
+  iff_intro (
+    assume H : a ≤ b, 
+    show a < b ∨ a = b, 
+      from or_elim (em (a = b)) (
+        take H1 : a = b,
+        show a < b ∨ a = b, from or_intror _ H1
+      ) (
+        take H2 : a ≠ b,
+        have H3 : ¬ b ≤ a, 
+          from not_intro (take H4: b ≤ a, absurd (le_antisym H H4) H2), 
+        have H4 : a < b, from resolve1 (le_or_lt b a) H3,
+        show a < b ∨ a = b, from or_introl H4 _
+      )
+  )(
+    assume H : a < b ∨ a = b, 
+    show a ≤ b, 
+      from or_elim H (
+        take H1 : a < b, lt_le H1
+      ) (
+        take H1 : a = b, subst (le_refl a) H1
+      )
+  )
+
+theorem ne_symm_iff {A : (Type U)} (a b : A) : a ≠ b ↔ b ≠ a
+:= iff_intro ne_symm ne_symm
+
+theorem lt_iff (a b : Nat) : a < b ↔ a ≤ b ∧ a ≠ b
+:=
+  calc 
+    a < b = ¬ b ≤ a            : symm (not_le_iff)
+       ... = ¬ (b < a ∨ b = a) : { le_iff }
+       ... = ¬ b < a ∧ b ≠ a   : not_or _ _
+       ... = a ≤ b ∧ b ≠ a     : { not_lt_iff }
+       ... = a ≤ b ∧ a ≠ b     : { ne_symm_iff _ _ } 
+
+theorem ne_zero_ge_one {x : Nat} (H : x ≠ 0) : x ≥ 1
+:= resolve2 (le_iff ◂ (le_zero x)) (ne_symm H)
+
+theorem ne_zero_one_ge_two {x : Nat} (H0 : x ≠ 0) (H1 : x ≠ 1) : x ≥ 2
+:= resolve2 (le_iff ◂ (ne_zero_ge_one H0)) (ne_symm H1)
+
+-- the forward direction can be replaced by ne_zero_ge_one, but
+-- note the comments below
+theorem ne_zero_iff (n : Nat) : n ≠ 0 ↔ n > 0
+:= 
+  iff_intro (
+    assume H : n ≠ 0,
+    refute (
+      assume H1 : ¬ n > 0,
+      -- curious: if you make the arguments implicit in the next line,
+      -- it fails (the evaluator is getting in the way, I think)
+      have H2 : n = 0, from le_antisym (@not_lt_le 0 n H1) (le_zero n), 
+      absurd H2 H
+    )
+  ) (
+    -- here too
+    assume H : n > 0, ne_symm (@lt_ne 0 n H)
+  )
+
+-- Note: this differs from Leo's naming conventions
+theorem mul_right_mono {x y : Nat} (H : x ≤ y) (z : Nat) : x * z ≤ y * z
+:=
+  obtain (w : Nat) (Hw : x + w = y), 
+    from le_elim H,
+  le_intro (
+    show x * z + w * z = y * z, 
+      from calc 
+        x * z + w * z = (x + w) * z : symm (distributel x w z)
+                  ... = y * z       : { Hw }
+  )
+
+theorem mul_left_mono (x : Nat) {y z : Nat} (H : y ≤ z) : x * y ≤ x * z
+:= subst (subst (mul_right_mono H x) (mul_comm y x)) (mul_comm z x)
+
+theorem le_addr (a b : Nat) : a ≤ a + b
+:= le_intro (refl (a + b))
+
+theorem le_addl (a b : Nat) : a ≤ b + a
+:= subst (le_addr a b) (add_comm a b)
+
+theorem add_left_mono {a b : Nat} (c : Nat) (H : a ≤ b) : c + a ≤ c + b
+:=  subst (subst (le_add H c) (add_comm a c)) (add_comm b c)
+
+theorem mul_right_strict_mono {x y z : Nat} (H : x < y) (znez : z ≠ 0) : x * z < y * z
+:=
+  obtain (w : Nat) (Hw : x + 1 + w = y), 
+    from le_elim H,
+  have H1 : y * z = x * z + w * z + z, 
+    from calc
+      y * z = (x + 1 + w) * z      : { symm Hw }
+        ... = (x + (1 + w)) * z    : { add_assoc _ _ _ }
+        ... = (x + (w + 1)) * z    : { add_comm _ _ }
+        ... = (x + w + 1) * z      : { symm (add_assoc _ _ _) }
+        ... = (x + w) * z + 1 * z  : distributel _ _ _ 
+        ... = (x + w) * z + z      : { mul_onel _ }
+        ... = x * z + w * z + z    : { distributel _ _ _ },
+  have H2 : x * z ≤ x * z + w * z, from le_addr _ _,
+  have H3 : x * z + w * z < x * z + w * z + z, from add_left_mono _ (ne_zero_ge_one znez),
+  show x * z < y * z, from subst (le_lt_trans H2 H3) (symm H1)
+
+theorem mul_left_strict_mono {x y z : Nat} (H : x < y) (znez : z ≠ 0) : z * x < z * y
+:= subst (subst (mul_right_strict_mono H znez) (mul_comm x z)) (mul_comm y z)
+
+theorem mul_left_le_cancel {a b c : Nat} (H : a * b ≤ a * c) (anez : a ≠ 0) : b ≤ c 
+:=
+  refute (
+    assume H1 : ¬ b ≤ c,
+    have H2 : a * c < a * b, from mul_left_strict_mono (not_le_lt H1) anez,
+    show false, from absurd H (lt_not_le H2)
+  )
+
+theorem mul_right_le_cancel {a b c : Nat} (H : b * a ≤ c * a) (anez : a ≠ 0) : b ≤ c 
+:= mul_left_le_cancel (subst (subst H (mul_comm b a)) (mul_comm c a)) anez
+
+theorem mul_left_lt_cancel {a b c : Nat} (H : a * b < a * c) : b < c
+:=
+  refute (
+    assume H1 : ¬ b < c,
+    have H2 : a * c ≤ a * b, from mul_left_mono a (not_lt_le H1),
+    show false, from absurd H (le_not_lt H2)
+  )
+
+theorem mul_right_lt_cancel {a b c : Nat} (H : b * a < c * a) : b < c 
+:= mul_left_lt_cancel (subst (subst H (mul_comm b a)) (mul_comm c a))
+
+theorem add_right_comm (a b c : Nat) : a + b + c = a + c + b
+:=
+  calc
+    a + b + c = a + (b + c) : add_assoc _ _ _
+          ... = a + (c + b) : { add_comm b c }
+          ... = a + c + b   : symm (add_assoc _ _ _)
+
+theorem add_left_le_cancel {a b c : Nat} (H : a + c ≤ b + c) : a ≤ b
+:=
+  obtain (d : Nat) (Hd : a + c + d = b + c), from le_elim H,
+  le_intro (add_injl (subst Hd (add_right_comm a c d)))
+
+theorem add_right_le_cancel {a b c : Nat} (H : c + a ≤ c + b) : a ≤ b
+:= add_left_le_cancel (subst (subst H (add_comm c a)) (add_comm c b))
+
+--
+-- more properties of multiplication
+--
+
+theorem mul_left_cancel {a b c : Nat} (H : a * b = a * c) (anez : a ≠ 0) : b = c
+:=
+  have H1 : a * b ≤ a * c, from subst (le_refl _) H,
+  have H2 : a * c ≤ a * b, from subst (le_refl _) H,
+  le_antisym (mul_left_le_cancel H1 anez) (mul_left_le_cancel H2 anez)
+
+theorem mul_right_cancel {a b c : Nat} (H : b * a = c * a) (anez : a ≠ 0) : b = c
+:= mul_left_cancel (subst (subst H (mul_comm b a)) (mul_comm c a)) anez
+
+
+--
+-- divisibility
+--
+
+definition dvd (a b : Nat) : Bool := ∃ c, a * c = b
+
+infix 50 | : dvd
+
+theorem dvd_intro {a b c : Nat} (H : a * c = b) : a | b
+:= exists_intro c H
+
+theorem dvd_elim {a b : Nat} (H : a | b) : ∃ c, a * c = b
+:= H
+  
+theorem dvd_self (n : Nat) : n | n := dvd_intro (mul_oner n)
+
+theorem one_dvd (a : Nat) : 1 | a
+:= dvd_intro (mul_onel a)
+
+theorem zero_dvd {a : Nat} (H: 0 | a) : a = 0
+:=
+  obtain (w : Nat) (H1 : 0 * w = a), from H,
+    subst (symm H1) (mul_zerol _)
+
+theorem dvd_zero (a : Nat) : a | 0
+:= exists_intro 0 (mul_zeror _)
+
+theorem dvd_trans {a b c} (H1 : a | b) (H2 : b | c) : a | c
+:= 
+  obtain (w1 : Nat) (Hw1 : a * w1 = b), from H1,
+  obtain (w2 : Nat) (Hw2 : b * w2 = c), from H2,
+    exists_intro (w1 * w2)
+      calc a * (w1 * w2) = a * w1 * w2 : symm (mul_assoc a w1 w2)
+                     ... = b * w2 : { Hw1 }
+                     ... = c : Hw2
+
+theorem dvd_le {x y : Nat} (H : x | y) (ynez : y ≠ 0) : x ≤ y
+:=
+  obtain (w : Nat) (Hw : x * w = y), from H,
+  have wnez : w ≠ 0, from
+    not_intro (take H1 : w = 0, absurd (
+      calc y = x * w : symm Hw
+         ... = x * 0 : { H1 }
+         ... = 0     : mul_zeror x
+    ) ynez),
+  have H2 : x * 1 ≤ x * w, from mul_left_mono x (ne_zero_ge_one wnez),
+  show x ≤ y, from subst (subst H2 (mul_oner x)) Hw
+
+theorem dvd_mul_right {a b : Nat} (H : a | b) (c : Nat) : a | b * c
+:=
+  obtain (d : Nat) (Hd : a * d = b), from dvd_elim H,
+  dvd_intro (
+    calc 
+      a * (d * c) = (a * d) * c : symm (mul_assoc _ _ _)
+              ... = b * c       : { Hd }
+  )
+
+theorem dvd_mul_left {a b : Nat} (H : a | b) (c : Nat) : a | c * b
+:= subst (dvd_mul_right H c) (mul_comm b c)
+
+theorem dvd_add {a b c : Nat} (H1 : a | b) (H2 : a | c) : a | b + c
+:=
+  obtain (w1 : Nat) (Hw1 : a * w1 = b), from H1,
+  obtain (w2 : Nat) (Hw2 : a * w2 = c), from H2,
+    exists_intro (w1 + w2)
+      calc a * (w1 + w2) = a * w1 + a * w2 : distributer _ _ _ 
+                     ... = b + a * w2 : { Hw1 }
+                     ... = b + c : { Hw2 }
+
+theorem dvd_add_cancel {a b c : Nat} (H1 : a | b + c) (H2 : a | b) : a | c
+:=
+  or_elim (em (a = 0)) (
+    assume az : a = 0,
+    have H3 : c = 0, from 
+      calc c = 0 + c : symm (add_zerol _)
+         ... = b + c : { symm (zero_dvd (subst H2 az)) }
+         ... = 0     : zero_dvd (subst H1 az),
+    show a | c, from subst (dvd_zero a) (symm H3)
+  ) (
+    assume anz : a ≠ 0,  
+    obtain (w1 : Nat) (Hw1 : a * w1 = b + c), from H1,
+    obtain (w2 : Nat) (Hw2 : a * w2 = b), from H2,
+    have H3 : a * w1 = a * w2 + c, from subst Hw1 (symm Hw2),
+    have H4 : a * w2 ≤ a * w1, from le_intro (symm H3),
+    have H5 : w2 ≤ w1, from mul_left_le_cancel H4 anz,
+    obtain (w3 : Nat) (Hw3 : w2 + w3 = w1), from le_elim H5,
+    have H6 : b + a * w3 = b + c, from
+      calc 
+        b + a * w3 = a * w2 + a * w3 : { symm Hw2 }
+               ... = a * (w2 + w3)   : symm (distributer _ _ _)
+               ... = a * w1          : { Hw3 }
+               ... = b + c           : Hw1,
+    have H7 : a * w3 = c, from add_injr H6,
+    show a | c, from dvd_intro H7
+  )
+
+--
+-- primes
+--
+
+definition prime p := p ≥ 2 ∧ forall m, m | p → m = 1 ∨ m = p
+
+theorem not_prime_has_divisor {n : Nat} (H1 : n ≥ 2) (H2 : ¬ prime n) : ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n
+:= 
+  have H3 : ¬ n ≥ 2 ∨ ¬ (∀ m : Nat, m | n → m = 1 ∨ m = n),
+    from not_and _ _ ◂ H2,
+  have H4 : ¬ ¬ n ≥ 2,
+    from (symm (not_not_eq _)) ◂ H1,
+  obtain (m : Nat) (H5 :  ¬ (m | n → m = 1 ∨ m = n)),
+    from not_forall_elim (resolve1 H3 H4),
+  have H6 : m | n ∧ ¬ (m = 1 ∨ m = n),
+    from (not_implies _ _) ◂ H5,
+  have H7 : ¬ (m = 1 ∨ m = n) ↔ (m ≠ 1 ∧ m ≠ n),
+    from not_or (m = 1) (m = n),
+  have H8 : m | n ∧ m ≠ 1 ∧ m ≠ n,
+    from subst H6 H7,
+  show ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n,
+    from exists_intro m H8
+
+theorem not_prime_has_divisor2 {n : Nat} (H1 : n ≥ 2) (H2 : ¬ prime n) : 
+  ∃ m, m | n ∧ m ≥ 2 ∧ m < n
+:=
+  have n_ne_0 : n ≠ 0, from
+    not_intro (take n0 : n = 0, substp (fun n, n ≥ 2) H1 n0),
+  obtain (m : Nat) (Hm : m | n ∧ m ≠ 1 ∧ m ≠ n),
+    from not_prime_has_divisor H1 H2,
+  let m_dvd_n := and_eliml Hm in
+  let m_ne_1 := and_eliml (and_elimr Hm) in
+  let m_ne_n := and_elimr (and_elimr Hm) in
+  have m_ne_0 : m ≠ 0, from 
+    not_intro (
+      take m0 : m = 0,
+      have n0 : n = 0, from zero_dvd (subst m_dvd_n m0),
+      absurd n0 n_ne_0
+    ),
+  exists_intro m (
+    and_intro m_dvd_n (
+      and_intro (
+        show m ≥ 2, from ne_zero_one_ge_two m_ne_0 m_ne_1
+      ) (
+        have m_le_n : m ≤ n, from dvd_le m_dvd_n n_ne_0,
+        show m < n, from resolve2 (le_iff ◂ m_le_n) m_ne_n
+      )
+    )
+  )
+
+theorem has_prime_divisor {n : Nat} : n ≥ 2 → ∃ p, prime p ∧ p | n
+:=
+  strong_induction_on n (
+    take n,
+    assume ih : ∀ m, m < n → m ≥ 2 → ∃ p, prime p ∧ p | m,
+    assume n_ge_2 : n ≥ 2,
+    show ∃ p, prime p ∧ p | n, from
+      or_elim (em (prime n)) (
+        assume H : prime n,
+        exists_intro n (and_intro H (dvd_self n))
+      ) (
+        assume H : ¬ prime n,
+        obtain (m : Nat) (Hm : m | n ∧ m ≥ 2 ∧ m < n), 
+          from not_prime_has_divisor2 n_ge_2 H,
+        obtain (p : Nat) (Hp : prime p ∧ p | m),
+          from ih m (and_elimr (and_elimr Hm)) (and_eliml (and_elimr Hm)),
+        have p_dvd_n : p | n, from dvd_trans (and_elimr Hp) (and_eliml Hm),
+        exists_intro p (and_intro (and_eliml Hp) p_dvd_n)
+      )
+  )
+
+--
+-- factorial
+--
+
+variable fact : Nat → Nat
+
+axiom fact_0 : fact 0 = 1
+
+axiom fact_succ : ∀ n, fact (n + 1) = (n + 1) * fact n
+
+-- can the simplifier do this?
+theorem fact_1 : fact 1 = 1
+:=
+  calc
+    fact 1 = fact (0 + 1)       : { symm (add_zerol 1) }
+       ... = (0 + 1) * fact 0   : fact_succ _
+       ... = 1 * fact 0         : { add_zerol 1 }
+       ... = 1 * 1              : { fact_0 }
+       ... = 1                  : mul_oner _
+
+theorem fact_ne_0 (n : Nat) : fact n ≠ 0
+:=
+  induction_on n (
+    not_intro (
+      assume H : fact 0 = 0,
+      have H1 : 1 = 0, from (subst H fact_0),
+      absurd H1 one_ne_zero
+    )
+  ) (
+    take n,
+    assume ih : fact n ≠ 0,
+    not_intro (
+      assume H : fact (n + 1) = 0,
+      have H1 : n + 1 = 0, from
+        mul_right_cancel (
+          calc 
+            (n + 1) * fact n = fact (n + 1) : symm (fact_succ n)
+                         ... = 0            : H
+                         ... = 0 * fact n   : symm (mul_zerol _)
+        ) ih,
+      absurd H1 (succ_nz _)
+    )
+  ) 
+ 
+theorem dvd_fact {m n : Nat} (m_gt_0 : m > 0) (m_le_n : m ≤ n) : m | fact n
+:=
+  obtain (m' : Nat) (Hm' : 1 + m' = m), from le_elim m_gt_0,
+  obtain (n' : Nat) (Hn' : 1 + n' = n), from le_elim (le_trans m_gt_0 m_le_n),
+  have m'_le_n' : m' ≤ n',
+    from add_right_le_cancel (subst (subst m_le_n (symm Hm')) (symm Hn')),
+  have H : ∀ n' m', m' ≤ n' → m' + 1 | fact (n' + 1), from
+    induction (
+      take m' ,
+      assume m'_le_0 : m' ≤ 0,
+      have Hm' : m' + 1 = 1,
+        from calc
+          m' + 1 = 0 + 1 : { le_antisym m'_le_0 (le_zero m') }
+             ... = 1     : add_zerol _,
+      show m' + 1 | fact (0 + 1), from subst (one_dvd _) (symm Hm')  
+    ) (
+      take n',
+      assume ih : ∀m', m' ≤ n' → m' + 1 | fact (n' + 1),
+      take m',
+      assume Hm' : m' ≤ n' + 1, 
+      have H1 : m' < n' + 1 ∨ m' = n' + 1, from le_iff ◂ Hm',
+      or_elim H1 (
+        assume H2 : m' < n' + 1,
+        have H3 : m' ≤ n', from lt_succ H2,
+        have H4 : m' + 1 | fact (n' + 1), from ih _ H3,
+        have H5 : m' + 1 | (n' + 1 + 1) * fact (n' + 1), from dvd_mul_left H4 _, 
+        show m' + 1 | fact (n' + 1 + 1), from subst H5 (symm (fact_succ _))
+      ) (
+        assume H2 : m' = n' + 1,
+        have H3 : m' + 1 | n' + 1 + 1, from subst (dvd_self _) H2,
+        have H4 : m' + 1 | (n' + 1 + 1) * fact (n' + 1), from dvd_mul_right H3 _, 
+        show m' + 1 | fact (n' + 1 + 1), from subst H4 (symm (fact_succ _))         
+      )
+    ),
+  have H1 : m' + 1 | fact (n' + 1), from H _ _ m'_le_n',
+  show m | fact n, 
+    from (subst (subst (subst (subst H1 (add_comm m' 1)) Hm') (add_comm n' 1)) Hn')
+
+theorem primes_infinite (n : Nat) : ∃ p, p ≥ n ∧ prime p
+:=
+  let m := fact (n + 1) in
+  have Hn1 : n + 1 ≥ 1, from le_addl _ _,
+  have m_ge_1 : m ≥ 1, from ne_zero_ge_one (fact_ne_0 _),
+  have m1_ge_2 : m + 1 ≥ 2, from le_add m_ge_1 1,
+  obtain (p : Nat) (Hp : prime p ∧ p | m + 1), from has_prime_divisor m1_ge_2,
+  let prime_p := and_eliml Hp in
+  let p_dvd_m1 := and_elimr Hp in
+  have p_ge_2 : p ≥ 2, from and_eliml prime_p,
+  have two_gt_0 : 2 > 0, from (ne_zero_iff 2) ◂ (succ_nz 1),
+  -- fails if arguments are left implicit
+  have p_gt_0 : p > 0, from @lt_le_trans 0 2 p two_gt_0 p_ge_2, 
+  have p_ge_n : p ≥ n, from
+    refute (
+      assume H1 : ¬ p ≥ n,
+      have H2 : p < n, from not_le_lt H1,
+      have H3 : p ≤ n + 1, from lt_le (lt_le_trans H2 (le_addr n 1)),
+      have H4 : p | m, from dvd_fact p_gt_0 H3,
+      have H5 : p | 1, from dvd_add_cancel p_dvd_m1 H4,
+      have H6 : p ≤ 1, from dvd_le H5 (succ_nz 0),
+      have H7 : 2 ≤ 1, from le_trans p_ge_2 H6,
+      absurd H7 (lt_nrefl 1)
+    ),
+  exists_intro p (and_intro p_ge_n prime_p)
+  
\ No newline at end of file