proposition: Lemma upper_dim_implies_perp2__col : upper_dim_axiom -> (forall X Y Z A B, Perp X Y A B -> Perp X Z A B -> Col X Y Z).
proof: Proof. intro HUP; intros. induction(col_dec A B X). induction(eq_dec_points X A). subst A. assert(X <> B). apply perp_distinct in H. spliter. assumption. apply perp_right_comm in H. apply perp_perp_in in H. apply perp_in_comm in H. apply perp_in_per in H. apply perp_right_comm in H0. apply perp_perp_in in H0. apply perp_in_comm in H0. apply perp_in_per in H0. apply col_permutation_2. eapply (upper_dim_implies_per2__col). assumption. apply H. assumption. assumption. assert(Perp A X X Y ). eapply perp_col. auto. apply perp_sym. apply H. assumption. assert(Perp A X X Z). eapply perp_col. auto. apply perp_sym. apply H0. assumption. apply col_permutation_2. apply upper_dim_implies_per2__col with A. assumption. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. eapply perp_col. auto. apply perp_sym. apply H. assumption. assumption. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. eapply perp_col. auto. apply perp_sym. apply H0. assumption. assert(HH0:=H). assert(HH1:=H0). unfold Perp in H. unfold Perp in H0. ex_and H Y0. ex_and H0 Z0. assert(HH2:=H). assert(HH3:=H2). apply perp_in_col in H. apply perp_in_col in H2. spliter. assert(Perp X Y0 A B). eapply perp_col. intro. subst Y0. contradiction. apply HH0. assumption. assert(Perp X Z0 A B). eapply perp_col. intro. subst Z0. contradiction. apply HH1. assumption. assert(Y0 = Z0). eapply l8_18_uniqueness. apply H1. assumption. apply perp_sym. assumption. assumption. apply perp_sym. assumption. subst Z0. eapply (col_transitivity_1 _ Y0). intro. subst Y0. contradiction. Col. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane