chore: variant of Int.toNat_sub

src/Init/Data/Int/Order.lean

@@ -603,6 +603,14 @@ theorem toNat_mul {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a * b).toNat = a.
   match a, b, eq_ofNat_of_zero_le ha, eq_ofNat_of_zero_le hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => rfl
 
+/--
+Variant of `Int.toNat_sub` taking non-negativity hypotheses,
+rather than expecting the arguments to be casts of natural numbers.
+-/
+theorem toNat_sub'' {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a - b).toNat = a.toNat - b.toNat :=
+  match a, b, eq_ofNat_of_zero_le ha, eq_ofNat_of_zero_le hb with
+  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => toNat_sub _ _
+
 theorem toNat_add_nat {a : Int} (ha : 0 ≤ a) (n : Nat) : (a + n).toNat = a.toNat + n :=
   match a, eq_ofNat_of_zero_le ha with | _, ⟨_, rfl⟩ => rfl