English
If b1 < b2, then for any a, pair(a,b1) < pair(a,b2).
Русский
Если b1 < b2, то для любого a выполняется pair(a,b1) < pair(a,b2).
LaTeX
$$$ \forall a,b_1,b_2 \in \mathbb{N},\; b_1 < b_2 \Rightarrow \operatorname{pair}(a,b_1) < \operatorname{pair}(a,b_2). $$$
Lean4
theorem pair_lt_pair_right (a) {b₁ b₂} (h : b₁ < b₂) : pair a b₁ < pair a b₂ :=
by
by_cases h₁ : a < b₁
· simpa [pair, h₁, Nat.add_assoc, lt_trans h₁ h, h] using mul_self_lt_mul_self h
· simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]
by_cases h₂ : a < b₂; swap; · simp [h₂, h]
simp only [h₂, ↓reduceIte]
rw [Nat.add_comm, Nat.add_comm _ a, Nat.add_assoc, Nat.add_lt_add_iff_left]
rwa [Nat.add_comm, ← sqrt_lt, sqrt_add_eq]
exact le_trans (not_lt.mp h₁) (Nat.le_add_left _ _)
