English
If a1 < a2, then for any b, pair(a1,b) < pair(a2,b).
Русский
Если a1 < a2, то для любого b выполняется pair(a1,b) < pair(a2,b).
LaTeX
$$$ \forall a_1,a_2,b \in \mathbb{N},\; a_1 < a_2 \Rightarrow \operatorname{pair}(a_1,b) < \operatorname{pair}(a_2,b). $$$
Lean4
theorem pair_lt_pair_left {a₁ a₂} (b) (h : a₁ < a₂) : pair a₁ b < pair a₂ b :=
by
by_cases h₁ : a₁ < b <;> simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]
· by_cases h₂ : a₂ < b
· simp [h₂, h]
simp only [h₂, ↓reduceIte]
apply Nat.add_lt_add_of_le_of_lt
· exact Nat.mul_self_le_mul_self (not_lt.mp h₂)
· exact Nat.lt_add_right _ h
· simp at h₁
simp only [not_lt_of_gt (lt_of_le_of_lt h₁ h), ite_false]
apply add_lt_add
· exact Nat.mul_self_lt_mul_self h
· apply Nat.add_lt_add_right; assumption
