α : Type ?u.1030791
a b : ZNum
h : a ≤ b
c : ZNum
⊢ c + a ≤ c + b
α : Type ?u.1030791
⊢ ∀ (a b : ZNum), a ≤ b → ∀ (c : ZNum), c + a ≤ c + b
intro a b h c
α : Type ?u.1030791
a b c : ZNum
⊢ a ≤ b → c + a ≤ c + b
α : Type ?u.1030791
a b : ZNum
h : a ≤ b
c : ZNum
⊢ c + a ≤ c + b
revert h
α : Type ?u.1030791
a b c : ZNum
⊢ ↑a ≤ ↑b → ↑c + ↑a ≤ ↑c + ↑b
α : Type ?u.1030791
a b c : ZNum
⊢ a ≤ b → c + a ≤ c + b
transfer_rw
no goals
α : Type ?u.1030791
a b c : ZNum
⊢ ↑a ≤ ↑b → ↑c + ↑a ≤ ↑c + ↑b
exact fun h => _root_.add_le_add_left h c