proposition: Lemma upper_dim_implies_col_perp2__col : upper_dim_axiom -> (forall A B X Y P, Col A B P -> Perp A B X P -> Perp P A Y P -> Col Y X P).
proof: Proof. intro HUP; intros. assert (P <> A). eapply perp_not_eq_1. apply H1. eapply upper_dim_implies_per2__col; auto. apply perp_in_per. apply perp_in_sym. apply perp_perp_in. apply H1. assumption. apply perp_in_per. apply perp_in_sym. apply perp_perp_in. apply perp_left_comm. eapply perp_col. auto. apply H0. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane