proposition: Lemma suppa_ts__concyclic : forall A B C D, TS A B C D -> SuppA A C B A D B -> Concyclic A B C D.
proof: Proof. intros A B. assert (Haux : forall C D, TS A B C D -> Obtuse A C B -> SuppA A C B A D B -> Concyclic A B C D). { intros C D HTS HObtuse HSuppa. split. apply ts__coplanar, HTS. assert (HNCol : ~ Col A B C) by (destruct HTS; Col). destruct (triangle_circumscription A B C HNCol) as [O]; spliter. assert (OnCircle A O A /\ OnCircle B O A /\ OnCircle C O A). unfold OnCircle; repeat split; Cong. spliter. exists O, A; repeat split; trivial. destruct (chord_completion O A C O) as [C'[HC' HBet]]; Circle. assert (TS A B C C'). apply bet_ts__ts with O; [apply l9_2, cop_obtuse_onc3__ts with A|]; assumption. apply (conga_cop_onc3_os__onc A B C'); trivial. apply coplanar_trans_1 with C; Col; Cop. exists C; split; Side. apply (suppa2__conga456 A C B); [apply (cop_onc4_ts__suppa O A)|]; assumption. } intros C D HTS HSuppa. assert (HCop : Coplanar A B C D) by (apply ts__coplanar, HTS). suma.assert_diffs; destruct (angle_partition A C B) as [|[|]]; auto; split; trivial. { destruct (Haux D C) as [_ [O [P]]]. Side. apply (acute_suppa__obtuse A C B); trivial. apply suppa_sym, HSuppa. exists O, P. spliter; repeat split; trivial. } destruct (midpoint_existence A B) as [M]. exists M, A. destruct HTS as [HNCol1 [HNCol2 _]]. unfold OnCircle; repeat split; [Cong..| |]; apply cong_symmetry, thales_converse_theorem with B; auto. apply (per_suppa__per A C B); assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec