exact le_of_lt (lt_trans (Nat.pair_lt_pair_left b₁ ha) (Nat.pair_lt_pair_right a₂ hb))
case inl.inl
n a₁ a₂ b₁ b₂ : ℕ
ha✝ : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₂.pair b₂
no goals