Theorem: Nat.lt_sub_right (QuickSortInLean/QuickSort.lean)

State before:
m n k : Nat
mk : k ≤ m
mn : m < n
⊢ m - k < n - k
Tactic:
show m - k + 1 ≤ n - k
State after:
m n k : Nat
mk : k ≤ m
mn : m < n
⊢ m - k + 1 ≤ n - k

State before:
m n k : Nat
mk : k ≤ m
mn : m < n
⊢ m - k + 1 ≤ n - k
Tactic:
have : m - k + 1 = m + 1 - k := Nat.sub_add_eq_add_sub mk
State after:
m n k : Nat
mk : k ≤ m
mn : m < n
this : m - k + 1 = m + 1 - k
⊢ m - k + 1 ≤ n - k

State before:
m n k : Nat
mk : k ≤ m
mn : m < n
this : m - k + 1 = m + 1 - k
⊢ m - k + 1 ≤ n - k
Tactic:
rw [this]
State after:
m n k : Nat
mk : k ≤ m
mn : m < n
this : m - k + 1 = m + 1 - k
⊢ m + 1 - k ≤ n - k

State before:
m n k : Nat
mk : k ≤ m
mn : m < n
this : m - k + 1 = m + 1 - k
⊢ m + 1 - k ≤ n - k
Tactic:
apply Nat.sub_le_sub_right mn
State after:
no goals