proposition: Lemma inangle_one_side2 : forall A B C P Q , ~ Col A B C -> ~ Col A B P -> ~ Col A B Q -> ~ Col C B P -> ~ Col C B Q -> InAngle P A B C -> InAngle Q A B C -> OS A B P Q /\ OS C B P Q.
proof: Proof. intros. split. apply (inangle_one_side _ _ C); Col. apply (inangle_one_side _ _ A); Col. apply l11_24. auto. apply l11_24. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2