We are trying to prove that in an arbitrary Hilbert plane (assuming Hilbert's axioms of Group I:Incidence, II:Order and III:Congruence https://en.wikipedia.org/wiki/Hilbert%27s_axioms), Tarski's axioms A1-A9 (https://en.wikipedia.org/wiki/Tarski%27s_axioms) for 2D neutral geometry hold.
It seems to be a folklore theorem, but we couldn't find a proper reference to a synthetic proof. We could prove most axioms but we have a problem with the five-segment axiom.
The five-segment axiom says that: $${(x \ne y \land Bxyz \land Bx'y'z' \land xy \equiv x'y' \land yz \equiv y'z' \land xu \equiv x'u' \land yu \equiv y'u')} \rightarrow zu \equiv z'u'$$
Using Hilbert's Foundations of Geometry theorem 14 (congruence of supplementary angles) and theorem 18 (Side-Side-Side) we can obtain the five segment axiom when u is not on line xy.
Does anyone know a reference for the proof of Tarski's five segment axiom in the degenerated case when u is on line xy ?
We have found a proof and formalized it using the Coq proof assistant, the details are here: https://hal.inria.fr/hal-01332044