proposition: Lemma cop_inangle__ex_col_inangle : forall A B C P Q, ~ Out B A C -> InAngle P A B C -> Coplanar A B C Q -> exists R, InAngle R A B C /\ P <> R /\ Col P Q R.
proof: Proof. intros A B C P Q HNOut HIn HCop. assert (h := inangle_distincts A B C P HIn); spliter. assert (A <> C) by (intro; subst; apply HNOut, out_trivial; auto). destruct (eq_dec_points P Q). { subst Q. destruct (eq_dec_points A P). subst P; exists C; split; Col. apply inangle3123; auto. exists A; split; Col; apply inangle1123; auto. } destruct (col_dec B P Q) as [HCol|HNCol1]. { destruct (segment_construction B P B P) as [R [HR1 HR2]]. exists R. assert_diffs; split; [|split; ColR]. apply l11_25 with P A C; try (apply out_trivial); auto. apply l6_6, bet_out; auto. } assert_diffs. destruct (col_dec A B C) as [HCol|HNCol2]. exists Q; split; Col. apply in_angle_line; auto. apply not_out_bet; assumption. destruct (col_dec B C P) as [HCol|HNCol3]. - assert (HNCol3 : ~ Col B A P) by (intro; apply HNCol2; ColR). destruct (cop_not_par_same_side B P Q P P A) as [Q0 [HCol1 HOS]]; Col. apply coplanar_perm_16, col_cop__cop with C; Cop. assert (Hd := os_distincts B P A Q0 HOS); spliter; clean. destruct (one_side_dec B A P Q0). { assert (HIn' : InAngle Q0 A B P) by (apply os2__inangle; assumption). exists Q0; split; Col. apply in_angle_trans with P; trivial. } assert (HR : exists R, Bet P R Q0 /\ Col P Q R /\ Col B A R). { destruct (col_dec B A Q0). exists Q0; split; Between; Col. assert_diffs. destruct (cop_nos__ts B A P Q0) as [_ [_ [R [HCol' HBet]]]]; Col; Cop. exists R; split; trivial; split; ColR. } destruct HR as [R [HR1 [HR2 HR3]]]. assert (P <> R) by (intro; subst; apply HNCol3, HR3). exists R; split; auto. apply out321__inangle; auto. apply col_one_side_out with P; trivial. apply one_side_transitivity with Q0; trivial. apply one_side_not_col124 in HOS. apply invert_one_side, out_one_side; Col. apply l6_6, bet_out; auto. - destruct (cop_not_par_same_side B P Q P P C) as [Q0 [HCol1 HOS]]; Col. apply coplanar_perm_3, coplanar_trans_1 with A; Cop. assert (Hd := os_distincts B P C Q0 HOS); spliter; clean. destruct (one_side_dec B C P Q0). { assert (HIn' : InAngle Q0 C B P) by (apply os2__inangle; assumption). exists Q0; split; Col. apply l11_24, in_angle_trans with P; trivial. apply l11_24, HIn. } assert (HR : exists R, Bet P R Q0 /\ Col P Q R /\ Col B C R). { destruct (col_dec B C Q0). exists Q0; split; Between; Col. assert_diffs. destruct (cop_nos__ts B C P Q0) as [_ [_ [R [HCol' HBet]]]]; Col; Cop. exists R; split; trivial; split; ColR. } destruct HR as [R [HR1 [HR2 HR3]]]. assert (P <> R) by (intro; subst; apply HNCol3, HR3). exists R; split; auto. apply l11_24, out321__inangle; auto. apply col_one_side_out with P; trivial. apply one_side_transitivity with Q0; trivial. apply one_side_not_col124 in HOS. apply invert_one_side, out_one_side; Col. apply l6_6, bet_out; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2