proposition: Lemma inscribed_angle_aux : forall O P A B C, OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OS A B O C -> TS O C A B -> gHalfA A C B A O B.
proof: Proof. intros O P A B C HA HB HC HOS HTS. destruct (segment_construction C O O P) as [C' []]. suma.assert_diffs. assert (O <> C') by (intro; treat_equalities; auto). assert (HCong := (onc2__cong O P)). apply suma_preserves_ghalfa with A C C' C' C B A O C' C' O B. apply (onc3_os__acute O P); assumption. apply ts__suma, invert_two_sides, col_two_sides with O; Side; Col. apply ts__suma, invert_two_sides, col_two_sides with C; Col. apply ghalfa_out4__ghalfa with A O A C'; try apply out_trivial; auto; [apply l6_6, bet_out|apply ghalfa_left_comm, bet_cong__ghalfa]; auto. apply ghalfa_out4__ghalfa with O B C' B; try apply out_trivial; auto; [apply l6_6, bet_out|apply ghalfa_right_comm, bet_cong__ghalfa]; auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec