proposition: Lemma in_angle_line : forall A B C P, P <> B -> A <> B -> C <> B -> Bet A B C -> InAngle P A B C.
proof: Proof. intros. repeat split; try assumption. exists B. split. assumption. left. reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2