match a with 
| 0 => simp [plus]; assumption 
| b+1 => 
  simp [plus] 
  apply Nat.succ_le_succ
  exact succ_leq_succ_of_leq m n b h
α β γ δ : Type
f : α → β
g : β → γ
h✝ : γ → δ
m n a : ℕ
h : m ≤ n
⊢ plus m a ≤ plus n a
no goals