proposition: Lemma col_inangle2__out : forall A B C P Q, ~ Bet A B C -> InAngle P A B C -> InAngle Q A B C -> Col B P Q -> Out B P Q.
proof: Proof. intros A B C P Q HNBet HP HQ HCol. assert (Hd := inangle_distincts A B C P HP); assert (Hd' := inangle_distincts A B C Q HQ); spliter; clean. destruct (col_dec A B C). assert (Out B A C) by (apply not_bet_out; assumption). apply l6_7 with A; [apply l6_6|]; apply in_angle_out with C; auto. destruct (col_dec B A P) as [HCol1|HNCol1]. apply l6_7 with A; [apply l6_6|]; apply col_in_angle_out with C; ColR. apply col_one_side_out with A; trivial. apply one_side_transitivity with C; [|apply one_side_symmetry]; apply invert_one_side, in_angle_one_side; Col. intro; apply HNCol1; ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2