English
If r1 ≤ r2 and either l + r2 ≤ 1 or r2 ≤ δ l, and BalancedSz l r1, then BalancedSz l r2.
Русский
Если r1 ≤ r2 и либо l + r2 ≤ 1, либо r2 ≤ δ l, и BalancedSz(l, r1), то BalancedSz(l, r2).
LaTeX
$$$$\forall l,r_1,r_2 \in \mathbb{N},\; r_1 \le r_2 \rightarrow (l + r_2 \le 1 \lor r_2 \le \delta l) \rightarrow \operatorname{BalancedSz}(l,r_1) \rightarrow \operatorname{BalancedSz}(l,r_2).$$$$
Lean4
theorem balancedSz_up {l r₁ r₂ : ℕ} (h₁ : r₁ ≤ r₂) (h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l) (H : BalancedSz l r₁) :
BalancedSz l r₂ := by
refine or_iff_not_imp_left.2 fun h => ?_
refine ⟨?_, h₂.resolve_left h⟩
cases H with
| inl H =>
cases r₂
· cases h (le_trans (Nat.add_le_add_left (Nat.zero_le _) _) H)
· exact le_trans (le_trans (Nat.le_add_right _ _) H) (Nat.le_add_left 1 _)
| inr H => exact le_trans H.1 (Nat.mul_le_mul_left _ h₁)
