English
The v-component after a step is the swap of the original v: step.v = v.swap.
Русский
Компонента v после шага равна swap исходной: step.v = v.swap.
LaTeX
$$$\\text{step.v} = v.swap$$$
Lean4
/-- The reduction step does not change the product vector. -/
theorem step_v (hr : u.r ≠ 0) : u.step.v = u.v.swap :=
by
let ha : u.r + u.b * u.q = u.a := u.rq_eq
let hr : u.r - 1 + 1 = u.r := (add_comm _ 1).trans (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr))
ext
· change ((u.y * u.q + u.z) * u.b + u.y * (u.r - 1 + 1) : ℕ) = u.y * u.a + u.z * u.b
rw [← ha, hr]
ring
· change ((u.w * u.q + u.x) * u.b + u.w * (u.r - 1 + 1) : ℕ) = u.w * u.a + u.x * u.b
rw [← ha, hr]
ring
