proposition: Lemma inangle_distincts : forall A B C P, InAngle P A B C -> A <> B /\ C <> B /\ P <> B.
proof: Proof. intros; unfold InAngle in *; spliter; repeat split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2