proposition: Lemma inscribed_angle_1 : forall O P A B C, A <> B -> B <> C -> A <> C -> OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> Coplanar A B C O -> SumA A C B A C B A O B.
proof: Proof. intros O P A B C HAB HBC HAC HA HB HC HCop. assert (~ Col A B C) by (apply (onc3__ncol O P); auto). destruct (col_dec A B O). { assert (Midpoint O A B) by (apply col_onc2__mid with P; auto). assert (Per A C B) by (apply thales_theorem with O; auto; apply cong_transitivity with O P; Cong). suma.assert_diffs; apply bet_per2__suma; Between. } destruct (cop__one_or_two_sides A B O C); Col; Cop. - destruct (chord_completion O P C O) as [C' []]; Circle. assert (TS A B C' C) by (apply l9_2, bet_ts__ts with O; Side). assert (SuppA A C' B A C B). apply (diam_onc2_ts__suppa O P); [..|repeat split|]; Between. apply (suma_suppa2__suma A C' B A C' B); trivial. apply ghalfa__suma, inscribed_angle with P; trivial. exists C; split; trivial. - apply ghalfa__suma, inscribed_angle with P; trivial. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec