proposition: Lemma inscribed_angle : forall O P A B C, OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OS A B O C -> gHalfA A C B A O B.
proof: Proof. intros O P A B C HA HB HC HOS. assert (HCong := (onc2__cong O P)). destruct (col_dec A O C). { suma.assert_diffs. assert (Bet C O A) by (apply col_inc_onc2__bet with O P; Col; Circle). assert (O <> C) by (intro; treat_equalities; auto). apply ghalfa_right_comm, ghalfa_out4__ghalfa with O B B A; try apply out_trivial; auto. apply l6_6, bet_out; auto. apply bet_cong__ghalfa; auto. } destruct (col_dec B O C). { suma.assert_diffs. assert (Bet C O B) by (apply col_inc_onc2__bet with O P; Col; Circle). assert (O <> C) by (intro; treat_equalities; auto). apply ghalfa_left_comm, ghalfa_out4__ghalfa with O A A B; try apply out_trivial; auto. apply l6_6, bet_out; auto. apply bet_cong__ghalfa; auto. } destruct (cop__one_or_two_sides O C A B); Cop. apply inscribed_angle_aux with P; assumption. apply inscribed_angle_aux1 with P; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec