proposition: Lemma suppa_ts2__suppa : forall A B C D, TS A C B D -> TS B D A C -> SuppA A B C A D C -> SuppA B A D B C D.
proof: Proof. intros A B C D HTS1 HTS2 HSuppa. assert (HCon : Concyclic A C B D) by (apply suppa_ts__concyclic; trivial). apply concyclic_aux in HCon. destruct HCon as [O [P]]; spliter. apply (cop_onc4_ts__suppa O P); trivial. apply coplanar_perm_2, coplanar_trans_1 with C; [destruct HTS1; Col|Cop..]. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec