The proof of Velu's formulae in Washington's "Elliptic Curves" uses two exercises (Ex. 12.6 and Ex.12.8). One part in Ex.12.6 is the following:
Let $E:y^2+a_1xy+a_3y=x^3+a_2x^2+a_4x+a_6$ be an elliptic curve over a field $K$. Let $P,Q$ be two points on $E$. Let $x_{P}, x_Q, x_{P+Q},y_P,y_Q$ denote the $x$- or $y$-coordinates of the points. Let $Q$ be a $2$-torsion point, so $2Q=\infty$ and $Q=-Q$. The exercise claims the following equality holds:
$x_{P+Q}-x_Q=\frac{3x_Q^2+2a_2x_Q+a_4-a_1y_Q}{x_P-x_Q}$
Since the cases $P=Q=-Q$ don't need examination, we assume $x_P\neq x_Q$ and we can use the addition formula as follows:
$x_{P+Q}=\frac{(y_P-y_Q)^2}{(x_P-x_Q)^2}+a_1\frac{y_P-y_Q}{x_P-x_Q}-a_2-x_P-x_Q$
So we need to show that:
$\frac{(y_P-y_Q)^2}{(x_P-x_Q)^2}+a_1\frac{y_P-y_Q}{x_P-x_Q}-a_2-x_P-x_Q-x_Q=\frac{3x_Q^2+2a_2x_Q+a_4-a_1y_Q}{x_P-x_Q}$
After working on it for a while I noticed that I can't solve it due to the following dead end:
The LHS has a $y_P^2$ term while the RHS has not. After replacing $y_P^2$ using the equation of the curve the LHS has a $a_6$ term while the RHS has not. For all i know dividing those terms by $(x_P-x_Q)$ doesn't change anything. I'm thankful for any kind of information, especially any $equalities$ I might have missed.
Note: Since $Q$ is a $2$-torsion point, we can use the negation formulae for $y$-coordinates $y_Q=-a_1x_Q-a_3-y_Q$ to replace $y_Q^2$ as an expression in $x_Q$. That's why that part isn't an issue for now.
The equation of the elliptic curve is $$y^2+a_1xy+a_3y=x^3+a_2x^2+a_4x+a_6.\tag{1}$$ I'll first prove the result, under the additional hypothesis that $Q=(0,0)$. For $Q$ to lie on $E$, $a_6=0$. Then the tangent to $E$ at $Q$ has the equation $a_3y+a_4x=0$. For $Q$ to be $2$-torsion, this has to be vertical, so $a_3=0$ and $a_4\ne0$. If $a_4$ were zero $E$ must have a singularity at $Q$. Then $(1)$ becomes $$y^2+a_1xy=x^3+a_2x^2+a_4x\tag{2}$$ with $a_4\ne0$.
Let $P$ be a point with $P\ne O,Q$. The points $P$, $Q$ and $-P-Q$ are collinear. They are the three points of intersection of $E$ with a non-vertical line through the origin. This line has the equation $y=tx$ for some $t$. Inserting this in $(2)$ gives $$x^3+(a_2-t^2-a_1t)x^2+a_4x=0.\tag{3}$$ The three roots of $(3)$ are $x_P$, $x_Q=0$ and $x_{-P-Q}=x_{P+Q}$. The product of the nonzero roots is $a_4$, that is $a_4=x_Px_{P+Q}$. Thus $$x_{P+Q}=\frac{a_4}{x_P}$$ which is the desired result in this case.
Returning to the general case, let $x'=x-x_Q$ and $y'=y-y_Q$. Then $(1)$ is equivalent to $$y'^2+a'_1x'y'=x'^3+a'_2x'^2+a'_4x'\tag{4}$$ for some $a_1'$, $a_2'$, $a_4'$. Then by the special case above $$x_{P+Q}-x_Q=x'_{P+Q}=\frac{a_4'}{x'_P}=\frac{a'_4}{x_P-x_Q}.$$ But $a_4'$ is the coefficient of $x'$ after substituting $x'+x_Q$ and $y'=x'+y_Q$ in $(1)$. This is clearly $$a_4'=3x_Q^2+2a_2x_Q+a_4-a_1y_Q.$$ That completes the proof in the general case.