proposition: Lemma inangle__lta : forall A B C P, ~ Col P B C -> InAngle P A B C -> LtA A B P A B C.
proof: Proof. intros A B C P HNCol HIn. split. apply inangle__lea, HIn. intro HConga. apply conga_cop__or_out_ts in HConga; [|Cop]. destruct HConga as [|Habs]. apply HNCol; Col. apply (l9_9 A B P C). assumption. destruct Habs as [HP [HC]]. apply in_angle_one_side; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2