proposition: Lemma upper_dim_implies_not_two_sides_one_side : upper_dim_axiom -> (forall A B X Y, ~ Col X A B -> ~ Col Y A B -> ~ TS A B X Y -> OS A B X Y).
proof: Proof. intro HUD; intros. assert (A <> B) by (intro; subst; Col). assert(exists PX, Col A B PX /\ Perp A B X PX). apply l8_18_existence. intro. apply H. apply col_permutation_2. assumption. ex_and H3 PX. induction(eq_dec_points PX A). subst PX. apply invert_one_side. eapply (upper_dim_implies_not_two_sides_one_side_aux HUD _ _ _ _ A); auto. apply perp_left_comm. assumption. Col. intro. apply H. Col. intro. apply H0. Col. intro. apply H1. apply invert_two_sides. assumption. apply (upper_dim_implies_not_two_sides_one_side_aux HUD _ _ _ _ PX); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane