English
If j < k, then (cycleIcc i j) k = k.
Русский
Если j < k, то (cycleIcc i j) k = k.
LaTeX
$$$\text{if } j < k:\ (cycleIcc(i,j))(k) = k$$$
Lean4
theorem cycleIcc_of_gt (h : j < k) : (cycleIcc i j) k = k :=
by
by_cases hij : i ≤ j
· have kin : k ∈ Set.range (natAdd_castLEEmb (Nat.sub_le n i)) := by simpa [range_natAdd_castLEEmb] using by cutsat
have :
(((addNatEmb (n - (n - i.1))).trans (finCongr _).toEmbedding).toEquivRange.symm ⟨k, kin⟩) =
subNat i.1 (k.cast (by cutsat)) (by simpa using by cutsat) :=
by simpa [symm_apply_eq] using eq_of_val_eq (by simpa using by cutsat)
simp only [cycleIcc_to_cycleRange hij kin, natAdd_castLEEmb, this, Function.Embedding.trans_apply, addNatEmb_apply,
coe_toEmbedding, finCongr_apply]
rw [cycleRange_of_gt]
· exact eq_of_val_eq (by simpa using by cutsat)
· exact lt_def.mpr (by simpa [sub_val_of_le hij] using by cutsat)
· simp [hij]
