case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
a₁ a₂ b : ℕ
h : a₁ < a₂
⊢ pair a₁ b < pair a₂ b
by_cases h₁ : a₁ < b <;> simp [pair, h₁, add_assoc]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)
case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
by_cases h₂ : a₂ < b <;> simp [pair, h₂, h]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)
simp at h₂
case neg.h₁
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ b * b ≤ a₂ * a₂

case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ a₁ < a₂ + b
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)
apply add_lt_add_of_le_of_lt
case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ a₁ < a₂ + b
case neg.h₁
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ b * b ≤ a₂ * a₂

case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ a₁ < a₂ + b
exact mul_self_le_mul_self h₂
no goals
case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ a₁ < a₂ + b
exact Nat.lt_add_right _ _ _ h
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
simp at h₁
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < a₂ * a₂ + (a₂ + b)
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
simp [not_lt_of_gt (lt_of_le_of_lt h₁ h)]
case neg.h₁
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ < a₂ * a₂

case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < a₂ * a₂ + (a₂ + b)
apply add_lt_add
case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b
case neg.h₁
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ < a₂ * a₂

case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b
exact mul_self_lt_mul_self h
case neg.h₂.bc
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ < a₂
case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b
apply add_lt_add_right
no goals
case neg.h₂.bc
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ < a₂
assumption