proposition: Lemma inscribed_angle_aux1 : forall O P A B C, OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OS A B O C -> OS O C A B -> gHalfA A C B A O B.
proof: Proof. assert (Haux : forall O P A B C, OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OS A B O C -> OS O C A B -> OS O B A C -> gHalfA A C B A O B). { intros O P A B C HA HB HC HOS1 HOS2 HOS3. destruct (chord_completion O P C O) as [C' [HC' HBet ]]; Circle. suma.assert_diffs. assert (C' <> O) by (intro; treat_equalities; auto). assert (TS O B A C'). { apply l9_8_2 with C; [|Side]. apply one_side_not_col124 in HOS3. repeat split. Col. intro; apply HOS3; ColR. exists O; split; Col. } assert (HCong := (onc2__cong O P)). apply acute_ghalfa2_sams_suma2__ghalfa123 with B C O A C O B O C' A O C'. - repeat split; auto. right; intro; assert_cols; assert_ncols; Col. exists C'. split; CongA. repeat split; [Side| |Cop]. apply l9_9_bis, invert_one_side, one_side_symmetry, os_ts1324__os; [|Side]. apply col_one_side with C; Col; Side. - apply (onc3_os__acute O P); assumption. - exists O. repeat (split; CongA); [|Cop]. apply l9_9, invert_two_sides, l9_31; Side. - exists C'. repeat (split; CongA); [Side|Cop]. - apply ghalfa_left_comm, bet_cong__ghalfa; auto. - apply ghalfa_left_comm, bet_cong__ghalfa; auto. } intros O P A B C HA HB HC HOS1 HOS2. assert_ncols. destruct (cop__one_or_two_sides O B A C) as [HTS|]; Col; Cop. apply ghalfa_comm, Haux with P; auto; [..|apply one_side_symmetry, os_ts1324__os]; Side. apply Haux with P; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec