proposition: Lemma diam_onc2_ts__suppa : forall O P A B C C', OnCircle A O P -> OnCircle B O P -> Diam C C' O P -> TS A B C C' -> SuppA A C B A C' B.
proof: Proof. intros O P A B C C' HA HB [HBet [HC HC']] HTS. suma.assert_diffs. assert (HCong := onc2__cong O P). assert (HMid : Midpoint O C C') by (split; Cong). assert (C <> C') by (intro; treat_equalities; auto). assert (HNColA : ~ Col C C' A) by (apply (onc3__ncol O P); auto). assert (HNColB : ~ Col C C' B) by (apply (onc3__ncol O P); auto). assert (HSumaA : SumA A C C' C C' A C A C') by (apply cong_mid__suma with O; auto). assert (HSumaB : SumA B C C' C C' B C B C') by (apply cong_mid__suma with O; auto). assert (Per C A C') by (apply thales_theorem with O; auto). assert (Per C B C') by (apply thales_theorem with O; auto). assert (HSuma : SumA C A C' C B C' C O C') by (suma.assert_diffs; apply bet_per2__suma; auto). apply bet_suma__suppa with C O C'; trivial. destruct (ex_suma C A C' C' C B) as [D [E [F HSuma1]]]; auto. assert (HTS2 : TS C C' A B) by (apply (chord_intersection O P); assumption). assert (HTS3 : TS C' C A B) by (apply invert_two_sides, HTS2). assert (Acute C' C A). { suma.assert_diffs; apply acute_out2__acute with O A. apply l6_6, bet_out; auto. apply out_trivial; auto. apply cong__acute; auto. } assert (Acute C' C B). { suma.assert_diffs; apply acute_out2__acute with O B. apply l6_6, bet_out; auto. apply out_trivial; auto. apply cong__acute; auto. } assert (Acute C C' A). { suma.assert_diffs; apply acute_out2__acute with O A. apply l6_6, bet_out; Between. apply out_trivial; auto. apply cong__acute; auto. } assert (Acute C C' B). { suma.assert_diffs; apply acute_out2__acute with O B. apply l6_6, bet_out; Between. apply out_trivial; auto. apply cong__acute; auto. } assert (HSuma2 : SumA A C B A C' C D E F). apply suma_sym, suma_assoc_1 with A C C' C' C B C A C'; SumA. assert (HSAMS : SAMS A C B A C' C). apply sams_sym, sams_assoc_1 with A C C' C' C B C A C'; SumA. apply suma_assoc_1 with A C' C C C' B D E F; [SumA..|]. apply suma_assoc_2 with C A C' B C C' C B C'; SumA. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec