Theorem: Pos.add_lt_add (Extra/Pos/Lemmas.lean)

State before:
x₁ y₁ x₂ y₂ : Pos
⊢ x₁ < y₁ → x₂ < y₂ → x₁ + x₂ < y₁ + y₂
Tactic:
by_toNat
State after:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat > x₁.toNat → y₂.toNat > x₂.toNat → y₁.toNat + y₂.toNat > x₁.toNat + x₂.toNat

State before:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat > x₁.toNat → y₂.toNat > x₂.toNat → y₁.toNat + y₂.toNat > x₁.toNat + x₂.toNat
Tactic:
exact Nat.add_lt_add
State after:
no goals