n m k : Nat
h₀ : succ k ≤ succ m
h₁ : n - k ≤ m - k
⊢ succ n ≤ succ m
n m k : Nat
h₀ : succ k ≤ succ m
h₁ : succ n - succ k ≤ succ m - succ k
⊢ succ n ≤ succ m
simp [succ_sub_succ] at h₁
no goals
n m k : Nat
h₀ : succ k ≤ succ m
h₁ : n - k ≤ m - k
⊢ succ n ≤ succ m
exact succ_le_succ <| Nat.le_of_le_of_sub_le_sub_right (le_of_succ_le_succ h₀) h₁