English
If r1 ≤ r2 and either l + r2 ≤ 1 or l ≤ δ r1, and BalancedSz l r2, then BalancedSz l r1.
Русский
Если r1 ≤ r2 и либо l + r2 ≤ 1, либо l ≤ δ r1, и BalancedSz l r2, то BalancedSz l r1.
LaTeX
$$$$\forall l,r_1,r_2,\; r_1 \le r_2 \rightarrow (l + r_2 \le 1 \lor l \le \delta r_1) \rightarrow \operatorname{BalancedSz}(l,r_2) \rightarrow \operatorname{BalancedSz}(l,r_1).$$$$
Lean4
theorem balancedSz_down {l r₁ r₂ : ℕ} (h₁ : r₁ ≤ r₂) (h₂ : l + r₂ ≤ 1 ∨ l ≤ delta * r₁) (H : BalancedSz l r₂) :
BalancedSz l r₁ :=
have : l + r₂ ≤ 1 → BalancedSz l r₁ := fun H => Or.inl (le_trans (Nat.add_le_add_left h₁ _) H)
Or.casesOn H this fun H => Or.casesOn h₂ this fun h₂ => Or.inr ⟨h₂, le_trans h₁ H.2⟩
