∀ {a b : ℤ} (ha₁ : Int64.minValue.toInt ≤ a) (ha₂ : a ≤ Int64.maxValue.toInt) (hb₁ : Int64.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int64.maxValue.toInt), Int64.ofInt (a.tmod b) = Int64.ofIntLE a ha₁ ha₂ % Int64.ofIntLE b hb₁ hb₂