proposition: Lemma col_in_angle : forall A B C P, A <> B -> C <> B -> P <> B -> Out B A P \/ Out B C P -> InAngle P A B C.
proof: Proof. intros. induction H2. repeat split; try assumption. exists A. split. apply between_symmetry. apply between_trivial. right. assumption. repeat split; try assumption. exists C. split. apply between_trivial. right. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2