theorem Int.repr_eq_if {a : Int} : a.repr = if 0 ≤ a then a.toNat.repr else "-" ++ (-a).toNat.repr

@[simp]

theorem Int.toString_eq_repr {a : Int} : toString a = a.repr