proposition: Lemma cop_perp2__col : forall X Y Z A B, Coplanar A B Y Z -> Perp X Y A B -> Perp X Z A B -> Col X Y Z.
proof: Proof. intros. induction(col_dec A B X). induction(eq_dec_points X A). subst A. assert(X <> B). apply perp_distinct in H0. spliter. assumption. 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 perp_right_comm in H1. apply perp_perp_in in H1. apply perp_in_comm in H1. apply perp_in_per in H1. apply col_permutation_2. apply cop_per2__col with B. Cop. auto. assumption. assumption. assert(Perp A X X Y ). eapply perp_col. auto. apply perp_sym. apply H0. assumption. assert(Perp A X X Z). eapply perp_col. auto. apply perp_sym. apply H1. assumption. apply col_permutation_2. apply cop_per2__col with A. assert_diffs; apply coplanar_perm_12, col_cop__cop with B; Cop. auto. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. assumption. apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. assumption. assert(HH0:=H0). assert(HH1:=H1). unfold Perp in H0. unfold Perp in H1. ex_and H0 Y0. ex_and H1 Z0. assert(HH2:=H0). assert(HH3:=H3). apply perp_in_col in H0. apply perp_in_col in H3. 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 H2. assumption. apply perp_sym. assumption. assumption. apply perp_sym. assumption. subst Z0. apply (col_transitivity_1 _ Y0). intro. subst Y0. contradiction. Col. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar