From 784184a137e0cb71a9a1b128d209e4960c1a8b4a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Jul 2015 12:48:07 -0500 Subject: [PATCH] chore(library/theories/number_theory/primes): remove unnecessary "have" --- library/theories/number_theory/primes.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/library/theories/number_theory/primes.lean b/library/theories/number_theory/primes.lean index f9ae6eb56..9671f9105 100644 --- a/library/theories/number_theory/primes.lean +++ b/library/theories/number_theory/primes.lean @@ -121,7 +121,6 @@ open eq.ops definition infinite_primes (n : nat) : {p | p ≥ n ∧ prime p} := let m := fact (n + 1) in -have Hn1 : n + 1 ≥ 1, from succ_le_succ (zero_le _), have m_ge_1 : m ≥ 1, from le_of_lt_succ (succ_lt_succ (fact_pos _)), have m1_ge_2 : m + 1 ≥ 2, from succ_le_succ m_ge_1, obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from sub_prime_and_dvd m1_ge_2,