English
If i ≤ j ≤ k, then the composition of cycleIcc i j and cycleIcc j k equals cycleIcc i k.
Русский
Если i ≤ j ≤ k, то композиция cycleIcc i j и cycleIcc j k равна cycleIcc i k.
LaTeX
$$$\\forall {n : \\mathbb{N}} \\; \\forall {i j k : \\mathrm{Fin}(n)},\\; i \\le j \\to j \\le k \\to (\\mathrm{cycleIcc}(i,j) \\circ \\mathrm{cycleIcc}(j,k)) = \\mathrm{cycleIcc}(i,k)$$$
Lean4
theorem trans [NeZero n] (hij : i ≤ j) (hjk : j ≤ k) : (cycleIcc i j) ∘ (cycleIcc j k) = (cycleIcc i k) :=
by
ext x
rcases lt_or_ge x i with ch | ch
· simp [cycleIcc_of_lt (lt_of_lt_of_le ch hij), cycleIcc_of_lt ch]
rcases lt_or_ge k x with ch | ch1
· simp [cycleIcc_of_gt (lt_of_le_of_lt hjk ch), cycleIcc_of_gt ch]
rcases lt_or_ge x j with ch2 | ch2
· simp [cycleIcc_of_lt ch2, cycleIcc_of_le_of_le ch ch1, cycleIcc_of_le_of_le ch (le_of_lt ch2)]
split_ifs
repeat cutsat
· simp [cycleIcc_of_le_of_le ch2 ch1, cycleIcc_of_le_of_le ch ch1]
split_ifs with h
· exact val_eq_of_eq (cycleIcc_of_last hij)
· simp [cycleIcc_of_gt (lt_of_le_of_lt ch2 (lt_add_one_of_succ_lt (by cutsat)))]
