[GOAL]
lo hi a : ℕ
h : Nat.succ lo ≤ a ∧ a ≤ hi
⊢ Nat.succ (Nat.pred a) ≤ hi
[PROOFSTEP]
rw [Nat.succ_pred_eq_of_pos]
[GOAL]
lo hi a : ℕ
h : Nat.succ lo ≤ a ∧ a ≤ hi
⊢ a ≤ hi
lo hi a : ℕ h : Nat.succ lo ≤ a ∧ a ≤ hi ⊢ 0 < a
[PROOFSTEP]
exact h.right
[GOAL]
lo hi a : ℕ
h : Nat.succ lo ≤ a ∧ a ≤ hi
⊢ 0 < a
[PROOFSTEP]
exact lt_of_le_of_lt (Nat.zero_le lo) h.left
