proposition: Lemma upper_dim_implies_not_two_sides_one_side_aux : upper_dim_axiom -> (forall A B X Y PX, A <> B -> PX <> A -> Perp A B X PX -> Col A B PX -> ~ Col X A B -> ~ Col Y A B -> ~ TS A B X Y -> OS A B X Y).
proof: Proof. intro HUD; intros. assert(exists P, exists T, Perp PX A P PX /\ Col PX A T /\ Bet Y T P). apply l8_21. assumption. ex_elim H6 P. ex_and H7 T. assert(HH:= upper_dim_implies_col_perp2__col HUD A B X P PX H2 H1 H6). assert(~Col P A B). apply perp_not_col in H6. intro. apply H6. ColR. assert(TS PX A P Y). repeat split. intro. apply H9. ColR. intro. apply H4. ColR. exists T. split. apply col_permutation_2. assumption. apply between_symmetry. assumption. assert(X <> PX). apply perp_not_eq_2 in H1. assumption. assert(P <> PX). apply perp_not_eq_2 in H6. assumption. assert(HA:= (or_bet_out X PX P)). induction HA. assert(TS PX A P X). repeat split; try assumption. intro. apply H9. ColR. intro. apply H3. ColR. exists PX. split. apply col_trivial_1. apply between_symmetry. assumption. eapply l9_8_1. apply l9_2. eapply (col_two_sides _ PX). apply col_permutation_5. assumption. assumption. apply invert_two_sides. apply H14. eapply (col_two_sides _ PX). apply col_permutation_5. assumption. assumption. apply invert_two_sides. apply l9_2. assumption. induction H13. assert(TS A B P Y). eapply (col_two_sides _ PX). Col. assumption. apply invert_two_sides. assumption. assert(HO:= out_two_sides_two_sides A B X Y P PX (sym_not_eq H0) H2 H13 H14). contradiction. apply col_permutation_1 in HH. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane