case pos
a b : ℕ
h : a < b
⊢ b ≤ b * b + a
a b : ℕ
⊢ b ≤ pair a b
by_cases h : a < b <;> simp [pair, h]
no goals
case pos
a b : ℕ
h : a < b
⊢ b ≤ b * b + a
exact le_trans (le_mul_self _) (Nat.le_add_right _ _)