apply Nat.succ_le_succ
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
b : ℕ
⊢ Nat.succ (plus m b) ≤ Nat.succ (plus n b)
case a
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
b : ℕ
⊢ plus m b ≤ plus n b