proposition: Lemma inangle_dec : forall A B C P, InAngle P A B C \/ ~ InAngle P A B C.
proof: Proof. intros A B C P. elim(cop_dec A B C P). { intro HCop. elim(eq_dec_points A B). intro; subst; right; unfold InAngle; intro; spliter; auto. intro. elim(eq_dec_points C B). intro; subst; right; unfold InAngle; intro; spliter; auto. intro. elim(eq_dec_points P B). intro; subst; right; unfold InAngle; intro; spliter; auto. intro. elim(col_dec A B C). { intro HColB. elim(bet_dec A B C). { intro HBBet. left. repeat split; auto. exists B. split; auto. } intro HBNBet. elim(out_dec B A P). { left. repeat split; auto. exists A; Between. } right. intro Habs. destruct Habs as [_ [_ [_ [X [HXBet HUn]]]]]. destruct HUn as [|HoutBXP]. subst; auto. assert(HInter := out2_bet_out A B C X P); auto. destruct HInter; auto. apply not_bet_out; auto. } intro HNColB. assert(HP' := symmetric_point_construction P B). destruct HP' as [P']. assert_diffs. elim(two_sides_dec B P A C). { intro. assert(HUn := two_sides_in_angle A B C P P'). destruct HUn as [HInAngle|HInAngle]; Between. destruct HInAngle as [_ [_ [_ [X [HXBet HUn]]]]]. destruct HUn as [HXB|HBout]. left; repeat split; auto; exists X; split; auto. right. intro Habs. destruct Habs as [_ [_ [_ [X' [HX'Bet HUn]]]]]. assert(Col B X' P) by (destruct HUn; subst; Col). assert(X = X') by (apply (l6_21 A C B P); ColR). subst X'. assert_diffs. destruct HUn; auto. apply (l6_4_1 P P' B); Between. apply (l6_7 _ _ X); auto. apply l6_6; auto. } intro HNts. elim(col_dec B A P). { intro. elim(out_dec B A P). { intro. left. repeat split; auto. exists A; Between. } intro. right. intro Habs. destruct Habs as [_ [_ [_ [X [HXBet HUn]]]]]. assert(Col B X P) by (destruct HUn; subst; Col). assert(X = A) by (apply (l6_21 A C B P); Col). subst X. destruct HUn; auto. } intro. elim(col_dec B C P). { intro. elim(out_dec B C P). { intro. left. repeat split; auto. exists C; Between. } intro. right. intro Habs. destruct Habs as [_ [_ [_ [X [HXBet HUn]]]]]. assert(Col B X P) by (destruct HUn; subst; Col). assert(X = C) by (apply (l6_21 A C B P); Col). subst X. destruct HUn; auto. } intro. right. intro. apply HNts. apply invert_two_sides. apply in_angle_two_sides; auto. } intro HNCop. right. intro. apply HNCop; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2