proposition: Lemma acute_one_side_aux0 : forall P A O B, Col A O P -> Acute A O P -> Perp O A B O -> OS O B A P.
proof: Proof. intros. assert(LtA A O P A O B). { assert_diffs. apply(acute_per__lta A O P A O B H0); auto. apply perp_perp_in in H1. apply perp_in_comm in H1. apply perp_in_per in H1. assumption. } assert(Out O A P). { assert_diffs. induction H. assert(LeA A O B A O P). { apply l11_31_2; auto. } apply lea__nlta in H3. contradiction. repeat split; auto. induction H. right; Between. left; Between. } apply(out_one_side O B A P); auto. left. apply perp_not_col in H1. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2