proposition: Lemma conga_cop__or_out_ts : forall A B C C', Coplanar A B C C' -> CongA A B C A B C' -> Out B C C' \/ TS A B C C'.
proof: Proof. intros. unfold CongA in H0. spliter. ex_and H4 A0. ex_and H5 C0. ex_and H4 A1. ex_and H5 C1. assert (A0=A1). apply (construction_uniqueness B A B A); auto. subst A1. induction (eq_dec_points C0 C1). subst C1. left. unfold Out. repeat split; try assumption. eapply l5_3. apply H6. assumption. right. assert(exists M, Midpoint M C0 C1). apply midpoint_existence. ex_and H14 M. assert(Cong B C0 B C1). apply cong_right_commutativity. eapply l2_11. apply H6. apply between_symmetry. apply H10. apply cong_symmetry. apply cong_left_commutativity. assumption. apply cong_right_commutativity. assumption. assert(Per A0 M C0). unfold Per. exists C1. split. assumption. assumption. assert(Per B M C0). unfold Per. exists C1. split. assumption. assumption. assert(Per A0 M C1). unfold Per. exists C0. split. apply l7_2. assumption. apply cong_symmetry. assumption. assert(Per B M C1). unfold Per. exists C0. split. apply l7_2. assumption. apply cong_symmetry. assumption. assert (B <> A0). intro. subst A0. apply between_identity in H8. subst A. absurde. assert (Cong A C0 A C1). eapply (l4_2 B A A0 C0 B A A0 C1). unfold IFSC. repeat split; try assumption. apply cong_reflexivity. apply cong_reflexivity. assert (Per A M C0). unfold Per. exists C1. split. assumption. assumption. assert (Per A M C1). unfold Per. exists C0. split. apply l7_2. assumption. apply cong_symmetry. assumption. assert(Col B A M). apply cop_per2__col with C0. apply coplanar_perm_12, col_cop__cop with C1; Col. apply coplanar_perm_12, col_cop__cop with C'; Col. apply coplanar_perm_5, col_cop__cop with C; Col; Cop. intro. subst M. apply is_midpoint_id in H15. contradiction. assumption. assumption. induction(eq_dec_points B M). subst M. assert(~Col A B C). apply per_not_col. assumption. auto. apply per_col with C1. intro. subst C1. apply l7_2 in H15. apply is_midpoint_id in H15. subst C0. absurde. assumption. assert(Bet C B C1). eapply between_exchange3. apply between_symmetry. apply H6. apply midpoint_bet. assumption. unfold Col. right; right. assumption. assert(~Col A B C'). apply per_not_col. assumption. auto. apply per_col with C1. intro. subst C1. apply l7_2 in H15. apply is_midpoint_id in H15. subst C0. absurde. assumption. assert(Bet C' B C0). eapply between_exchange3. apply between_symmetry. apply H10. apply midpoint_bet. apply l7_2. assumption. unfold Col. right; left. apply between_symmetry. assumption. unfold TS. repeat split. Col. Col. exists B. split. Col. apply between_symmetry. eapply between_exchange3. apply between_symmetry. apply H10. apply between_symmetry. eapply between_exchange3. apply between_symmetry. apply H6. apply midpoint_bet. assumption. assert(TS B M C0 C1). unfold TS. repeat split. intro. apply per_not_col in H17. apply H17. apply col_permutation_1. assumption. assumption. intro. subst C0. apply is_midpoint_id in H15. subst C1. absurde. intro. apply per_not_col in H19. apply H19. Col. assumption. intro. subst C1. apply l7_2 in H15. apply is_midpoint_id in H15. subst C0. absurde. exists M. split. apply col_trivial_3. apply midpoint_bet. assumption. apply (col_two_sides _ _ A) in H26. apply invert_two_sides in H26. assert(TS A B C C1). eapply l9_5. apply H26. apply col_trivial_3. unfold Out. repeat split. intro. subst C0. apply cong_symmetry in H14. apply cong_identity in H14. subst C1. absurde. assumption. right. assumption. apply l9_2. eapply l9_5. apply l9_2. apply H27. apply col_trivial_3. unfold Out. repeat split. intro. subst C1. apply cong_identity in H14. subst C0. absurde. intro. subst C'. apply cong_identity in H7. subst C0. absurde. right. assumption. Col. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2