Fix foreign EC add soundness

[mitschabaude]

closes #1531

The foreign EC addition gadget is modified to assert $x_1 \ne x_2$. We do this by first computing $\Delta := x_1 - x_2$ (which is needed subsequently) and checking that $\Delta$ can take none of the values $0$, $f$ and $2f$ -- which are those values equal to 0 modulo $f$ which can't be excluded due to range checks on $x_1$ and $x_2$.

Since $\Delta$ consists of 3 limbs $(\Delta_0, \Delta_1, \Delta_2)$, checking that it doesn't equal $0 = (0,0,0)$ entails checking that not all of the limbs equal 0. We make this more efficient by combining the lower two limbs into one field element (safe, because they are < 2^88), and using a new specialized assertNotVectorEquals() gadget which is suitable to check a vector inequality like $(\Delta_{01}, \Delta_2) \ne (0, 0)$.

Results. The EC add gadget increases from 63 to 69 rows. To me, this seems like a reasonable trade-off given that EC add becomes much less scary to use and analyzing soundness of the higher-level gadgets like scalar mul and ECDSA does not have to reason about degenerate addition cases.