Require Export GeoCoq.Tarski_dev.Ch10_line_reflexivity.
Require Import GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2.

Section T10_1.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma cop__cong_on_bissect : forall A B M P X,
 Coplanar A B X P -> Midpoint M A B -> Perp_at M A B P M -> Cong X A X B ->
 Col M P X.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
intros.
(* Goal: @Col Tn M P X *)
assert(X = M \/ ~ Col A B X /\ Perp_at M X M A B).
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: @Col Tn M P X *)
assert_diffs; apply(cong_perp_or_mid A B M X); Cong.
(* Goal: @Col Tn M P X *)
induction H3.
(* Goal: @Col Tn M P X *)
(* Goal: @Col Tn M P X *)
treat_equalities; Col.
(* Goal: not (@Col Tn P O B) *)
spliter.
(* Goal: @Col Tn M P X *)
apply perp_in_perp in H1.
(* Goal: @Col Tn M P X *)
apply perp_in_perp in H4.
(* Goal: @Col Tn M P X *)
assert_cols.
(* Goal: @Col Tn M P X *)
apply(cop_perp2__col _ _ _ A B); Perp; Cop.
Qed.

Lemma cong_cop_mid_perp__col : forall A B M P X,
 Coplanar A B X P -> Cong A X B X -> Midpoint M A B -> Perp A B P M -> Col M P X.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
intros.
(* Goal: @Col Tn M P X *)
apply (cop__cong_on_bissect A B); Cong.
(* Goal: @Perp_at Tn M A B P M *)
apply l8_15_1; Col.
Qed.

Lemma cop__image_in_col : forall A B P P' Q Q' M,
 Coplanar A B P Q -> ReflectL_at M P P' A B -> ReflectL_at M Q Q' A B ->
 Col M P Q.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
    assert(ReflectL P P' A B).
      eapply (image_in_is_image_spec M).
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    assert(ReflectL Q Q' A B).
      eapply (image_in_is_image_spec M).
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    unfold ReflectL_at in *.
(* Goal: not (@Col Tn P O B) *)
    spliter.
    induction H4.
      induction H6.
        induction (eq_dec_points A M).
          subst M.
          assert (Per B A P).
            unfold Per.
            exists P'.
(* Goal: and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q) *)
            split.
              apply l7_2.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
              assumption.
            apply cong_commutativity.
            eapply is_image_spec_col_cong with A B;Col.
          assert (Per B A Q).
            unfold Per.
            exists Q'.
(* Goal: and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q) *)
            split.
              apply l7_2.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
              assumption.
            apply cong_commutativity.
            eapply is_image_spec_col_cong with A B;Col.
          apply col_permutation_2.

          apply cop_per2__col with B.
(* Goal: @Coplanar Tn O B P A *)
(* Goal: not (@Col Tn P O B) *)
            Cop.
            apply perp_distinct in H4.
(* Goal: not (@Col Tn P O B) *)
            spliter.
            auto.
(* Goal: @Per Tn Y B A *)
(* Goal: @Cong Tn B X B Y *)
            apply l8_2.
            apply H8.
(* Goal: @Per Tn Y B A *)
(* Goal: @Cong Tn B X B Y *)
          apply l8_2.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
          assumption.
        assert (Per A M P).
          unfold Per.
          exists P'.
(* Goal: and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q) *)
          split.
            apply l7_2.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
          apply cong_commutativity.
          eapply is_image_spec_col_cong.
            apply H2.
(* Goal: not (@Col Tn P O B) *)
          Col.
        assert (Per A M Q).
          unfold Per.
          exists Q'.
(* Goal: and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q) *)
          split.
            apply l7_2.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
          apply cong_commutativity.
          eapply is_image_spec_col_cong.
            apply H3.
          apply col_trivial_3.
        apply col_permutation_2.
        apply cop_per2__col with A.
(* Goal: @Coplanar Tn O B P A *)
(* Goal: not (@Col Tn P O B) *)
          assert_diffs; apply coplanar_perm_12, col_cop__cop with B; Cop.
          auto.
(* Goal: @Per Tn Y B A *)
(* Goal: @Cong Tn B X B Y *)
          apply l8_2.
          apply H9.
          auto.
(* Goal: @Per Tn Y B A *)
(* Goal: @Cong Tn B X B Y *)
        apply l8_2.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
      subst P'.
      apply l7_3 in H0.
      subst P.
(* Goal: not (@Col Tn P O B) *)
      Col.
    subst Q'.
    apply l7_3 in H1.
    subst Q.
(* Goal: not (@Col Tn P O B) *)
    Col.
Qed.

Lemma l10_10_spec : forall A B P Q P' Q',
 ReflectL P' P A B -> ReflectL Q' Q A B ->
 Cong P Q P' Q'.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
    destruct (eq_dec_points A B).
      subst B.
      assert (P' = P) by (apply (image_spec__eq A); assumption).
      assert (Q' = Q) by (apply (image_spec__eq A); assumption).
      subst; Cong.
    assert(HH0 := H).
    assert(HH1 := H0).
    unfold ReflectL in H.
    unfold ReflectL in H0.
(* Goal: not (@Col Tn P O B) *)
    spliter.
    ex_and H X.
    ex_and H0 Y.
    assert (exists M, Midpoint M X Y).
      apply midpoint_existence.
    ex_elim H6 Z.
    assert (Col A B Z).
(* Goal: @Per Tn A' B' C' *)
      induction (eq_dec_points X Y).
(* Goal: @Bet Tn A' B' C' *)
(* Goal: @Bet Tn A' B' C' *)
        subst Y.
        apply l7_3 in H7.
        subst X.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
      ColR.
    double P Z R.
    double P' Z R'.
    apply cong_commutativity.
(* Goal: @Col Tn M P X *)
    induction H3.
(* Goal: @TS Tn O B P A *)
      induction H2.
        assert (ReflectL R R' A B).
          apply is_image_is_image_spec .
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
          eapply (midpoint_preserves_image ) with P P' Z.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
            apply l10_4.
            apply is_image_is_image_spec;auto.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
          assumption.
        assert(R <> R').
(* Goal: not (@Col Tn A' B' C') *)
          intro.
          subst R'.
          assert( P' = P).
            eapply l7_9.
              apply H9.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
          subst P'.
          apply perp_distinct in H3.
(* Goal: not (@Col Tn P O B) *)
          spliter.
          absurde.
        assert (Midpoint Y R R') by (eauto using symmetry_preserves_midpoint).
        assert (Cong Q' R' Q R) by (apply (l7_13 Y); assumption).
        assert (Cong P' Z P Z) by (apply (is_image_spec_col_cong A B); assumption).
        assert (Cong Q' Z Q Z) by (apply (is_image_spec_col_cong A B); assumption).
        apply cong_commutativity, (five_segment R R' Z Z); Cong; Between.
          apply cong_transitivity with P Z; [|apply cong_transitivity with P' Z]; Cong.
          intro; treat_equalities; contradiction.
      subst Q'.
      apply l7_3 in H0.
      subst Q.
      apply cong_commutativity.
      eapply is_image_spec_col_cong.
        apply l10_4_spec.
        apply HH0.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    subst P'.
    apply l7_3 in H.
    subst P.
    eapply is_image_spec_col_cong.
      apply l10_4_spec.
      apply HH1.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    assumption.
Qed.

Lemma l10_10 : forall A B P Q P' Q',
 Reflect P' P A B -> Reflect Q' Q A B ->
 Cong P Q P' Q'.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: @Cong Tn P Q P' Q' *)
    induction (eq_dec_points A B).
(* Goal: @Bet Tn A' B' C' *)
(* Goal: @Bet Tn A' B' C' *)
      subst.
(* Goal: @Cong Tn P Q P' Q' *)
(* Goal: @Cong Tn P Q P' Q' *)
      unfold Reflect in *.
(* Goal: @Cong Tn P Q P' Q' *)
(* Goal: @Cong Tn P Q P' Q' *)
      induction H.
(* Goal: @Cong Tn P Q P' Q' *)
(* Goal: @Cong Tn P Q P' Q' *)
(* Goal: @Cong Tn P Q P' Q' *)
        intuition.
(* Goal: @Cong Tn P Q P' Q' *)
(* Goal: @Cong Tn P Q P' Q' *)
      induction H0.
(* Goal: @Cong Tn P Q P' Q' *)
(* Goal: @Cong Tn P Q P' Q' *)
(* Goal: @Cong Tn P Q P' Q' *)
        intuition.
(* Goal: not (@Col Tn P O B) *)
      spliter.
      apply l7_13 with B; apply l7_2;auto.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    apply l10_10_spec with A B;try apply is_image_is_image_spec;assumption.
Qed.

Lemma image_preserves_bet : forall A B C A' B' C' X Y,
  ReflectL A A' X Y -> ReflectL B B' X Y -> ReflectL C C' X Y ->
  Bet A B C ->
  Bet A' B' C'.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: @Bet Tn A' B' C' *)
    destruct (eq_dec_points X Y).
(* Goal: @Bet Tn A' B' C' *)
(* Goal: @Bet Tn A' B' C' *)
      subst Y.
      apply image_spec__eq in H.
      apply image_spec__eq in H0.
      apply image_spec__eq in H1.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      subst; assumption.
    eapply l4_6.
      apply H2.
    unfold Cong_3.
    repeat split; apply l10_10_spec with X Y.
      apply l10_4_spec.
      apply H.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      apply l10_4_spec; assumption.
      apply l10_4_spec.
      apply H.
      apply l10_4_spec.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
      apply l10_4_spec.
      apply H0.
    apply l10_4_spec.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    assumption.
Qed.

Lemma image_gen_preserves_bet : forall A B C A' B' C' X Y,
  Reflect A A' X Y ->
  Reflect B B' X Y ->
  Reflect C C' X Y ->
  Bet A B C ->
  Bet A' B' C'.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: @Bet Tn A' B' C' *)
    destruct (eq_dec_points X Y).
(* Goal: @Bet Tn A' B' C' *)
(* Goal: @Bet Tn A' B' C' *)
      subst Y.
(* Goal: @Bet Tn A' B' C' *)
(* Goal: @Bet Tn A' B' C' *)
      apply image__midpoint in H.
(* Goal: @Bet Tn A' B' C' *)
(* Goal: @Bet Tn A' B' C' *)
      apply image__midpoint in H0.
(* Goal: @Bet Tn A' B' C' *)
(* Goal: @Bet Tn A' B' C' *)
      apply image__midpoint in H1.
(* Goal: @Bet Tn A' B' C' *)
(* Goal: @Bet Tn A' B' C' *)
      subst.
(* Goal: @Bet Tn A' B' C' *)
(* Goal: @Bet Tn A' B' C' *)
      apply l7_15 with A B C X; Midpoint.
    eapply image_preserves_bet;try apply is_image_is_image_spec; eauto.
Qed.

Lemma image_preserves_col : forall A B C A' B' C' X Y,
  ReflectL A A' X Y -> ReflectL B B' X Y -> ReflectL C C' X Y ->
  Col A B C ->
  Col A' B' C'.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
    destruct H2 as [HBet|[HBet|HBet]]; [|apply col_permutation_2|apply col_permutation_1];
    apply bet_col; eapply image_preserves_bet; eauto.
Qed.

Lemma image_gen_preserves_col : forall A B C A' B' C' X Y,
  Reflect A A' X Y -> Reflect B B' X Y -> Reflect C C' X Y ->
  Col A B C ->
  Col A' B' C'.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
    destruct H2 as [HBet|[HBet|HBet]]; [|apply col_permutation_2|apply col_permutation_1];
    apply bet_col; eapply image_gen_preserves_bet; eauto.
Qed.

Lemma image_gen_preserves_ncol : forall A B C A' B' C' X Y,
  Reflect A A' X Y -> Reflect B B' X Y -> Reflect C C' X Y ->
  ~ Col A B C ->
  ~ Col A' B' C'.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: not (@Col Tn A' B' C') *)
    intro.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    apply H2, image_gen_preserves_col with A' B' C' X Y; try (apply l10_4); assumption.
Qed.

Lemma image_gen_preserves_inter : forall A B C D I A' B' C' D' I' X Y,
  Reflect A A' X Y -> Reflect B B' X Y -> Reflect C C' X Y -> Reflect D D' X Y ->
  ~ Col A B C -> C <> D ->
  Col A B I -> Col C D I -> Col A' B' I' -> Col C' D' I' ->
  Reflect I I' X Y.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: @Reflect Tn I I' X Y *)
    destruct (l10_6_existence X Y I) as [I0 HI0]; trivial.
(* Goal: @Reflect Tn I I' X Y *)
    assert (I' = I0); [|subst; assumption].
(* Goal: @eq (@Tpoint Tn) I' I0 *)
    apply (l6_21 A' B' C' D'); trivial.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      apply image_gen_preserves_ncol with A B C X Y; assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      intro; subst D'; apply H4, l10_2_uniqueness with X Y C'; assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      apply image_gen_preserves_col with A B I X Y; assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      apply image_gen_preserves_col with C D I X Y; assumption.
Qed.

Lemma intersection_with_image_gen : forall A B C A' B' X Y,
  Reflect A A' X Y -> Reflect B B' X Y ->
  ~ Col A B A' -> Col A B C -> Col A' B' C ->
  Col C X Y.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: @Col Tn C X Y *)
    apply l10_8.
(* Goal: @Reflect Tn C C X Y *)
    assert (Reflect A' A X Y) by (apply l10_4; assumption).
(* Goal: @Reflect Tn C C X Y *)
    assert (~ Col A' B' A) by (apply image_gen_preserves_ncol with A B A' X Y; trivial).
(* Goal: @Col Tn A B C *)
    assert_diffs.
(* Goal: @Reflect Tn C C X Y *)
    apply image_gen_preserves_inter with A B A' B' A' B' A B; trivial.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    apply l10_4; assumption.
Qed.

Lemma image_preserves_midpoint :
 forall A B C A' B' C' X Y,
 ReflectL A A' X Y -> ReflectL B B' X Y -> ReflectL C C' X Y ->
 Midpoint A B C ->
 Midpoint A' B' C'.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
    unfold Midpoint in *.
(* Goal: not (@Col Tn P O B) *)
    spliter.
(* Goal: and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q) *)
    repeat split.
      eapply image_preserves_bet.
        apply H0.
        apply H.
        apply H1.
        apply H2.
    eapply cong_transitivity.
      eapply l10_10_spec.
        apply H0.
      apply H.
    eapply cong_transitivity.
      apply H3.
    eapply l10_10_spec.
      apply l10_4_spec.
      apply H.
    apply l10_4_spec.
    apply H1.
Qed.


Lemma image_spec_preserves_per : forall A B C A' B' C' X Y,
 ReflectL A A' X Y -> ReflectL B B' X Y -> ReflectL C C' X Y ->
 Per A B C ->
 Per A' B' C'.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: @Per Tn A' B' C' *)
    induction (eq_dec_points X Y).
(* Goal: @Bet Tn A' B' C' *)
(* Goal: @Bet Tn A' B' C' *)
      subst Y.
      apply image_spec__eq in H.
      apply image_spec__eq in H0.
      apply image_spec__eq in H1.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      subst; assumption.
    double C B C1.
    assert (exists C1', ReflectL C1 C1' X Y).
      apply l10_6_existence_spec.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    ex_and H5 C1'.
    unfold Per.
    exists C1'.
(* Goal: and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q) *)
    split.
      eapply image_preserves_midpoint.
        apply H0.
        apply H1.
        apply H6.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    eapply cong_transitivity.
      eapply l10_10_spec.
        apply H.
      apply H1.
    eapply cong_transitivity.
      unfold Per in H2.
      ex_and H2 C2.
      assert (C2=C1).
        eapply symmetric_point_uniqueness.
          apply H2.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
      subst C2.
      apply H5.
    eapply l10_10_spec.
      apply l10_4_spec.
      apply H.
    apply l10_4_spec.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    assumption.
Qed.

Lemma image_preserves_per : forall A B C A' B' C' X Y,
 Reflect A A' X Y -> Reflect B B' X Y -> Reflect C C' X Y ->
 Per A B C ->
 Per A' B' C'.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: @Per Tn A' B' C' *)
    induction (eq_dec_points X Y).
    - induction H; induction H0; induction H1; spliter; [contradiction..|].
(* Goal: @Per Tn A' B' C' *)
      treat_equalities.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      apply midpoint_preserves_per with A B C X; [|apply l7_2..]; assumption.
    - induction H; induction H0; induction H1; spliter; [|contradiction..].
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      apply image_spec_preserves_per with A B C X Y; assumption.
Qed.

Lemma l10_12 : forall A B C A' B' C',
 Per A B C -> Per A' B' C' ->
 Cong A B A' B' -> Cong B C B' C' ->
 Cong A C A' C'.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
    induction (eq_dec_points B C).
      treat_equalities;auto.
(* Goal: @Cong Tn P Q P' Q' *)
    induction (eq_dec_points A B).
      treat_equalities;auto.
    assert (exists X, Midpoint X B B').
      apply midpoint_existence.
    ex_and H5 X.
    double A' X A1.
    double C' X C1.
    assert(Cong_3 A' B' C' A1 B C1)
    by (repeat split;eauto using l7_13, l7_2).
    assert (Per A1 B C1)
      by (eauto using l8_10).
    unfold Cong_3 in H8.
(* Goal: not (@Col Tn P O B) *)
    spliter.
    assert(Cong A B A1 B) by (apply cong_transitivity with A' B'; trivial).
    assert(Cong B C B C1) by (apply cong_transitivity with B' C'; trivial).
    apply cong_transitivity with A1 C1; Cong.
    clear dependent A'; clear dependent B'; clear dependent C'; clear X.

    assert(exists Y, Midpoint Y C C1)
      by (apply midpoint_existence).
    ex_and H0 Y.
    assert(Reflect C1 C B Y) by (apply cong_midpoint__image; assumption).
    assert(exists A2, Reflect A1 A2 B Y).
      apply l10_6_existence.
    ex_elim H2 A2.
    assert (Cong C A2 C1 A1).
      eapply l10_10.
        apply H0.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    apply cong_transitivity with A2 C; Cong.
    assert (Reflect B B B Y) by apply image_triv.
    assert (Per A2 B C).
      eapply (image_preserves_per A1 B C1 A2 B C).
        apply H5.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    assert (Cong A B A2 B).
      apply cong_transitivity with A1 B; trivial.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      apply cong_symmetry, l10_10 with B Y; assumption.
    clear dependent A1; clear dependent C1; clear dependent Y.

    assert (exists Z, Midpoint Z A A2).
      apply midpoint_existence.
    ex_and H0 Z.
    assert (Reflect A2 A B Z) by (apply cong_midpoint__image; Cong).
    destruct (symmetric_point_construction C B) as [C0].
    assert (Cong A C A C0) by (apply per_double_cong with B; assumption).
    assert (Cong A2 C A2 C0) by (apply per_double_cong with B; assumption).
    assert (Reflect C0 C B Z).
      apply is_image_rev, cong_midpoint__image; trivial.
      induction (eq_dec_points A A2).
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        treat_equalities; assumption.
(* Goal: not (@Col Tn P O B) *)
      apply (l4_17 A A2); Col.
    assert (Cong A C A2 C0).
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      apply l10_10 with B Z; assumption.
    apply cong_transitivity with A2 C0; Cong.
Qed.

Lemma cong4_cop2__eq : forall A B C P Q, ~ Col A B C ->
  Cong A P B P -> Cong A P C P -> Coplanar A B C P ->
  Cong A Q B Q -> Cong A Q C Q -> Coplanar A B C Q ->
  P = Q.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros A B C P Q HNCol; intros.
(* Goal: @eq (@Tpoint Tn) P Q *)
    destruct (eq_dec_points P Q); [assumption|].
(* Goal: @eq (@Tpoint Tn) P Q *)
    exfalso.
(* Goal: not (@Col Tn P O B) *)
    apply HNCol.
    assert (Haux : forall R, Col P Q R -> Cong A R B R /\ Cong A R C R).
(* Goal: forall (R : @Tpoint Tn) (_ : @Col Tn P Q R), and (@Cong Tn A R B R) (@Cong Tn A R C R) *)
(* Goal: @Col Tn A B C *)
      intros R HR; split; apply cong_commutativity, (l4_17 P Q); Cong.
(* Goal: @Col Tn A B C *)
    destruct (midpoint_existence A B) as [D].
(* Goal: @Col Tn A B C *)
    assert_diffs.
(* Goal: @Col Tn A B C *)
    assert (HCol1 : Col P Q D).
(* Goal: @Coplanar Tn O B P A *)
(* Goal: not (@Col Tn P O B) *)
    { assert (Coplanar A B C D) by Cop.
(* Goal: @Coplanar Tn O B P A *)
(* Goal: not (@Col Tn P O B) *)
      apply cong3_cop2__col with A B; Cong; apply coplanar_pseudo_trans with A B C; Cop.
    }
(* Goal: not (@Col Tn P O B) *)
    destruct (diff_col_ex3 P Q D HCol1) as [R1]; spliter.
(* Goal: @Col Tn A B C *)
    destruct (segment_construction R1 D R1 D) as [R2 []].
(* Goal: @Col Tn A B C *)
    assert_diffs.
    assert (Col P Q R2) by ColR.
(* Goal: @Col Tn A B C *)
    destruct (Haux R1); trivial.
(* Goal: @Col Tn A B C *)
    destruct (Haux R2); trivial.
(* Goal: @Col Tn A B C *)
    assert (Cong A R1 A R2).
(* Goal: @TS Tn O P A B *)
(* Goal: @TS Tn O B P A *)
    { assert (Per A D R1) by (apply l8_2; exists B; split; Cong).
(* Goal: @Cong Tn A R1 A R2 *)
      apply l10_12 with D D; Cong.
      apply per_col with R1; ColR.
    }
    apply cong3_cop2__col with R1 R2; auto; [apply col_cop2__cop with P Q; auto..| |].
(* Goal: @Cong Tn C R1 C R2 *)
      apply cong_transitivity with A R1; [|apply cong_transitivity with A R2]; Cong.
(* Goal: @Cong Tn C R1 C R2 *)
      apply cong_transitivity with A R1; [|apply cong_transitivity with A R2]; Cong.
Qed.

Lemma l10_16 : forall A B C A' B' P,
 ~ Col A B C -> ~ Col A' B' P -> Cong A B A' B' ->
 exists C', Cong_3 A B C A' B' C' /\ OS  A' B' P C' .
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: @Cong Tn P Q P' Q' *)
    induction (eq_dec_points A B).
      subst B.
      apply cong_symmetry in H1.
      apply False_ind.
      apply H.
      apply col_trivial_1.
    assert(exists X, Col A B X /\ Perp A B C X).
      apply l8_18_existence.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    ex_and H3 X.
    assert (exists X', Cong_3 A B X A' B' X').
      eapply l4_14.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    ex_elim H5 X'.
    assert (exists Q, Perp A' B' Q X' /\ OS A' B' P Q).
      apply l10_15.
        eapply l4_13.
          apply H3.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    ex_and H5 Q.
    assert (exists C', Out X' C' Q /\ Cong  X' C' X C).
      eapply l6_11_existence.
        apply perp_distinct in H5.
(* Goal: not (@Col Tn P O B) *)
        spliter.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
(* Goal: not (@Col Tn A' B' C') *)
      intro.
      subst C.
      apply perp_distinct in H4.
(* Goal: not (@Col Tn P O B) *)
      spliter.
      absurde.
    ex_and H8 C'.
    exists C'.
    unfold Cong_3 in *.
(* Goal: not (@Col Tn P O B) *)
    spliter.
    assert (Cong A C A' C').
      induction(eq_dec_points A X).
        subst X.
        apply cong_symmetry in H10.
        apply cong_identity in H10.
        subst X'.
        apply cong_symmetry.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
      eapply l10_12.
        3: apply H10.
        apply perp_in_per.
        eapply l8_14_2_1b_bis.
          eapply perp_col.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
            apply perp_right_comm.
            apply H4.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
          assumption.
          apply col_trivial_3.
        apply col_trivial_1.
        apply perp_in_per.
        eapply l8_14_2_1b_bis.
          eapply perp_col.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            intro assumption.
            subst X'.
            apply cong_identity in H10.
(* Goal: @TS Tn O B P A *)
            contradiction.
            apply perp_sym.
            eapply perp_col.
(* Goal: not (@Col Tn A' B' C') *)
              intro.
              subst X'.
              apply cong_symmetry in H9.
              apply cong_identity in H9.
              subst X.
              apply perp_distinct in H4.
(* Goal: not (@Col Tn P O B) *)
              spliter.
              absurde.
              apply perp_sym.
              apply perp_right_comm.
              apply H5.
(* Goal: @Col Tn X B Y *)
(* Goal: @Cong Tn B X B Y *)
            apply col_permutation_5.
            eapply out_col.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
          eapply l4_13.
            apply H3.
          unfold Cong_3.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
          repeat split;assumption.
          apply col_trivial_3.
        apply col_trivial_1.
      apply cong_symmetry.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    assert (Cong B C B' C').
      induction(eq_dec_points B X).
        subst X.
        apply cong_symmetry in H11.
        apply cong_identity in H11.
        subst X'.
        apply cong_symmetry.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
      eapply l10_12.
        3: apply H11.
        apply perp_in_per.
        eapply l8_14_2_1b_bis.
          eapply perp_col.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
            apply perp_comm.
            apply H4.
          apply col_permutation_4.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
          assumption.
          apply col_trivial_3.
        apply col_trivial_1.
        apply perp_in_per.
        eapply l8_14_2_1b_bis.
          eapply perp_col.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            intro assumption.
            subst X'.
            apply cong_identity in H11.
(* Goal: @TS Tn O B P A *)
            contradiction.
            apply perp_sym.
            eapply perp_col.
(* Goal: not (@Col Tn A' B' C') *)
              intro.
              subst X'.
              apply cong_symmetry in H9.
              apply cong_identity in H9.
              subst X.
              apply perp_distinct in H4.
(* Goal: not (@Col Tn P O B) *)
              spliter.
              absurde.
              apply perp_sym.
              apply perp_comm.
              apply H5.
(* Goal: @Col Tn X B Y *)
(* Goal: @Cong Tn B X B Y *)
            apply col_permutation_5.
            eapply out_col.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
          apply col_permutation_4.
          eapply l4_13.
            apply H3.
          unfold Cong_3.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
          repeat split; assumption.
          apply col_trivial_3.
        apply col_trivial_1.
      apply cong_symmetry.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
(* Goal: and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q) *)
    repeat split.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    assert (T19 := (l9_19 A' B' C' Q X')).
    assert (OS A' B' C' Q <-> Out X' C' Q /\ ~ Col A' B' C').
      apply T19.
        eapply l4_13.
          apply H3.
        unfold Cong_3.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        repeat split; assumption.
      apply col_permutation_1.
      apply out_col.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    apply cong_symmetry in H1.
    destruct H14.
(* Goal: not (@Col Tn P O B) *)
    spliter.
    assert (OS A' B' C' Q).
      apply H15.
(* Goal: and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q) *)
      split.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
(* Goal: not (@Col Tn A' B' C') *)
      intro.
      apply H.
      eapply l4_13.
        apply H16.
      unfold Cong_3.
(* Goal: and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q) *)
      repeat split.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
        apply cong_symmetry.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
      apply cong_symmetry.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
    eapply one_side_transitivity.
      apply H7.
    apply one_side_symmetry.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    assumption.
Qed.

Lemma cong_cop_image__col : forall A B P P' X,
 P <> P' -> Reflect P P' A B -> Cong P X P' X -> Coplanar A B P X ->
 Col A B X.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: @Cong Tn P Q P' Q' *)
(* Goal: @Cong Tn P Q P' Q' *)
    unfold Reflect in *.
(* Goal: @Cong Tn P Q P' Q' *)
(* Goal: @Cong Tn P Q P' Q' *)
    induction H0.
(* Goal: not (@Col Tn P O B) *)
      spliter.
      unfold ReflectL in H3.
(* Goal: not (@Col Tn P O B) *)
      spliter.
      ex_and H3 M.
      induction H4.
        induction(eq_dec_points A M).
          subst M.
          assert (Perp P A A B).
            eapply perp_col.
              apply perp_distinct in H4.
(* Goal: not (@Col Tn P O B) *)
              spliter.
(* Goal: not (@Col Tn A' B' C') *)
              intro.
              subst P.
              apply l7_2 in H3.
              apply is_midpoint_id in H3.
              subst P'.
              absurde.
              apply perp_sym.
              apply perp_right_comm.
              apply H4.
(* Goal: not (@Col Tn P O B) *)
            unfold Col.
            right; left.
            apply midpoint_bet.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
          apply perp_comm in H6.
          apply perp_perp_in in H6.
          apply perp_in_comm in H6.
          apply perp_in_per in H6.
          assert (Per X A P).
            unfold Per.
            exists P'.
(* Goal: and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q) *)
            split.
              apply l7_2.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
              assumption.
            Cong.
          apply l8_2 in H6.
          apply col_permutation_2.
          apply (cop_per2__col P).
(* Goal: @Coplanar Tn O B P A *)
(* Goal: not (@Col Tn P O B) *)
            Cop.
(* Goal: not (@Col Tn A' B' C') *)
            intro.
            subst P.
            apply l7_2 in H3.
            apply is_midpoint_id in H3.
            subst P'.
            absurde.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
          assumption.
        assert (Perp P M M A).
          eapply perp_col.
(* Goal: not (@Col Tn A' B' C') *)
            intro.
            subst P.
            apply l7_2 in H3.
            apply is_midpoint_id in H3.
            subst P'.
            absurde.
            apply perp_sym.
            apply perp_comm.
            eapply perp_col.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
              assumption.
              apply H4.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
(* Goal: not (@Col Tn P O B) *)
          unfold Col.
          right; left.
          apply midpoint_bet.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
          assumption.
        apply perp_comm in H7.
        apply perp_perp_in in H7.
        apply perp_in_comm in H7.
        apply perp_in_per in H7.
        assert (Per X M P).
          unfold Per.
          exists P'.
(* Goal: and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q) *)
          split.
            apply l7_2.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
          apply cong_commutativity.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
          assumption.
        apply l8_2 in H7.
        assert (Col A X M).
          assert (P <> M).
(* Goal: not (@Col Tn A' B' C') *)
            intro.
            subst P.
            apply l7_2 in H3.
            apply is_midpoint_id in H3.
            subst P'.
            absurde.
          apply (cop_per2__col P).
(* Goal: @Coplanar Tn O B P A *)
(* Goal: not (@Col Tn P O B) *)
            apply coplanar_perm_2, col_cop__cop with B; Cop.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
            assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
          assumption.
        eapply col_transitivity_1.
          apply H6.
(* Goal: @Col Tn X B Y *)
(* Goal: @Cong Tn B X B Y *)
          apply col_permutation_5.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
          assumption.
(* Goal: @Col Tn X B Y *)
(* Goal: @Cong Tn B X B Y *)
        apply col_permutation_5.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
      subst P'.
      absurde.
(* Goal: not (@Col Tn P O B) *)
    spliter;subst;Col.
Qed.

Lemma cong_cop_per2_1 :
 forall A B X Y, A <> B -> Per A B X -> Per A B Y ->
 Cong B X B Y -> Coplanar A B X Y -> X = Y \/ Midpoint B X Y.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: or (@eq (@Tpoint Tn) X Y) (@Midpoint Tn B X Y) *)
    eapply l7_20.
(* Goal: @Col Tn X B Y *)
(* Goal: @Cong Tn B X B Y *)
      apply col_permutation_5.
(* Goal: @Col Tn X Y B *)
(* Goal: @Cong Tn B X B Y *)
      apply (cop_per2__col A).
(* Goal: @Coplanar Tn O B P A *)
(* Goal: not (@Col Tn P O B) *)
        Cop.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
(* Goal: @Per Tn Y B A *)
(* Goal: @Cong Tn B X B Y *)
        apply l8_2.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
        assumption.
(* Goal: @Per Tn Y B A *)
(* Goal: @Cong Tn B X B Y *)
      apply l8_2.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      assumption.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    assumption.
Qed.

Lemma cong_cop_per2 : forall A B X Y,
 A <> B -> Per A B X -> Per A B Y -> Cong B X B Y -> Coplanar A B X Y ->
 X = Y \/ ReflectL X Y A B.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: or (@eq (@Tpoint Tn) X Y) (@ReflectL Tn X Y A B) *)
    induction (cong_cop_per2_1 A B X Y H H0 H1 H2 H3).
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      left; assumption.
(* Goal: or (@TS Tn O A P B) (@TS Tn O B P A) *)
    right.
    apply is_image_is_image_spec; auto.
(* Goal: @Reflect Tn X Y A B *)
    apply l10_4, cong_midpoint__image; trivial.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    apply per_double_cong with B; assumption.
Qed.

Lemma cong_cop_per2_gen : forall A B X Y,
 A <> B -> Per A B X -> Per A B Y -> Cong B X B Y -> Coplanar A B X Y ->
 X = Y \/ Reflect X Y A B.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: or (@eq (@Tpoint Tn) X Y) (@Reflect Tn X Y A B) *)
    induction (cong_cop_per2 A B X Y H H0 H1 H2 H3).
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
      left; assumption.
(* Goal: or (@TS Tn O A P B) (@TS Tn O B P A) *)
    right.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    apply is_image_is_image_spec; assumption.
Qed.

Lemma ex_perp_cop : forall A B C P,
 A <> B -> exists Q, Perp A B Q C /\ Coplanar A B P Q.
Proof.
(* Goal: forall (A B C P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q)) *)
  intros A B C P HAB.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q)) *)
  destruct (col_dec A B C) as [HCol|HNCol]; [destruct (col_dec A B P) as [|HNCol]|].
  - destruct (not_col_exists A B HAB) as [P' HNCol].
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q)) *)
    destruct (l10_15 A B C P' HCol HNCol) as [Q []].
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q)) *)
    exists Q.
(* Goal: and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q) *)
    split; trivial.
(* Goal: not (@Col Tn P O B) *)
    exists P; left; Col.
  - destruct (l10_15 A B C P HCol HNCol) as [Q []].
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q)) *)
    exists Q.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    split; [|apply os__coplanar]; assumption.
  - destruct (l8_18_existence A B C HNCol) as [Q []].
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q)) *)
    exists Q.
(* Goal: and (@Perp Tn A B Q C) (@Coplanar Tn A B P Q) *)
    split.
(* Goal: @Perp Tn A B Q C *)
(* Goal: @Coplanar Tn A B P Q *)
      Perp.
(* Goal: not (@Col Tn P O B) *)
    exists Q; left; split; Col.
Qed.

Lemma hilbert_s_version_of_pasch_aux : forall A B C I P, Coplanar A B C P ->
  ~ Col A I P -> ~ Col B C P -> Bet B I C -> B <> I -> I <> C -> B <> C ->
  exists X, Col I P X /\
            ((Bet A X B /\ A <> X /\ X <> B /\ A <> B) \/
             (Bet A X C /\ A <> X /\ X <> C /\ A <> C)).
Proof.
(* Goal: forall (A B C I P : @Tpoint Tn) (_ : @Coplanar Tn A B C P) (_ : not (@Col Tn A I P)) (_ : not (@Col Tn B C P)) (_ : @Bet Tn B I C) (_ : not (@eq (@Tpoint Tn) B I)) (_ : not (@eq (@Tpoint Tn) I C)) (_ : not (@eq (@Tpoint Tn) B C)), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn I P X) (or (and (@Bet Tn A X B) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X B)) (not (@eq (@Tpoint Tn) A B))))) (and (@Bet Tn A X C) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X C)) (not (@eq (@Tpoint Tn) A C))))))) *)
intros A B C I P HCop HNC HNC' HBet HBI HIC HBC.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn I P X) (or (and (@Bet Tn A X B) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X B)) (not (@eq (@Tpoint Tn) A B))))) (and (@Bet Tn A X C) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X C)) (not (@eq (@Tpoint Tn) A C))))))) *)
assert (HTS : TS I P B C).
(* Goal: @TS Tn O P A B *)
(* Goal: @TS Tn O B P A *)
  {
(* Goal: @TS Tn I P B C *)
  assert_cols; split; try (intro; apply HNC'; ColR).
(* Goal: and (not (@Col Tn C I P)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T I P) (@Bet Tn B T C))) *)
  split; try (intro; apply HNC'; ColR).
(* Goal: not (@Col Tn P O B) *)
  exists I; Col.
  }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn I P X) (or (and (@Bet Tn A X B) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X B)) (not (@eq (@Tpoint Tn) A B))))) (and (@Bet Tn A X C) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X C)) (not (@eq (@Tpoint Tn) A C))))))) *)
assert (HCop1 : Coplanar A P B I) by (assert_diffs; apply col_cop__cop with C; Cop; Col).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn I P X) (or (and (@Bet Tn A X B) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X B)) (not (@eq (@Tpoint Tn) A B))))) (and (@Bet Tn A X C) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X C)) (not (@eq (@Tpoint Tn) A C))))))) *)
elim (two_sides_dec I P A B); intro HTS'.

(* Goal: @TS Tn O P A B *)
(* Goal: @TS Tn O B P A *)
  {
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn I P X) (or (and (@Bet Tn A X B) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X B)) (not (@eq (@Tpoint Tn) A B))))) (and (@Bet Tn A X C) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X C)) (not (@eq (@Tpoint Tn) A C))))))) *)
  destruct HTS' as [Hc1 [Hc2 [T [HCol HBet']]]].
(* Goal: not (@Col Tn P O B) *)
  exists T; split; Col.
(* Goal: not (@Col Tn P O B) *)
  left; split; Col.
(* Goal: and (not (@eq (@Tpoint Tn) A T)) (and (not (@eq (@Tpoint Tn) T C)) (not (@eq (@Tpoint Tn) A C))) *)
  split; try (intro; treat_equalities; Col).
(* Goal: @Col Tn M P X *)
(* Goal: @Col Tn M P X *)
  split; intro; treat_equalities; Col.
  }

(* Goal: @TS Tn O P A B *)
(* Goal: @TS Tn O B P A *)
  {
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn I P X) (or (and (@Bet Tn A X B) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X B)) (not (@eq (@Tpoint Tn) A B))))) (and (@Bet Tn A X C) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X C)) (not (@eq (@Tpoint Tn) A C))))))) *)
  rename HTS' into HOS.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn I P X) (or (and (@Bet Tn A X B) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X B)) (not (@eq (@Tpoint Tn) A B))))) (and (@Bet Tn A X C) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X C)) (not (@eq (@Tpoint Tn) A C))))))) *)
  assert (HTS' : TS I P A C).
(* Goal: @TS Tn O P A B *)
(* Goal: @TS Tn O B P A *)
    {
(* Goal: not (@Col Tn P O B) *)
    apply l9_8_2 with B; Col.
(* Goal: not (@Col Tn P O B) *)
    unfold TS in HTS; spliter.
(* Goal: @Coplanar Tn O B P A *)
(* Goal: not (@Col Tn P O B) *)
    apply cop__not_two_sides_one_side; Cop.
(* Goal: not (@Col Tn P O B) *)
    intro; apply HOS; apply l9_2; Col.
    }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn I P X) (or (and (@Bet Tn A X B) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X B)) (not (@eq (@Tpoint Tn) A B))))) (and (@Bet Tn A X C) (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) X C)) (not (@eq (@Tpoint Tn) A C))))))) *)
  destruct HTS' as [Hc1 [Hc2 [T [HCol HBet']]]].
(* Goal: not (@Col Tn P O B) *)
  exists T; split; Col.
(* Goal: not (@Col Tn P O B) *)
  right; split; Col.
(* Goal: and (not (@eq (@Tpoint Tn) A T)) (and (not (@eq (@Tpoint Tn) T C)) (not (@eq (@Tpoint Tn) A C))) *)
  split; try (intro; treat_equalities; Col).
(* Goal: @Col Tn M P X *)
(* Goal: @Col Tn M P X *)
  split; intro; treat_equalities; Col.
  }
Qed.

Lemma hilbert_s_version_of_pasch : forall A B C P Q, Coplanar A B C P ->
  ~ Col C Q P -> ~ Col A B P -> BetS A Q B ->
  exists X, Col P Q X /\ (BetS A X C \/ BetS B X C).
Proof.
(* Goal: forall (A B C P Q : @Tpoint Tn) (_ : @Coplanar Tn A B C P) (_ : not (@Col Tn C Q P)) (_ : not (@Col Tn A B P)) (_ : @BetS Tn A Q B), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (or (@BetS Tn A X C) (@BetS Tn B X C))) *)
intros A B C P Q HCop HNC1 HNC2 HAQB.
(* Goal: not (@Col Tn P O B) *)
rewrite BetSEq in HAQB; spliter.
destruct (hilbert_s_version_of_pasch_aux C A B Q P) as [X [HPQX HBetS]]; Cop;
try exists X; try split; Col; do 2 rewrite BetSEq;
induction HBetS; spliter; repeat split; Between.
Qed.


Lemma two_sides_cases : forall O P A B,
 ~ Col O A B -> OS O P A B -> TS O A P B \/ TS O B P A.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
intros.
(* Goal: or (@TS Tn O A P B) (@TS Tn O B P A) *)
assert (HCop := os__coplanar O P A B H0).
(* Goal: or (@TS Tn O A P B) (@TS Tn O B P A) *)
assert(TS O A P B \/ OS O A P B).
(* Goal: @TS Tn O P A B *)
(* Goal: @TS Tn O B P A *)
{
(* Goal: not (@Col Tn P O B) *)
  apply(cop__one_or_two_sides O A P B); Col.
(* Goal: @Coplanar Tn O B P A *)
(* Goal: not (@Col Tn P O B) *)
    Cop.
(* Goal: not (@Col Tn P O B) *)
  unfold OS in H0.
(* Goal: not (@Col Tn P O B) *)
  ex_and H0 R.
(* Goal: not (@Col Tn P O A) *)
  unfold TS in H0.
(* Goal: not (@Col Tn P O B) *)
  spliter.
(* Goal: not (@Col Tn P O B) *)
  Col.
}
(* Goal: or (@TS Tn O A P B) (@TS Tn O B P A) *)
induction H1.
left; auto.
(* Goal: or (@TS Tn O A P B) (@TS Tn O B P A) *)
right.

(* Goal: @TS Tn O B P A *)
assert(TS O B P A \/ OS O B P A).
(* Goal: @TS Tn O P A B *)
(* Goal: @TS Tn O B P A *)
{
(* Goal: not (@Col Tn P O B) *)
  apply(cop__one_or_two_sides O B P A); Col.
(* Goal: @Coplanar Tn O B P A *)
(* Goal: not (@Col Tn P O B) *)
    Cop.
(* Goal: not (@Col Tn P O B) *)
  unfold OS in H0.
(* Goal: not (@Col Tn P O B) *)
  ex_and H0 R.
(* Goal: not (@Col Tn P O B) *)
  unfold TS in H2.
(* Goal: not (@Col Tn P O B) *)
  spliter.
(* Goal: not (@Col Tn P O B) *)
  Col.
}
(* Goal: @TS Tn O B P A *)
induction H2.
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
assumption.
(* Goal: @TS Tn O B P A *)
assert(TS O P A B).
(* Goal: @TS Tn O P A B *)
(* Goal: @TS Tn O B P A *)
{
  apply(l9_31 O A P B); auto.
}
(* Goal: @TS Tn O B P A *)
apply l9_9 in H3.
(* Goal: @TS Tn O B P A *)
contradiction.
Qed.

Lemma not_par_two_sides :
  forall A B C D I, C <> D -> Col A B I -> Col C D I -> ~ Col A B C ->
  exists X, exists Y, Col C D X /\ Col C D Y /\ TS A B X Y.
Proof.
(* Goal: forall (A B C D I : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Col Tn C D X) (and (@Col Tn C D Y) (@TS Tn A B X Y)))) *)
intros A B C D I HCD HCol1 HCol2 HNC.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Col Tn C D X) (and (@Col Tn C D Y) (@TS Tn A B X Y)))) *)
assert (HX : exists X, Col C D X /\ I <> X) by (exists C; split; try intro; treat_equalities; Col).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Col Tn C D X) (and (@Col Tn C D Y) (@TS Tn A B X Y)))) *)
destruct HX as [X [HCol3 HIX]].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Col Tn C D X) (and (@Col Tn C D Y) (@TS Tn A B X Y)))) *)
destruct (symmetric_point_construction X I) as [Y HMid].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Col Tn C D X) (and (@Col Tn C D Y) (@TS Tn A B X Y)))) *)
exists X; exists Y; assert_diffs; assert_cols; do 2 (split; try ColR).
(* Goal: @TS Tn A B X Y *)
split; try (intro; assert (I = X) by (assert_diffs; assert_cols; apply l6_21 with A B C D; Col); Col).
split; try (intro; assert (I = Y) by (assert_diffs; assert_cols; apply l6_21 with A B C D;
                                      Col; ColR); Col).
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A B) (@Bet Tn X T Y)) *)
exists I; unfold Midpoint in HMid; spliter; split; Col; Between.
Qed.

Lemma cop_not_par_other_side :
  forall A B C D I P, C <> D -> Col A B I -> Col C D I -> ~ Col A B C -> ~ Col A B P ->
  Coplanar A B C P ->
  exists Q, Col C D Q /\ TS A B P Q.
Proof.
(* Goal: @Coplanar Tn O B P A *)
(* Goal: not (@Col Tn P O B) *)
intros A B C D I P HCD HCol1 HCol2 HNC1 HNC2 HCop.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
destruct (not_par_two_sides A B C D I HCD HCol1 HCol2 HNC1) as [X [Y [HCol3 [HCol4 HTS]]]].
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
assert (Coplanar A B P X).
(* Goal: @Coplanar Tn A B P X *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
  apply coplanar_trans_1 with C; [Col|Cop|].
  exists I; right; right; split; ColR.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@TS Tn A B P Q)) *)
elim (two_sides_dec A B P X); intro HOS; [exists X; Col|].
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@TS Tn A B P Q)) *)
assert_diffs; apply cop__not_two_sides_one_side in HOS; Col; [|intro; unfold TS in HTS; intuition].
(* Goal: not (@Col Tn P O B) *)
exists Y; split; Col.
(* Goal: not (@Col Tn P O B) *)
apply l9_8_2 with X; [|apply one_side_symmetry]; Col.
Qed.

Lemma cop_not_par_same_side :
  forall A B C D I P, C <> D -> Col A B I -> Col C D I -> ~ Col A B C -> ~ Col A B P ->
  Coplanar A B C P ->
  exists Q, Col C D Q /\ OS A B P Q.
Proof.
(* Goal: @Coplanar Tn O B P A *)
(* Goal: not (@Col Tn P O B) *)
intros A B C D I P HCD HCol1 HCol2 HNC1 HNC2 HCop.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
destruct (not_par_two_sides A B C D I HCD HCol1 HCol2 HNC1) as [X [Y [HCol3 [HCol4 HTS]]]].
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
assert (Coplanar A B P X).
(* Goal: @Coplanar Tn A B P X *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
  apply coplanar_trans_1 with C; [Col|Cop|].
  exists I; right; right; split; ColR.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
elim (one_side_dec A B P X); intro HTS2; [exists X; Col|].
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
assert_diffs; apply cop__not_one_side_two_sides in HTS2; Col; [|intro; unfold TS in HTS; intuition].
(* Goal: not (@Col Tn P O B) *)
exists Y; split; Col.
(* Goal: @OS Tn A B P Y *)
exists X; split; Side.
Qed.

End T10_1.

Section T10_2D.

(* Goal: @TS Tn O P A B *)
(* Goal: @TS Tn O B P A *)
Context `{T2D:Tarski_2D}.

Lemma all_coplanar : forall A B C D, Coplanar A B C D.
Proof.
apply upper_dim_implies_all_coplanar;
(* Goal: @upper_dim_axiom Tn *)
unfold upper_dim_axiom; apply upper_dim.
Qed.

Lemma per2__col : forall A B C X, Per A X C -> X <> C -> Per B X C -> Col A B X.
Proof.
apply upper_dim_implies_per2__col;
(* Goal: @upper_dim_axiom Tn *)
unfold upper_dim_axiom; apply upper_dim.
Qed.

Lemma perp2__col : forall X Y Z A B,
 Perp X Y A B -> Perp X Z A B -> Col X Y Z.
Proof.
(* Goal: forall (X Y Z A B : @Tpoint Tn) (_ : @Perp Tn X Y A B) (_ : @Perp Tn X Z A B), @Col Tn X Y Z *)
    intros X Y Z A B.
(* Goal: forall (_ : @Perp Tn X Y A B) (_ : @Perp Tn X Z A B), @Col Tn X Y Z *)
    apply cop_perp2__col, all_coplanar.
Qed.

Lemma cong_on_bissect : forall A B M P X,
 Midpoint M A B -> Perp_at M A B P M -> Cong X A X B ->
 Col M P X.
Proof.
(* Goal: forall (A B M P X : @Tpoint Tn) (_ : @Cong Tn A X B X) (_ : @Midpoint Tn M A B) (_ : @Perp Tn A B P M), @Col Tn M P X *)
intros A B M P X.
(* Goal: forall (_ : @Midpoint Tn M A B) (_ : @Perp_at Tn M A B P M) (_ : @Cong Tn X A X B), @Col Tn M P X *)
apply cop__cong_on_bissect, all_coplanar.
Qed.

Lemma cong_mid_perp__col : forall A B M P X, Cong A X B X -> Midpoint M A B -> Perp A B P M -> Col M P X.
Proof.
(* Goal: forall (A B M P X : @Tpoint Tn) (_ : @Cong Tn A X B X) (_ : @Midpoint Tn M A B) (_ : @Perp Tn A B P M), @Col Tn M P X *)
intros A B M P X.
(* Goal: forall (_ : @Cong Tn A X B X) (_ : @Midpoint Tn M A B) (_ : @Perp Tn A B P M), @Col Tn M P X *)
apply cong_cop_mid_perp__col, all_coplanar.
Qed.

Lemma image_in_col : forall A B P P' Q Q' M,
 ReflectL_at M P P' A B -> ReflectL_at M Q Q' A B ->
 Col M P Q.
Proof.
(* Goal: forall (A B P P' Q Q' M : @Tpoint Tn) (_ : @ReflectL_at Tn M P P' A B) (_ : @ReflectL_at Tn M Q Q' A B), @Col Tn M P Q *)
intros A B P P' Q Q' M.
(* Goal: forall (_ : @ReflectL_at Tn M P P' A B) (_ : @ReflectL_at Tn M Q Q' A B), @Col Tn M P Q *)
apply cop__image_in_col, all_coplanar.
Qed.

Lemma cong_image__col : forall A B P P' X,
 P <> P' -> Reflect P P' A B -> Cong P X P' X ->
 Col A B X.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: @Col Tn A B X *)
    assert (HCop := all_coplanar A B P X).
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    apply cong_cop_image__col with P P'; assumption.
Qed.

Lemma cong_per2_1 :
 forall A B X Y, A <> B -> Per A B X -> Per A B Y ->
 Cong B X B Y -> X = Y \/ Midpoint B X Y.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: or (@eq (@Tpoint Tn) X Y) (@Reflect Tn X Y A B) *)
    assert (HCop := all_coplanar A B X Y).
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    apply (cong_cop_per2_1 A); assumption.
Qed.


Lemma cong_per2 : forall A B X Y,
 A <> B -> Per A B X -> Per A B Y -> Cong B X B Y ->
 X = Y \/ ReflectL X Y A B.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: or (@eq (@Tpoint Tn) X Y) (@Reflect Tn X Y A B) *)
    assert (HCop := all_coplanar A B X Y).
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    apply cong_cop_per2; assumption.
Qed.

Lemma cong_per2_gen : forall A B X Y,
 A <> B -> Per A B X -> Per A B Y -> Cong B X B Y ->
 X = Y \/ Reflect X Y A B.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
    intros.
(* Goal: or (@eq (@Tpoint Tn) X Y) (@Reflect Tn X Y A B) *)
    assert (HCop := all_coplanar A B X Y).
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
    apply cong_cop_per2_gen; assumption.
Qed.

Lemma not_two_sides_one_side :
 forall A B X Y,
  ~ Col X A B ->
  ~ Col Y A B ->
  ~ TS A B X Y ->
  OS A B X Y.
Proof.
(* Goal: forall (A B X Y : @Tpoint Tn) (_ : not (@Col Tn X A B)) (_ : not (@Col Tn Y A B)) (_ : not (@TS Tn A B X Y)), @OS Tn A B X Y *)
intros A B X Y.
(* Goal: forall (_ : not (@Col Tn X A B)) (_ : not (@Col Tn Y A B)) (_ : not (@TS Tn A B X Y)), @OS Tn A B X Y *)
apply cop__not_two_sides_one_side, all_coplanar.
Qed.

Lemma col_perp2__col :
 forall A B X Y P,
  Col A B P ->
  Perp A B X P ->
  Perp P A Y P ->
  Col Y X P.
Proof.
apply upper_dim_implies_col_perp2__col;
(* Goal: @upper_dim_axiom Tn *)
unfold upper_dim_axiom; apply upper_dim.
Qed.

Lemma hilbert_s_version_of_pasch_2D : forall A B C P Q,
  ~ Col C Q P -> ~ Col A B P -> BetS A Q B ->
  exists X, Col P Q X /\ (BetS A X C \/ BetS B X C).
Proof.
(* Goal: forall (A B C P Q : @Tpoint Tn) (_ : not (@Col Tn C Q P)) (_ : not (@Col Tn A B P)) (_ : @BetS Tn A Q B), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (or (@BetS Tn A X C) (@BetS Tn B X C))) *)
intros A B C P Q.
(* Goal: forall (_ : not (@Col Tn C Q P)) (_ : not (@Col Tn A B P)) (_ : @BetS Tn A Q B), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn P Q X) (or (@BetS Tn A X C) (@BetS Tn B X C))) *)
apply hilbert_s_version_of_pasch, all_coplanar.
Qed.

Lemma not_one_side_two_sides :
 forall A B X Y,
  ~ Col X A B ->
  ~ Col Y A B ->
  ~ OS A B X Y ->
  TS A B X Y.
Proof.
(* Goal: forall (A B X Y : @Tpoint Tn) (_ : not (@Col Tn X A B)) (_ : not (@Col Tn Y A B)) (_ : not (@OS Tn A B X Y)), @TS Tn A B X Y *)
apply upper_dim_implies_not_one_side_two_sides.
(* Goal: @upper_dim_axiom Tn *)
unfold upper_dim_axiom; apply upper_dim.
Qed.

Lemma one_or_two_sides :
 forall A B X Y,
  ~ Col X A B ->
  ~ Col Y A B ->
  TS A B X Y \/ OS A B X Y.
Proof.
(* Goal: forall (A B X Y : @Tpoint Tn) (_ : not (@Col Tn X A B)) (_ : not (@Col Tn Y A B)), or (@TS Tn A B X Y) (@OS Tn A B X Y) *)
apply upper_dim_implies_one_or_two_sides.
(* Goal: @upper_dim_axiom Tn *)
unfold upper_dim_axiom; apply upper_dim.
Qed.

Lemma not_par_other_side :
  forall A B C D I P, C <> D -> Col A B I -> Col C D I -> ~ Col A B C -> ~ Col A B P ->
  exists Q, Col C D Q /\ TS A B P Q.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
assert (HCop := all_coplanar A B C P).
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
apply cop_not_par_other_side with I; assumption.
Qed.

Lemma not_par_same_side :
  forall A B C D I P, C <> D -> Col A B I -> Col C D I -> ~ Col A B C -> ~ Col A B P ->
  exists Q, Col C D Q /\ OS A B P Q.
Proof.
(* Goal: forall (A B C D I P : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C D)) (_ : @Col Tn A B I) (_ : @Col Tn C D I) (_ : not (@Col Tn A B C)) (_ : not (@Col Tn A B P)), @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Col Tn C D Q) (@OS Tn A B P Q)) *)
assert (HCop := all_coplanar A B C P).
(* Goal: @TS Tn O B P A *)
(* Goal: @TS Tn O B P A *)
apply cop_not_par_same_side with I; assumption.
Qed.

End T10_2D.

Hint Resolve all_coplanar : cop.