Theorem: sub_one_le_sub_one (FormalBook/Chapter_01.lean)

State before:
n m : ℕ
⊢ n ≤ m → n - 1 ≤ m - 1
Tactic:
exact fun h => pred_le_pred h
State after:
no goals