Theorem: LoVe.Nat.plus_le_plus_right (LoVe/LoVelib.lean)

State before:
l m n : ℕ
⊢ m + l ≤ n + l ↔ m ≤ n
Tactic:
apply Iff.intro
State after:
case mp
l m n : ℕ
⊢ m + l ≤ n + l → m ≤ n

case mpr
l m n : ℕ
⊢ m ≤ n → m + l ≤ n + l

State before:
case mp
l m n : ℕ
⊢ m + l ≤ n + l → m ≤ n

case mpr
l m n : ℕ
⊢ m ≤ n → m + l ≤ n + l
Tactic:
{ intro h
  apply Nat.le_of_add_le_add_right h }
State after:
case mpr
l m n : ℕ
⊢ m ≤ n → m + l ≤ n + l

State before:
case mpr
l m n : ℕ
⊢ m ≤ n → m + l ≤ n + l
Tactic:
{ intro h
  apply Nat.add_le_add_right h }
State after:
no goals

State before:
case mp
l m n : ℕ
⊢ m + l ≤ n + l → m ≤ n
Tactic:
intro h
State after:
case mp
l m n : ℕ
h : m + l ≤ n + l
⊢ m ≤ n

State before:
case mp
l m n : ℕ
h : m + l ≤ n + l
⊢ m ≤ n
Tactic:
apply Nat.le_of_add_le_add_right h
State after:
no goals

State before:
case mpr
l m n : ℕ
⊢ m ≤ n → m + l ≤ n + l
Tactic:
intro h
State after:
case mpr
l m n : ℕ
h : m ≤ n
⊢ m + l ≤ n + l

State before:
case mpr
l m n : ℕ
h : m ≤ n
⊢ m + l ≤ n + l
Tactic:
apply Nat.add_le_add_right h
State after:
no goals