English
Dual statement to ge_antitone for t.ge under shifts.
Русский
Двойственное утверждение к ge_antitone для t.ge при сдвигах.
LaTeX
$$$\\text{Antitone } t.ge$ under shift; formalization omitted.$$
Lean4
theorem le_monotone : Monotone t.le :=
by
let H := fun (a : ℕ) => ∀ (n : ℤ), t.le n ≤ t.le (n + a)
suffices ∀ (a : ℕ), H a by
intro n₀ n₁ h
obtain ⟨a, ha⟩ := Int.nonneg_def.1 h
obtain rfl : n₁ = n₀ + a := by cutsat
apply this
have H_zero : H 0 := fun n => by
simp only [Nat.cast_zero, add_zero]
rfl
have H_one : H 1 := fun n X hX =>
by
rw [← t.shift_le n 1 (n + (1 : ℕ)) rfl, ObjectProperty.prop_shift_iff]
rw [← t.shift_le n 0 n (add_zero n), ObjectProperty.prop_shift_iff] at hX
exact t.le_zero_le _ hX
have H_add : ∀ (a b c : ℕ) (_ : a + b = c) (_ : H a) (_ : H b), H c :=
by
intro a b c h ha hb n
rw [← h, Nat.cast_add, ← add_assoc]
exact (ha n).trans (hb (n + a))
intro a
induction a with
| zero => exact H_zero
| succ a ha => exact H_add a 1 _ rfl ha H_one
