feat(GroupTheory/Perm/Fin): Add (cycleIcc i j) ∘ j.succAbove = i.succAbove for i ≤ j (leanprover-community#39170)

- proves `(cycleIcc i j) ∘ j.succAbove = i.succAbove` for `i ≤ j`, giving the expected `succAbove` compatibility for `cycleIcc`

Author: yuanyi-350

Mathlib/GroupTheory/Perm/Fin.lean

@@ -449,6 +449,11 @@ theorem cycleIcc_zero_eq_cycleRange (i : Fin n) [NeZero n] : cycleIcc 0 i = cycl
   · simp [-cycleIcc_def_le, ch]
   · simp [-cycleIcc_def_le, cycleIcc_of_gt ch, cycleRange_of_gt ch]
 
+theorem cycleIcc_comp_succAbove {n : ℕ} (i j : Fin (n + 1)) (hij : i ≤ j) :
+    (cycleIcc i j) ∘ j.succAbove = i.succAbove := by
+  grind [cycleIcc_of_lt, succAbove_of_castSucc_lt, cycleIcc_of_ge_of_lt,
+    succAbove_of_le_castSucc, coeSucc_eq_succ, cycleIcc_of_gt]
+
 theorem cycleIcc.trans [NeZero n] (hij : i ≤ j) (hjk : j ≤ k) :
     (cycleIcc i j) ∘ (cycleIcc j k) = (cycleIcc i k) := by
   ext x