Theorem: Lean4Lean.VExpr.Skips.of_liftN_hi (Lean4Lean/Theory/VExpr.lean)

State before:
n1 : Nat
e : VExpr
k1 n2 k2 : Nat
self : Skips (liftN n1 e k1) n2 k2
h : n2 + k2 ≤ k1
⊢ Skips e n2 k2
Tactic:
obtain ⟨k1, rfl⟩ := Nat.le_iff_exists_add'.1 h
State after:
case intro
n1 : Nat
e : VExpr
n2 k2 k1 : Nat
self : Skips (liftN n1 e (k1 + (n2 + k2))) n2 k2
h : n2 + k2 ≤ k1 + (n2 + k2)
⊢ Skips e n2 k2

State before:
case intro
n1 : Nat
e : VExpr
n2 k2 k1 : Nat
self : Skips (liftN n1 e (k1 + (n2 + k2))) n2 k2
h : n2 + k2 ≤ k1 + (n2 + k2)
⊢ Skips e n2 k2
Tactic:
rwa [Skips, Nat.add_comm n2, ← Nat.add_assoc, ← liftN_unliftN_hi (Nat.le_add_left ..),
  liftN'_comm (h := Nat.le_add_left ..), Nat.add_comm, liftN_inj] at self
State after:
no goals