proof goes through -- but ugly

src/Init/Data/Int/Lemmas.lean

@@ -21,6 +21,15 @@ 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 x h' =>
+    simp
+  case h_2 x h' =>
+    rw [Nat.sub_eq_zero_of_le h] at h'
+    simp 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
@@ -52,13 +61,85 @@ theorem negOfNat_eq : negOfNat n = -ofNat n := rfl
 @[local simp] theorem negSucc_mul_negSucc' (m n : Nat) :
     -[m+1] * -[n+1] = ofNat (succ m * succ n) := rfl
 
-@[local simp] theorem ofNat_sub_ofNat (m n : Nat) (h : n ≤ m) : (↑m - ↑n : Int) = ↑(m - n) := by
-  sorry
-
 /- ## some basic functions and properties -/
 
+
+def alr (n nb : Nat): -↑n = -[nb+1] → n = nb + 1 := by
+  intro h
+  unfold Neg.neg at h
+  unfold instNegInt at h
+  unfold Int.neg at h
+  simp at h
+  unfold negOfNat at h
+  split at h
+  symm at h
+  symm
+  simp at h
+  simp at h
+  subst h
+  simp
+
+def alb (n nb : Nat) : n = nb + 1 → -↑n = -[nb+1] := by
+  intro h
+  unfold Neg.neg
+  unfold instNegInt
+  unfold Int.neg
+  simp
+  unfold negOfNat
+  split
+  symm
+  symm at h
+  simp
+  simp at h
+  simp
+  simp at h
+  rw [Nat.add_one_inj] at h
+  rw [h]
+
+def alc (n nb : Nat) : n = nb + 1 ↔ -↑n = -[nb+1] := by
+  apply Iff.intro
+  · intro h
+    apply alb
+    simp [h]
+  · intro h
+    apply alr
+    simp [h]
+
 @[norm_cast] theorem ofNat_inj : ((m : Nat) : Int) = (n : Nat) ↔ m = n := ⟨ofNat.inj, congrArg _⟩
 
+@[local simp] theorem ofNat_sub_ofNat (m n : Nat) (h : n ≤ m) : (↑m - ↑n : Int) = ↑(m - n) := by
+  unfold HSub.hSub instHSub Sub.sub instSub Int.sub
+  unfold HAdd.hAdd instHAdd Add.add instAdd Int.add
+  simp
+  split
+  case h_1 ia ib na nb ha hb =>
+    simp at hb
+    simp_all
+    cases n
+    · simp_all
+      symm at hb
+      simp [instSubNat]
+      have aad := (@ofNat_inj m na).mp ha
+      rw [aad]
+      have aax := (@ofNat_inj nb 0).mp
+      simp at aax
+      rw [aax hb]
+      simp
+    · simp_all
+  case h_2 ia ib na nb ha hb =>
+    rw [negSucc_coe] at hb
+    simp at hb
+    have asdas := alr n nb hb
+    have aad := (@ofNat_inj m na).mp ha
+    have aa : (nb + 1) <= na := by
+      rw [asdas] at h
+      rw [aad] at h
+      simp [h]
+    rw [subNatNat_of_sub aa]
+    congr <;> simp_all
+  · simp_all
+  · simp_all
+
 theorem ofNat_eq_zero : ((n : Nat) : Int) = 0 ↔ n = 0 := ofNat_inj
 
 theorem ofNat_ne_zero : ((n : Nat) : Int) ≠ 0 ↔ n ≠ 0 := not_congr ofNat_eq_zero

src/Init/Data/Int/Order.lean

@@ -529,6 +529,14 @@ 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
@@ -1068,3 +1076,6 @@ 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_]