In Neutral Geometry, prove that the opposite sides of a rectangle are congruent. I'm having some trouble proving a theorem of Neutral Geometry. First, allow me to clearly state what we are allowed to assume in Neutral Geometry:


*

*Hilbert's incidence axioms

*Hilbert's order axioms

*Hilbert's congruence axioms

*We are $\textbf{NOT}$ allowed to assume Hilbert's Euclidean parallel postulate (which means we cannot use the converse of the AIA theorem) and we are $\textbf{NOT}$ allowed to assume Dedekind's Axiom (which means we cannot draw a bijection between angle sizes and real number degree measures). Every proof I have found from searching online involves implicitly assuming one of those two axioms, but they don't necessarily hold in Neutral Geometry.
Having said that, here's the theorem I'm trying to prove:
If $\square ABCD$ is a rectangle, then $\overline{AB}\cong\overline{DC}$ and $\overline{AD}\cong\overline{BC}$. Here's my attempted proof:
$\textit{proof}$:


*

*Suppose $\square ABCD$ is a rectangle.

*$\overline{AD}\cong\overline{AD}$ because $\cong$ is reflexive.

*$\sphericalangle A\cong\sphericalangle D$ because $\sphericalangle A$ and $\sphericalangle D$ are right angles and all right angles are congruent.

*$\textbf{Suddenly, a miracle occurs, and we find that}$ $\sphericalangle CAD\cong\sphericalangle BDA$.

*By 2, 3, 4, and the ASA criterion for triangle congruence, we find that $\triangle CDA\cong\triangle BAD$.

*By 5, $\overline{AB}\cong\overline{DC}$.

*Use a similar argument to show that $\overline{AD}\cong\overline{BC}$ $\blacksquare$
Can someone help me fill in the justification for step 4? Is it even possible to justify step 4 in Neutral geometry?
Thanks for your help,
Jay
 A: There is something weird about this question:  Rectangles do not exist in non-Euclidean geometry, so the hypothesis that $ABCD$ is a rectangle implies we must be in Euclidean geometry, and the framing of this as a question of "neutral geometry" doesn't really make sense.
Having said that, there is a stronger and more general version of this that does make sense:

Theorem.  Let $ABCD$ be a quadrilateral with right angles at $A$ and $B$ and congruent angles at $C$ and $D$.  Then $AD \cong BC$.

A quadrilateral with those properties is called a Saccheri quadrilateral, and they exist in all geometries.  Your problem would follow from the above theorem as a simple consequence.
To prove the Theorem above, it's actually easier to start by proving its converse:

Theorem.  Let $ABCD$ be a quadrilateral with right angles at $A$ and $B$ and $AD \cong BC$.  Then $\angle C \cong \angle D$.

Let's suppose you've proved the second theorem above.  (Sketch:  First prove $\Delta ABD \cong \Delta BAC$, then use that to prove $\Delta DCB \cong \Delta CDA$.)  Here's how to use it to prove the first theorem:
Suppose $ABCD$ is a quadrilateral with right angles at $A$ and $B$ and congruent angles at $C$ and $D$, but $AD \not\cong BC$. Then without loss of generality $AD < BC$, so we can find a point $C'$ on $BC$ such that $BC' \cong AD$.  Now $ABC'D$ satisfies the hypotheses of the theorem we have already proved, so  $\angle ADC' \cong \angle BC'D$.  Now use the exterior angle theorem to derive a contradiction.
A: I have also seen this as If a rectangle exists, then the opposite sides are congruent. So if you add the existence of a rectangle to your assumptions, you can get there. 
Assume not, that is assume in rectangle $ABCD$ that $AB<CD$. Then choose $E$ on line $CD$ such that $DE=AB$. By looking at the possibilities for angle DEB, you can reach contradictions in every case except where it's a right angle and $E=C$.
