fromInt_toInt

formal source

 216    rw [toInt_mk, toNat_zero, toNat_fromNat]
 217    simp [Int.negSucc_eq]
 218
 219theorem fromInt_toInt : ∀ z : LogicInt, fromInt (toInt z) = z := by
 220  intro z
 221  induction z using Quotient.inductionOn with
 222  | h p =>
 223    rcases p with ⟨a, b⟩
 224    show fromInt (toInt (mk a b)) = mk a b
 225    rw [toInt_mk]
 226    -- (toNat a : Int) - toNat b. Case on sign.
 227    by_cases h : toNat b ≤ toNat a
 228    · -- Non-negative case
 229      have hge : (0 : Int) ≤ (toNat a : Int) - toNat b := by
 230        have : (toNat b : Int) ≤ toNat a := by exact_mod_cast h
 231        linarith
 232      obtain ⟨k, hk⟩ := Int.eq_ofNat_of_zero_le hge
 233      rw [hk]
 234      show fromInt (Int.ofNat k) = mk a b
 235      show mk (LogicNat.fromNat k) LogicNat.zero = mk a b
 236      apply sound
 237      -- LogicNat.fromNat k + b = a + 0 = a in LogicNat.
 238      -- We have: (toNat a : Int) - toNat b = k as Int, so toNat a = toNat b + k in Nat.
 239      have hknat : (k : Int) = (toNat a : Int) - toNat b := hk.symm
 240      have hknat' : toNat a = toNat b + k := by
 241        have : (toNat a : Int) = toNat b + k := by linarith
 242        exact_mod_cast this
 243      show LogicNat.fromNat k + b = a + LogicNat.zero
 244      rw [LogicNat.add_zero]
 245      have hcast := congrArg fromNat hknat'
 246      rw [LogicNat.fromNat_toNat] at hcast
 247      -- hcast : a = fromNat (toNat b + k)
 248      -- We need: fromNat k + b = a
 249      have : LogicNat.fromNat (toNat b + k) = LogicNat.fromNat (toNat b) + LogicNat.fromNat k := by