proposition: Lemma inangle__lea : forall A B C P, InAngle P A B C -> LeA A B P A B C.
proof: Proof. intros A B C P HIn. exists P; split; trivial. unfold InAngle in HIn; spliter. apply conga_refl; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2