proposition: Lemma col_two_sides : forall A B C P Q, Col A B C -> A <> C -> TS A B P Q -> TS A C P Q.
proof: Proof. intros. unfold TS in *. spliter. ex_and H3 T. repeat split. intro. apply H1. apply col_permutation_2. eapply col_transitivity_1. apply H0. apply col_permutation_5. assumption. apply col_permutation_1. assumption. intro. apply H2. apply col_permutation_2. eapply col_transitivity_1. apply H0. apply col_permutation_5. assumption. apply col_permutation_1. assumption. exists T. split. apply col_permutation_2. apply col_transitivity_1 with B. intro. subst B. Col. assumption. apply col_permutation_1. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar