Proof of Velu's formulas in Washington's Elliptic Curves 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.
 A: 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.
