From ac94282d7a809c9db9adef8b4032ad7ea02fcf63 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 19 Oct 2024 15:29:04 +0100 Subject: [PATCH] remove redundant proofs --- src/Init/Data/Int/Lemmas.lean | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean index 9bf3c18bbeba..4b0e560fb00d 100644 --- a/src/Init/Data/Int/Lemmas.lean +++ b/src/Init/Data/Int/Lemmas.lean @@ -21,14 +21,6 @@ theorem subNatNat_of_sub_eq_zero {m n : Nat} (h : n - m = 0) : subNatNat m n = theorem subNatNat_of_sub_eq_succ {m n k : Nat} (h : n - m = succ k) : subNatNat m n = -[k+1] := by rw [subNatNat, h] -theorem subNatNat_of_sub {m n : Nat} (h : n ≤ m) : subNatNat m n = ↑(m - n) := by - rw [subNatNat, ofNat_eq_coe] - split - case h_1 _ _ => - simp - case h_2 _ h' => - simp [Nat.sub_eq_zero_of_le h] at h' - @[simp] protected theorem neg_zero : -(0:Int) = 0 := rfl @[norm_cast] theorem ofNat_add (n m : Nat) : (↑(n + m) : Int) = n + m := rfl @@ -62,10 +54,6 @@ theorem negOfNat_eq : negOfNat n = -ofNat n := rfl /- ## some basic functions and properties -/ -def eq_add_one_iff_neg_eq_negSucc {m n : Nat} : m = n + 1 ↔ -↑m = -[n+1] := by - simp [Neg.neg, instNegInt, Int.neg, negOfNat] - split <;> simp [Nat.add_one_inj] - @[norm_cast] theorem ofNat_inj : ((m : Nat) : Int) = (n : Nat) ↔ m = n := ⟨ofNat.inj, congrArg _⟩ theorem ofNat_eq_zero : ((n : Nat) : Int) = 0 ↔ n = 0 := ofNat_inj