proposition: Lemma onc3_os__acute : forall O P A B C, OnCircle A O P -> OnCircle B O P -> OnCircle C O P -> OS A B O C -> Acute A C B.
proof: Proof. intros O P A B C HA HB HC HOS. destruct (midpoint_existence A B) as [M HM]. assert (HNCol : ~ Col A B C) by (eapply one_side_not_col124, HOS). assert (HLt : Lt M A M C). { assert (HNCol1 : ~ Col A B O) by (eapply one_side_not_col123, HOS). assert (M <> O) by (intro; treat_equalities; apply HNCol1; Col). assert (O <> C) by (intro; treat_equalities; auto). suma.assert_diffs. assert (Cong O A O C) by (apply (onc2__cong O P); assumption). destruct (angle_partition M O C); auto. - assert (HMO := H). clear H. destruct (l8_18_existence M O C) as [H []]. { intro. destruct (acute_col__out M O C) as [_ [_ [HBet|HBet]]]; auto. - apply l9_9_bis in HOS. apply HOS. repeat split; Col. exists M; split; Col. - apply (le__nlt O C O M); Le. apply (cong2_lt__lt O M O P); Cong. apply bet_inc2__incs with A B; Circle; Between. } assert (Perp O M A B) by (apply mid_onc2__perp with P; auto). assert (HOS1 : OS A B C H). { apply l12_6, par_not_col_strict with C; Col. apply l12_9 with O M; Perp; [|Cop| |Cop]. apply coplanar_perm_5, col_cop__cop with B; Col; Cop. apply coplanar_perm_5, col_cop__cop with A; Col; Cop. } assert (M <> H) by (intro; subst; apply one_side_not_col124 in HOS1; apply HOS1; Col). assert (Per M H C) by (apply perp_per_1, perp_left_comm, perp_col with O; Col). apply lt_transitivity with H C; [|suma.assert_diffs; apply l11_46; auto]. apply cong_lt_per2__lt_1 with O O; Cong. apply l8_2, per_col with M; Col; Perp. apply perp_per_1, perp_left_comm, perp_col1 with B; Col. apply bet__lt1213; auto; apply out2__bet. apply (acute_col_perp__out C); [apply acute_sym|..]; Col; Perp. apply (l9_19 A B); Col; apply one_side_transitivity with C; assumption. - apply lt_transitivity with O C; [|apply l11_46; auto]. apply (cong2_lt__lt M A O A); Cong. apply l11_46; auto. left. apply mid_onc2__per with P B; auto. } destruct HLt as [[C' [HBet HCong]] HNCong]. exists A, C', B; split. apply thales_theorem with M; trivial. suma.assert_diffs. assert (C <> C') by (intro; subst; apply HNCong, HCong). apply os3__lta. - apply one_side_transitivity with M. apply invert_one_side, out_one_side; [Col|apply l6_6, bet_out; Between]. apply out_one_side; [left; intro; apply HNCol; ColR|apply l6_6, bet_out; Between]. - apply out_one_side_1 with M; Col; apply l6_6, bet_out; auto. - apply one_side_transitivity with M. apply invert_one_side, out_one_side; [Col|apply l6_6, bet_out; Between]. apply out_one_side; [left; intro; apply HNCol; ColR|apply l6_6, bet_out; Between]. Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec