English
If x and y are PartENat and x + y equals a natural number n, then x equals the natural cast of n minus a certain natural determined by y.
Русский
Если x и y — PartENat и x+y = n, натуральное, тогда x равно натуральному привидению n минус некое натуральное число зависящее от y.
LaTeX
$$$ \exists x,y : \mathrm{PartENat}, \exists n : \mathbb{N}, x+y=n \Rightarrow x = \uparrow\bigl(n - y_{\mathrm{get}}(\mathrm{dom\_of\_le\_natCast}(\cdot))\bigr) $$$
Lean4
theorem eq_natCast_sub_of_add_eq_natCast {x y : PartENat} {n : ℕ} (h : x + y = n) :
x = ↑(n - y.get (dom_of_le_natCast ((le_add_left le_rfl).trans_eq h))) :=
by
lift x to ℕ using dom_of_le_natCast ((le_add_right le_rfl).trans_eq h)
lift y to ℕ using dom_of_le_natCast ((le_add_left le_rfl).trans_eq h)
rw [← Nat.cast_add, natCast_inj] at h
rw [get_natCast, natCast_inj, eq_tsub_of_add_eq h]
