clean up proofs

opencompl · Oct 19, 2024 · 3b7b071 · 3b7b071
1 parent a1c7c23
commit 3b7b071
Showing 1 changed file with 0 additions and 11 deletions.
diff --git a/src/Init/Data/Int/Order.lean b/src/Init/Data/Int/Order.lean
@@ -529,14 +529,6 @@ theorem toNat_sub_toNat_neg : ∀ n : Int, ↑n.toNat - ↑(-n).toNat = n
   | 0 => rfl
   | _+1 => rfl
 
-@[local simp] theorem ofNat_sub_ofNat (m n : Nat) (h : n ≤ m) : (↑m - ↑n : Int) = ↑(m - n) := by
- by_cases h' : n = m
- · subst h'
-   simp
- · have h'' : n < m := by simp [Nat.lt_of_le_of_ne, *]
-   induction (m-n)
-   sorry
-
 /-! ### toNat' -/
 
 theorem mem_toNat' : ∀ {a : Int} {n : Nat}, toNat' a = some n ↔ a = n
@@ -1076,6 +1068,3 @@ theorem eq_natAbs_iff_mul_eq_zero : natAbs a = n ↔ (a - n) * (a + n) = 0 := by
   rw [natAbs_eq_iff, Int.mul_eq_zero, ← Int.sub_neg, Int.sub_eq_zero, Int.sub_eq_zero]
 
 end Int
-
-@[local simp] theorem ofNat_sub_ofNat (m n : Nat) (h : n ≤ m) : (↑m - ↑n : Int) = ↑(m - n) := by
-  [Int.sub_]