proposition: Lemma col_preserves_two_sides : forall A B C D X Y, C <> D -> Col A B C -> Col A B D -> TS A B X Y -> TS C D X Y.
proof: Proof. intros A B C D X Y. assert (H := A). intros. unfold TS in *. assert (~ Col X A B). spliter. assumption. clear H. assert (A <> B). intro. subst B. Col. spliter. repeat split. intro. apply H4. apply col_permutation_2. apply (colx C D); Col. intro. apply H5. apply col_permutation_2. apply (colx C D); Col. ex_and H6 T. exists T. split. eapply col3. apply H. apply col_permutation_1. assumption. assumption. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar