Theorem: le_eq_sub (Pdl/MultisetOrder.lean)

State before:
⊢ ∀ (M N P Q : ℕ), M ≤ P → M + N = P + Q → N = Q + (P - M)
Tactic:
intros M N P Q h0 h1
State after:
M N P Q : ℕ
h0 : M ≤ P
h1 : M + N = P + Q
⊢ N = Q + (P - M)

State before:
M N P Q : ℕ
h0 : M ≤ P
h1 : M + N = P + Q
⊢ N = Q + (P - M)
Tactic:
have := tsub_add_cancel_of_le h0
State after:
M N P Q : ℕ
h0 : M ≤ P
h1 : M + N = P + Q
this : P - M + M = P
⊢ N = Q + (P - M)

State before:
M N P Q : ℕ
h0 : M ≤ P
h1 : M + N = P + Q
this : P - M + M = P
⊢ N = Q + (P - M)
Tactic:
linarith
State after:
no goals