Theorem: LoVe.Nat.plus_lt_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.lt_of_add_lt_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_lt_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.lt_of_add_lt_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_lt_add_right h
State after:
no goals