proposition: Lemma acute_one_side_aux : forall P A O B, OS O A P B -> Acute A O P -> Perp O A B O -> OS O B A P.
proof: Proof. intros P A O B HOS. intros. unfold Acute in H. ex_and H A'. ex_and H1 B'. ex_and H C'. assert(Per A O B). { apply perp_perp_in in H0. apply perp_in_comm in H0. apply perp_in_per in H0. assumption. } assert(CongA A' B' C' A O B). { assert_diffs. apply l11_16; auto. } assert(LtA A O P A O B). { apply(conga_preserves_lta A O P A' B' C' A O P A O B); auto. assert_diffs. apply conga_refl; auto. } assert(~Col P O B). { intro. assert(Per A O P). { assert_diffs. apply (per_col A O B P); Col. } unfold LtA in H4. spliter. apply H7. assert_diffs. apply(l11_16); auto. } assert(NC:~Col A O P). { unfold OS in HOS. ex_and HOS R. unfold TS in H6. spliter. Col. } assert(TS O B A P \/ OS O B A P). { apply(cop__one_or_two_sides O B A P); Cop. apply perp_not_col in H0; Col. } induction H6. unfold TS in H6. spliter. ex_and H8 T. assert(O <> T). { intro. treat_equalities. assert(LeA A O B A O P). { assert_diffs. apply(l11_31_2 A O B A O P); auto. } assert(~LtA A O P A O B). { apply lea__nlta. assumption. } contradiction. } assert(InAngle T A O P). { unfold InAngle. assert_diffs. repeat split; auto. exists T. split; auto. right. finish. } assert(OS O A T P). { apply invert_one_side. apply out_one_side. right; Col. assert_diffs. repeat split; auto. apply perp_not_col in H0. intro; treat_equalities. apply H0; Col. } assert(OS O A T B). { apply (one_side_transitivity _ _ _ P); auto. } destruct(l9_19 O A T B O); Col. apply H14 in H13. spliter. assert(InAngle B A O P). { assert_diffs. apply(l11_25 T A O P A P B H11); auto; try(apply out_trivial; auto). apply l6_6; auto. } apply inangle__lea in H17. apply lea__nlta in H17. contradiction. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2