feat(Data/Fin/Basic): intCast_val_sub_eq_ite (#17190)

Co-authored-by: Daniel Weber <[email protected]>
leanprover-community · Oct 16, 2024 · 1aaa5b9 · 1aaa5b9
1 parent ebec1b6
commit 1aaa5b9
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
@@ -433,6 +433,10 @@ theorem val_add_eq_ite {n : ℕ} (a b : Fin n) :
     Nat.mod_eq_of_lt (show ↑b < n from b.2)]
 --- Porting note: syntactically the same as the above
 
+lemma intCast_val_sub_eq_sub_add_ite {n : ℕ} (a b : Fin n) :
+    ((a - b).val : ℤ) = a.val - b.val + if b ≤ a then 0 else n := by
+  split <;> fin_omega
+
 section OfNatCoe
 
 @[simp]