proposition: Lemma lea_in_angle : forall A B C P, LeA A B P A B C -> OS A B C P -> InAngle P A B C.
proof: Proof. intros. assert(H1 := H0). clear H0. assert(H0 : CongA A B P A B P). { assert(~ Col A B P) by (apply (one_side_not_col123 _ _ _ C); Side). assert_diffs. apply conga_refl; auto. } unfold LeA in H. ex_and H T. apply (conga_preserves_in_angle A B C T). apply conga_refl. unfold CongA in H0. spliter. auto. intro. subst C. unfold OS in H1. ex_and H1 X. unfold TS in H1. spliter. apply H1. Col. eapply conga_trans; apply conga_sym. apply H2. apply H0. apply H. apply one_side_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2