Theorem: Pos.add_le_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_le_add
State after:
no goals