Require Export GeoCoq.Tarski_dev.Ch09_plane.
Require Export GeoCoq.Tarski_dev.Tactics.CoincR_for_cop.

Ltac CopR :=
 let tpoint := constr:(Tpoint) in
 let col := constr:(Col) in
 let cop := constr:(Coplanar) in
   assert_ncols; Cop_refl tpoint col cop.

Section T10.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma ex_sym : forall A B X, exists Y, (Perp A B X Y \/ X = Y) /\
   (exists M, Col A B M /\ Midpoint M X Y).
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
    induction (col_dec A B X).
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 X X) (@Col Tn A B X0)) *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
      exists X.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        right.
(* Goal: @eq (@Tpoint Tn) X X *)
        reflexivity.
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 X X) (@Col Tn A B X0)) *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
      exists X.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @Midpoint Tn X X X *)
(* Goal: @Col Tn A B X *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
      apply l7_3_2.
    assert (exists M, Col A B M /\ Perp A B X M).
      apply l8_18_existence.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    ex_and H0 M0.
    double X M0 Z.
    exists Z.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      left.
(* Goal: @Perp Tn A B X Y *)
      apply perp_sym.
      eapply perp_col.
        intro.
        subst Z.
        apply l7_3 in H2.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
        apply perp_distinct in H1.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        absurde.
(* Goal: @Perp Tn A B X Y *)
        apply perp_sym.
        apply H1.
      unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      left.
      apply midpoint_bet.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X P' P) (@Col Tn B A X)) *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
    exists M0.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma is_image_is_image_spec : forall P P' A B, A<>B -> (Reflect P' P A B <-> ReflectL P' P A B).
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @Reflect Tn A B' C D *)
    unfold Reflect.
(* Goal: or (and (not (@eq (@Tpoint Tn) C D)) (@ReflectL Tn A B' C D)) (and (@eq (@Tpoint Tn) C D) (@Midpoint Tn C B' A)) *)
    tauto.
Qed.

Lemma ex_sym1 : forall A B X, A<>B -> exists Y, (Perp A B X Y \/ X = Y) /\
 (exists M, Col A B M /\ Midpoint M X Y /\ Reflect X Y A B).
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
    induction (col_dec A B X).
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 X X) (@Col Tn A B X0)) *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
      exists X.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        right.
(* Goal: @eq (@Tpoint Tn) X X *)
        reflexivity.
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 X X) (@Col Tn A B X0)) *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
      exists X.
      rewrite -> (is_image_is_image_spec) by apply H.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: @Midpoint Tn X X X *)
(* Goal: @Col Tn A B X *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
        apply l7_3_2.
(* Goal: @ReflectL Tn X X A B *)
      unfold ReflectL.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 X X) (@Col Tn A B X0)) *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
        exists X.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
        split.
(* Goal: @Midpoint Tn X X X *)
(* Goal: @Col Tn A B X *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
          apply l7_3_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      right.
(* Goal: @eq (@Tpoint Tn) X X *)
      reflexivity.
    assert (exists M, Col A B M /\ Perp A B X M).
      apply l8_18_existence.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    ex_and H1 M0.
    double X M0 Z.
    exists Z.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      left.
(* Goal: @Perp Tn A B X Y *)
      apply perp_sym.
      eapply perp_col.
        intro.
        subst Z.
        apply l7_3 in H3.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
        apply perp_distinct in H2.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        absurde.
(* Goal: @Perp Tn A B X Y *)
        apply perp_sym.
        apply H2.
      unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      left.
      apply midpoint_bet.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X P' P) (@Col Tn B A X)) *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
    exists M0.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    rewrite -> (is_image_is_image_spec) by apply H.
(* Goal: @ReflectL Tn X X A B *)
    unfold ReflectL.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X P' P) (@Col Tn B A X)) *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
      exists M0.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    left.
(* Goal: @Perp Tn A B X Y *)
    apply perp_sym.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
    apply perp_left_comm.
    eapply perp_col.
      intro.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
      subst X.
      apply l7_3 in H3.
      subst Z.
      apply perp_distinct in H2.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
      absurde.
(* Goal: @Perp Tn A B X Y *)
      apply perp_sym.
      apply H2.
    unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    left.
    apply midpoint_bet.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma l10_2_uniqueness : forall A B P P1 P2,
 Reflect P1 P A B -> Reflect P2 P A B -> P1=P2.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @Reflect Tn Y X A B *)
    induction (eq_dec_points A B).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      subst.
(* Goal: @Reflect Tn P P' B A *)
      unfold Reflect in *.
(* Goal: or (and (not (@eq (@Tpoint Tn) B A)) (@ReflectL Tn P P' B A)) (and (@eq (@Tpoint Tn) B A) (@Midpoint Tn B P' P)) *)
      induction H.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        intuition.
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
      induction H0.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        intuition.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
      eapply symmetric_point_uniqueness with P B;auto.
    rewrite -> (is_image_is_image_spec) in * by apply H1.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    unfold ReflectL in *.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter.
(* Goal: and (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X P P') (@Col Tn A B X))) (or (@Perp Tn A B P P') (@eq (@Tpoint Tn) P P')) *)
    ex_and H X.
    ex_and H0 Y.
    induction H2; induction H3.
      assert (P <> X).
        intro.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
        apply is_midpoint_id in H.
        subst P1.
        apply perp_distinct in H3.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        absurde.
      assert (P <> Y).
        intro.
        subst Y.
        apply is_midpoint_id in H0.
        subst P2.
        apply perp_distinct in H2.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        absurde.
      assert (Perp P X A B).
        eapply perp_col.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
          apply H3.
        unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        right; left.
        apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      assert (Perp P Y A B).
        eapply perp_col.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
          apply H2.
        unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        right; left.
        apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      induction (eq_dec_points X A).
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
        assert (~ Col A B P /\ Per P A B).
          eapply l8_16_1.
            apply col_trivial_3.
            apply col_trivial_2.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
            auto.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        assert (Y = A).
          eapply l8_18_uniqueness.
            apply H10.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
(* Goal: @Perp Tn A B X Y *)
            apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
            apply col_trivial_3.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        subst Y.
        eapply symmetric_point_uniqueness.
          apply H.
        apply H0.
      assert (~ Col A B P /\ Per P X A).
        eapply l8_16_1.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
          apply col_trivial_3.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
          auto.
(* Goal: @Perp Tn A B X Y *)
        apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
      assert (Y = X).
        eapply l8_18_uniqueness.
          apply H11.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @Perp Tn A B X Y *)
        apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      subst Y.
      eapply symmetric_point_uniqueness.
        apply H.
      apply H0.
      subst P1.
      assert (P <> Y).
        intro.
        subst Y.
        apply l7_3 in H.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
        apply is_midpoint_id in H0.
        subst P2.
        eapply perp_distinct in H2.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        absurde.
      assert (Perp P Y A B).
        eapply perp_col.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
          apply H2.
        unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        right; left.
        apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      apply l7_3 in H.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
      subst X.
      induction (eq_dec_points Y A).
        subst Y.
        assert (~ Col A B P /\ Per P A B).
          eapply l8_16_1.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
            apply col_trivial_2.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
            auto; auto.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
(* Goal: @Midpoint Tn A P' P *)
(* Goal: @Midpoint Tn A P' P *)
        contradiction.
      assert (~ Col A B P /\ Per P Y A).
        eapply l8_16_1.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
          apply col_trivial_3.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
          auto.
(* Goal: @Perp Tn A B X Y *)
        apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
(* Goal: @Midpoint Tn A P' P *)
(* Goal: @Midpoint Tn A P' P *)
      contradiction.
      subst P2.
      assert (P <> X).
        intro.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
        apply l7_3 in H0.
        subst Y.
        apply is_midpoint_id in H.
        subst P1.
        eapply perp_distinct in H3.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        absurde.
      assert (Perp P X A B).
        eapply perp_col.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
          apply H3.
        unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        right; left.
        apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      apply l7_3 in H0.
      subst Y.
      induction (eq_dec_points X A).
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
        assert (~ Col A B P /\ Per P A B).
          eapply l8_16_1.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
            apply col_trivial_2.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
            auto.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
(* Goal: @Midpoint Tn A P' P *)
(* Goal: @Midpoint Tn A P' P *)
        contradiction.
      assert (~ Col A B P /\ Per P X A).
        eapply l8_16_1.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
          apply col_trivial_3.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
          auto.
(* Goal: @Perp Tn A B X Y *)
        apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
(* Goal: @Midpoint Tn A P' P *)
(* Goal: @Midpoint Tn A P' P *)
      contradiction.
    subst P1.
    subst P2.
(* Goal: @eq (@Tpoint Tn) X X *)
    reflexivity.
Qed.

Lemma l10_2_uniqueness_spec : forall A B P P1 P2,
 ReflectL P1 P A B -> ReflectL P2 P A B -> P1=P2.
Proof.
(* Goal: forall (A B P P1 P2 : @Tpoint Tn) (_ : @ReflectL Tn P P1 A B) (_ : @ReflectL Tn P P2 A B), @eq (@Tpoint Tn) P1 P2 *)
    intros A B P P1 P2 HP1 HP2.
(* Goal: @eq (@Tpoint Tn) P1 P2 *)
    assert (HR1 := HP1).
(* Goal: @eq (@Tpoint Tn) P1 P2 *)
    assert (HR2 := HP2).
(* Goal: @eq (@Tpoint Tn) P1 P2 *)
    destruct HR1 as [HX1 [HPerp|Heq1]].
(* Goal: @Midpoint Tn A P' P *)
      assert_diffs; apply (l10_2_uniqueness A B P); apply is_image_is_image_spec; assumption.
(* Goal: @eq (@Tpoint Tn) P1 P2 *)
    destruct HR2 as [HX2 [HPerp|Heq2]].
(* Goal: @Midpoint Tn A P' P *)
      assert_diffs; apply (l10_2_uniqueness A B P); apply is_image_is_image_spec; assumption.
(* Goal: @eq (@Tpoint Tn) P1 P2 *)
   congruence.
Qed.

Lemma l10_2_existence_spec : forall A B P,
 exists P', ReflectL P' P A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
    induction (col_dec A B P).
(* Goal: @ReflectL Tn X X A B *)
      unfold ReflectL.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @Reflect Tn P' P A B) *)
      exists P.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @Reflect Tn P' P A B) *)
        exists P.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
        split.
(* Goal: @Midpoint Tn X X X *)
(* Goal: @Col Tn A B X *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
          apply l7_3_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      right.
(* Goal: @eq (@Tpoint Tn) X X *)
      reflexivity.
    assert (exists X, Col A B X /\ Perp A B P X).
      eapply l8_18_existence.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    ex_and H0 X.
    double P X P'.
(* Goal: @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => @Reflect Tn P' P A B) *)
    exists P'.
(* Goal: @ReflectL Tn X X A B *)
    unfold ReflectL.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 X X) (@Col Tn A B X0)) *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
      exists X.
(* Goal: @Midpoint Tn A P' P *)
      split; assumption.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    left.
(* Goal: @Perp Tn A B X Y *)
    apply perp_sym.
    eapply perp_col.
      intro.
      subst P'.
      apply l7_3 in H2.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
      subst X.
      apply perp_distinct in H1.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
      absurde.
(* Goal: @Perp Tn A B X Y *)
      apply perp_sym.
      apply H1.
    unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    left.
    apply midpoint_bet.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma l10_2_existence : forall A B P,
 exists P', Reflect P' P A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @Reflect Tn Y X A B *)
    induction (eq_dec_points A B).
(* Goal: @Reflect Tn P' P A B *)
(* Goal: @Reflect Tn P' P A B *)
      subst B.
(* Goal: @Reflect Tn A B' C D *)
      unfold Reflect.
(* Goal: @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => or (and (not (@eq (@Tpoint Tn) A A)) (@ReflectL Tn P' P A A)) (and (@eq (@Tpoint Tn) A A) (@Midpoint Tn A P P'))) *)
(* Goal: @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => @Reflect Tn P' P A B) *)
      elim (symmetric_point_construction P A).
(* Goal: forall (x : @Tpoint Tn) (_ : @Midpoint Tn A P x), @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => or (and (not (@eq (@Tpoint Tn) A A)) (@ReflectL Tn P' P A A)) (and (@eq (@Tpoint Tn) A A) (@Midpoint Tn A P P'))) *)
(* Goal: @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => @Reflect Tn P' P A B) *)
      intros P'.
(* Goal: @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => @Reflect Tn P' P A B) *)
      exists P'.
(* Goal: or (and (not (@eq (@Tpoint Tn) C D)) (@ReflectL Tn A B' C D)) (and (@eq (@Tpoint Tn) C D) (@Midpoint Tn C B' A)) *)
      tauto.
(* Goal: @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => @Reflect Tn P' P A B) *)
    elim (l10_2_existence_spec A B P).
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros P'; intros.
(* Goal: @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => @Reflect Tn P' P A B) *)
    exists P'.
(* Goal: @Reflect Tn A B' C D *)
    unfold Reflect.
(* Goal: or (and (not (@eq (@Tpoint Tn) C D)) (@ReflectL Tn A B' C D)) (and (@eq (@Tpoint Tn) C D) (@Midpoint Tn C B' A)) *)
    tauto.
Qed.

Lemma l10_4_spec : forall A B P P',
 ReflectL P P' A B ->
 ReflectL P' P A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    unfold ReflectL in *.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter.
(* Goal: and (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X P P') (@Col Tn A B X))) (or (@Perp Tn A B P P') (@eq (@Tpoint Tn) P P')) *)
    ex_and H X.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 X X) (@Col Tn A B X0)) *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
      exists X.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
    induction H0.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      left.
(* Goal: @Perp Tn A B P P' *)
(* Goal: or (@Perp Tn A B P P') (@eq (@Tpoint Tn) P P') *)
      apply perp_right_comm.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
    auto.
Qed.

Lemma l10_4 : forall A B P P', Reflect P P' A B -> Reflect P' P A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @Reflect Tn Y X A B *)
    induction (eq_dec_points A B).
(* Goal: @Reflect Tn P' P A B *)
(* Goal: @Reflect Tn P' P A B *)
      subst B.
(* Goal: @Reflect Tn P P' B A *)
      unfold Reflect in *.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      elim H;intros.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        intuition.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      right.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
      apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    rewrite -> (is_image_is_image_spec) in * by apply H0.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
    apply l10_4_spec;auto.
Qed.

Lemma l10_5 : forall A B P P' P'',
 Reflect P' P A B ->
 Reflect P'' P' A B -> P=P''.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @Reflect Tn Y X A B *)
    induction (eq_dec_points A B).
(* Goal: @Reflect Tn P P' B A *)
      unfold Reflect in *.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      subst.
(* Goal: or (and (not (@eq (@Tpoint Tn) B A)) (@ReflectL Tn P P' B A)) (and (@eq (@Tpoint Tn) B A) (@Midpoint Tn B P' P)) *)
      induction H.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        intuition.
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
      induction H0.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        intuition.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
      apply symmetric_point_uniqueness with P' B.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    rewrite -> (is_image_is_image_spec) in * by apply H1.
    eapply l10_2_uniqueness.
      eapply l10_4.
      apply is_image_is_image_spec.
        apply H1.
      apply H.
    apply is_image_is_image_spec.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma l10_6_uniqueness : forall A B P P1 P2, Reflect P P1 A B -> Reflect P P2 A B -> P1 = P2.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @Reflect Tn Y X A B *)
    induction (eq_dec_points A B).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      subst.
(* Goal: @Reflect Tn P P' B A *)
      unfold Reflect in *.
(* Goal: or (and (not (@eq (@Tpoint Tn) B A)) (@ReflectL Tn P P' B A)) (and (@eq (@Tpoint Tn) B A) (@Midpoint Tn B P' P)) *)
      induction H.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        intuition.
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
      induction H0.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        intuition.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
      apply symmetric_point_uniqueness with P B.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
      apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    eapply l10_2_uniqueness.
(* Goal: @Reflect Tn P' P A B *)
      apply l10_4.
      apply H.
(* Goal: @Reflect Tn P' P A B *)
    apply l10_4.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma l10_6_uniqueness_spec : forall A B P P1 P2, ReflectL P P1 A B -> ReflectL P P2 A B -> P1 = P2.
Proof.
(* Goal: forall (A B P P1 P2 : @Tpoint Tn) (_ : @ReflectL Tn P P1 A B) (_ : @ReflectL Tn P P2 A B), @eq (@Tpoint Tn) P1 P2 *)
    intros A B P P1 P2 HP1 HP2.
(* Goal: @eq (@Tpoint Tn) P1 P2 *)
    assert (HR1 := HP1).
(* Goal: @eq (@Tpoint Tn) P1 P2 *)
    assert (HR2 := HP2).
(* Goal: @eq (@Tpoint Tn) P1 P2 *)
    destruct HR1 as [HX1 [HPerp|Heq1]].
(* Goal: @Midpoint Tn A P' P *)
      assert_diffs; apply (l10_6_uniqueness A B P); apply is_image_is_image_spec; assumption.
(* Goal: @eq (@Tpoint Tn) P1 P2 *)
    destruct HR2 as [HX2 [HPerp|Heq2]].
(* Goal: @Midpoint Tn A P' P *)
      assert_diffs; apply (l10_6_uniqueness A B P); apply is_image_is_image_spec; assumption.
(* Goal: @eq (@Tpoint Tn) X X *)
    subst; reflexivity.
Qed.

Lemma l10_6_existence_spec : forall A B P', A<>B -> exists P, ReflectL P' P A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ReflectL Tn P' P A B) *)
    assert (exists P, ReflectL P P' A B).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ReflectL Tn P P' A B) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ReflectL Tn P' P A B) *)
      eapply l10_2_existence_spec.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ReflectL Tn P' P A B) *)
    ex_and H0 P.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @Reflect Tn P' P A B) *)
    exists P.
(* Goal: @ReflectL Tn P' P A B *)
    apply l10_4_spec.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma l10_6_existence : forall A B P', exists P, Reflect P' P A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @Reflect Tn P' P A B) *)
    assert (exists P, Reflect P P' A B).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @Reflect Tn P P' A B) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @Reflect Tn P' P A B) *)
      eapply l10_2_existence.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @Reflect Tn P' P A B) *)
    ex_and H P.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @Reflect Tn P' P A B) *)
    exists P.
(* Goal: @Reflect Tn P' P A B *)
    apply l10_4.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma l10_7 : forall A B P P' Q Q',
 Reflect P' P A B -> Reflect Q' Q A B ->
  P'=Q' -> P = Q.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
    subst Q'.
    eapply l10_2_uniqueness.
(* Goal: @Reflect Tn P' P A B *)
      apply l10_4.
      apply H.
(* Goal: @Reflect Tn P' P A B *)
    apply l10_4.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma l10_8 : forall A B P, Reflect P P A B -> Col P A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @Reflect Tn Y X A B *)
    induction (eq_dec_points A B).
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
      subst;Col.
(* Goal: @Col Tn P A B *)
    unfold Reflect in H.
(* Goal: @Col Tn P A B *)
    unfold ReflectL in H.
(* Goal: or (and (not (@eq (@Tpoint Tn) B A)) (@ReflectL Tn P P' B A)) (and (@eq (@Tpoint Tn) B A) (@Midpoint Tn B P' P)) *)
    induction H.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
      ex_and H1 X.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
      apply l7_3 in H1.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
      subst X.
(* Goal: @Col Tn B B A *)
      Col.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter. subst. Col.
Qed.

Lemma col__refl : forall A B P, Col P A B -> ReflectL P P A B.
Proof.
(* Goal: @Col Tn B B A *)
    intros A B P HCol.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X P P) (@Col Tn A B X)) *)
(* Goal: or (@Perp Tn A B P P) (@eq (@Tpoint Tn) P P) *)
      exists P; repeat split; finish; Between.
(* Goal: @eq (@Tpoint Tn) X X *)
    right; reflexivity.
Qed.


(** Here we need the assumption that A<>B *)
Lemma is_image_col_cong : forall A B P P' X, A<>B ->
 Reflect P P' A B -> Col A B X -> Cong P X P' X.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
    rewrite is_image_is_image_spec in H0 by apply H.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    unfold ReflectL in *.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter.
    ex_and H0 M0.
    induction H2.
      assert (HH:= H2).
      apply perp_distinct in HH.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
      induction (eq_dec_points M0 X).
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
        unfold Midpoint in *.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        Cong.
      assert (Perp M0 X P' P).
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
        eapply perp_col2;eauto.
      assert(~ Col A B P /\ Per P M0 X).
        eapply l8_16_1.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
          auto.
(* Goal: @Perp Tn A B X Y *)
        apply perp_sym.
        eapply perp_col.
          intro.
          subst P.
          apply l7_2 in H0.
          apply is_midpoint_id in H0.
          subst P'.
          absurde.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
          apply perp_left_comm.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
          apply H2; eapply perp_left_comm.
        unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        right; left.
        apply midpoint_bet.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
      eapply l8_2 in H9.
      unfold Per in H9.
      ex_and H9 P0.
      assert (P0 = P').
        eapply symmetric_point_uniqueness.
          apply H9.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      subst P0.
      apply cong_commutativity.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    subst P'.
(* Goal: @eq (@Tpoint Tn) X X *)
    apply cong_reflexivity.
Qed.

Lemma is_image_spec_col_cong : forall A B P P' X,
 ReflectL P P' A B -> Col A B X -> Cong P X P' X.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    unfold ReflectL in *.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X P' P) (@Col Tn B A X)) *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
    ex_and H M0.
    induction H1.
      assert (HH:= H1).
      apply perp_distinct in HH.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
      induction (eq_dec_points M0 X).
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
        unfold Midpoint in *.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        Cong.
      assert (Perp M0 X P' P) by (eauto using perp_col2).
      assert(~ Col A B P /\ Per P M0 X).
        eapply l8_16_1.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
          auto.
(* Goal: @Perp Tn A B X Y *)
        apply perp_sym.
        eapply perp_col.
          intro.
          subst P.
          apply l7_2 in H.
          apply is_midpoint_id in H.
          subst P'.
          absurde.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
          apply perp_left_comm.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
          apply H1; eapply perp_left_comm.
        unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        right; left.
        apply midpoint_bet.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
      eapply l8_2 in H8.
      unfold Per in H8.
      ex_and H8 P0.
      assert (P0 = P').
        eapply symmetric_point_uniqueness.
          apply H8.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      subst P0.
      Cong.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    subst.
    Cong.
Qed.

Lemma image_id : forall A B T T',
  A<>B ->
  Col A B T ->
  Reflect T T' A B ->
  T = T'.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
    rewrite is_image_is_image_spec in H1 by apply H.
    unfold ReflectL in H1.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
    ex_and H1 X.
    induction H2.
      assert (A <> B /\ T' <> T).
        apply perp_distinct in H2.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
(* Goal: @Midpoint Tn A P' P *)
        split; assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
      induction (eq_dec_points A X).
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
        assert (Perp A B T' A).
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
          eapply perp_col.
            intro.
            subst T'.
            apply is_midpoint_id in H1.
            subst A.
            absurde.
(* Goal: @Perp Tn A B X Y *)
            apply perp_sym.
            apply H2.
          unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
          right; left.
          apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
          apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        assert (~ Col  A T' B).
          apply perp_not_col.
          apply perp_comm.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        assert (A = T).
(* Goal: @Col Tn B B A *)
          apply l6_21 with A T' B T; assert_cols; Col.
(* Goal: @Col Tn B B A *)
          intro; treat_equalities; Col.
        subst A.
        apply l7_2 in H1.
        apply is_midpoint_id in H1.
        subst T'.
        absurde.
      induction (eq_dec_points B X).
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
        assert (Perp A B T' B).
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
          eapply perp_col.
            intro.
            subst T'.
            apply is_midpoint_id in H1.
(* Goal: @Reflect Tn P' P A B *)
(* Goal: @Reflect Tn P' P A B *)
            subst B.
            absurde.
(* Goal: @Perp Tn A B X Y *)
            apply perp_sym.
            apply H2.
          unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
          right; left.
          apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
          apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        assert (~ Col  B T' A).
          apply perp_not_col.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
          apply perp_left_comm.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        assert (B = T).
          eapply l6_21.
            apply H8.
            apply H4.
            apply col_trivial_3.
            unfold Col.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
            right; right.
            apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
            apply l7_2.
            apply H1.
            apply col_trivial_2.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
(* Goal: @Reflect Tn P' P A B *)
(* Goal: @Reflect Tn P' P A B *)
        subst B.
        apply l7_2 in H1.
        apply is_midpoint_id in H1.
        subst T'.
        absurde.
      assert (Col A X T) by ColR.
      assert (Perp A B T' X).
(* Goal: @Perp Tn A B X Y *)
        apply perp_sym.
        eapply perp_col.
          intro.
          subst T'.
          apply is_midpoint_id in H1.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
          subst X.
          absurde.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
          apply H2.
(* Goal: @Col Tn P P' Y *)
        assert_cols.
(* Goal: @Col Tn B B A *)
        Col.
      assert (~ Col  X T' A).
        apply perp_not_col.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
        apply perp_left_comm.
(* Goal: @Perp Tn A B X Y *)
        apply perp_sym.
        eapply perp_col.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
          apply H9.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      assert (X = T).
        eapply l6_21.
          apply H10.
          apply H6.
          apply col_trivial_3.
          unfold Col.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
          right; right.
          apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
          apply l7_2.
          apply H1.
          apply col_trivial_2.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
      subst X.
      apply l7_2 in H1.
      apply is_midpoint_id in H1.
      subst T'.
      absurde.
    subst T'.
(* Goal: @eq (@Tpoint Tn) X X *)
    reflexivity.
Qed.

Lemma osym_not_col : forall A B P P',
 Reflect P P' A B ->
 ~ Col A B P -> ~ Col A B P'.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @Reflect Tn P P' B A *)
    unfold Reflect in *.
(* Goal: or (and (not (@eq (@Tpoint Tn) B A)) (@ReflectL Tn P P' B A)) (and (@eq (@Tpoint Tn) B A) (@Midpoint Tn B P' P)) *)
    induction H.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
      assert ( HH:= H1).
      unfold ReflectL in HH.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
      ex_and H2 T.
      intro.
      induction H3.
        assert (P'=P).
          eapply image_id.
            apply H.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
(* Goal: @Reflect Tn P' P A B *)
          apply l10_4.
          apply is_image_is_image_spec.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        subst P'.
        apply perp_distinct in H3.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        absurde.
      apply H0.
      subst P'.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter. subst. Col5.
Qed.

Lemma midpoint_preserves_image : forall A B P P' Q Q' M,
 A <> B -> Col A B M -> Reflect P P' A B ->
 Midpoint M P Q -> Midpoint M P' Q' -> Reflect Q Q' A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
    rewrite is_image_is_image_spec in * by apply H.
    assert (HH1:=H1).
    unfold ReflectL in H1.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
    ex_and H1 X.
    induction H4.
      double X M Y.
      assert (Midpoint Y Q Q').
        eapply symmetry_preserves_midpoint.
          apply H2.
          apply H6.
          apply H3.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
        apply H1.
      assert (P <> P').
        intro.
        subst P'.
        apply perp_distinct in H4.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        absurde.
      assert (Q <> Q').
        intro.
        subst Q'.
        apply l7_3 in H7.
        subst Q.
        assert (P=P').
          eapply l7_9.
            apply H2.
          apply H3.
        subst P'.
        apply perp_distinct in H4.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        absurde.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: @Per Tn A B X *)
        exists Y.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
        split.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
          apply l7_2.
          apply H7.
(* Goal: or (@Perp Tn A B X Y) (@eq (@Tpoint Tn) X Y) *)
        induction (eq_dec_points X Y).
          subst Y.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Per Tn P C A) (and (@Cong Tn P C X Y) (@OS Tn A B P D))) *)
        assert_diffs.
        ColR.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      left.
      assert(Per M Y Q).
        unfold Per.
        exists Q'.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
        split.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        unfold Midpoint in *.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        eapply cong_transitivity.
          apply cong_symmetry.
          apply H14.
        apply cong_symmetry.
        eapply cong_transitivity.
          apply cong_symmetry.
          apply H13.
        eapply is_image_col_cong.
          apply H.
(* Goal: @Reflect Tn P' P A B *)
          apply l10_4.
          apply is_image_is_image_spec.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
          apply HH1.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: or (@Perp Tn A B X Y) (@eq (@Tpoint Tn) X Y) *)
      induction (eq_dec_points X Y).
        subst Y.
        apply l7_3 in H6.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
(* Goal: @Perp Tn A B X Y *)
        apply perp_sym.
        eapply perp_col.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
          auto.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
          apply perp_left_comm.
          eapply perp_col.
(* Goal: @Perp Tn A B X Y *)
            2:apply perp_sym.
            2:apply H4.
            intro.
            subst Q'.
            apply l7_3 in H3.
            subst P'.
            apply is_midpoint_id in H1.
            subst P.
            absurde.
          eapply (col_transitivity_2 M).
            intro.
            subst P'.
            apply is_midpoint_id in H1.
            subst P.
            absurde.
            unfold Col.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
            right; right.
            apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
            apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
          unfold Col.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
          right; right.
          apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
          apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        eapply (col_transitivity_2 M).
          intro.
          subst Q'.
          apply l7_2 in H7.
          apply is_midpoint_id in H7.
          subst Q.
          absurde.
          unfold Col.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
          right; right.
          apply midpoint_bet.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        unfold Col.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        right; right.
        apply midpoint_bet.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      apply per_perp_in in H10.
        apply perp_in_perp_bis in H10.
        induction H10.
          apply perp_distinct in H10.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
          spliter.
          absurde.
        apply perp_comm.
(* Goal: @Perp Tn A B X Y *)
        apply perp_sym.
        eapply perp_col.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
          apply perp_comm.
          eapply (perp_col  Y Q).
            intro.
            subst Q.
            apply perp_distinct in H10.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
            spliter.
            absurde.
(* Goal: @Perp Tn A B X Y *)
            apply perp_sym.
            induction (eq_dec_points A M).
              subst A.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
              apply perp_left_comm.
              eapply (perp_col _ M).
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
                auto.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
                apply perp_left_comm.
                eapply (perp_col _ Y).
(* Goal: @Midpoint Tn A P' P *)
                  assumption.
(* Goal: @Midpoint Tn A P' P *)
                  assumption.
                induction (eq_dec_points M X).
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
                  subst X.
                  apply is_midpoint_id in H6.
                  subst M.
                  apply col_trivial_1.
                eapply (col_transitivity_1 _ X).
(* Goal: @Midpoint Tn A P' P *)
                  assumption.
                  unfold Col.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
                  right; right.
                  apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
                  apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
                  assumption.
                apply col_permutation_5.
(* Goal: @Midpoint Tn A P' P *)
                assumption.
              apply col_trivial_2.
            induction (eq_dec_points B M).
              subst M.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
              apply perp_left_comm.
              apply (perp_col _ Y).
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
                auto.
(* Goal: @Midpoint Tn A P' P *)
                assumption.
              induction (eq_dec_points B X).
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
                subst X.
                apply is_midpoint_id in H6.
                subst Y.
                absurde.
              eapply col_transitivity_1.
                apply H13.
                unfold Col.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
                right; right.
                apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
                apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
                assumption.
              apply col_permutation_1.
(* Goal: @Midpoint Tn A P' P *)
              assumption.
            eapply perp_col.
(* Goal: @Midpoint Tn A P' P *)
              assumption.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
              apply perp_left_comm.
              eapply (perp_col M Y).
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
                auto.
(* Goal: @Midpoint Tn A P' P *)
                assumption.
              assert(Col B X M).
                eapply col_transitivity_2.
                  apply H.
(* Goal: @Midpoint Tn A P' P *)
                  assumption.
(* Goal: @Midpoint Tn A P' P *)
                assumption.
              induction (eq_dec_points M X).
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
                subst X.
                apply is_midpoint_id in H6.
(* Goal: @Midpoint Tn A P' P *)
(* Goal: @Midpoint Tn A P' P *)
                contradiction.
              assert(Col B Y M).
                apply col_permutation_1.
                eapply (col_transitivity_2  X).
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
                  auto.
                  apply col_permutation_1.
(* Goal: @Midpoint Tn A P' P *)
                  assumption.
                unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
                left.
                apply midpoint_bet.
(* Goal: @Midpoint Tn A P' P *)
                assumption.
              eapply (col_transitivity_1 _ B).
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
                auto.
                apply col_permutation_2.
(* Goal: @Midpoint Tn A P' P *)
                assumption.
              apply col_permutation_3.
              apply H0.
            apply col_permutation_5.
            apply H0.
          apply col_trivial_2.
        unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        left.
        apply midpoint_bet.
        apply H7.
        intro.
        subst Y.
        apply l7_2 in H6.
        apply is_midpoint_id in H6.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
        absurde.
      intro.
      subst Q.
      apply is_midpoint_id in H7.
      subst Q'.
      absurde.
    subst P'.
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
    apply l7_3 in H1.
    subst P.
    assert(Q = Q').
      eapply l7_9.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
        apply H2.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
      apply l7_2.
      apply H3.
    subst Q'.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
      exists Q.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: @Midpoint Tn X X X *)
(* Goal: @Col Tn A B X *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
        apply l7_3_2.
      induction (eq_dec_points M X).
(* Goal: @Col Tn P A B *)
(* Goal: @Col Tn P A B *)
        subst X.
        assert(M=Q).
          apply is_midpoint_id.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        subst Q.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      ColR.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    right.
(* Goal: @eq (@Tpoint Tn) X X *)
    reflexivity.
Qed.

Lemma image_in_is_image_spec :
 forall M A B P P',
  ReflectL_at M P P' A B -> ReflectL P P' A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @ReflectL Tn P P' A B *)
    unfold ReflectL_at in H.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter.
(* Goal: @ReflectL Tn X X A B *)
    unfold ReflectL.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X P' P) (@Col Tn A B X)) *)
(* Goal: or (@Perp Tn A B P' P) (@eq (@Tpoint Tn) P' P) *)
      exists M.
(* Goal: @Midpoint Tn A P' P *)
      split; assumption.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma image_in_gen_is_image : forall M A B P P',
 Reflect_at M P P' A B  -> Reflect P P' A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @Reflect Tn P P' A B *)
    unfold Reflect_at in H.
(* Goal: or (and (not (@eq (@Tpoint Tn) B A)) (@ReflectL Tn P P' B A)) (and (@eq (@Tpoint Tn) B A) (@Midpoint Tn B P' P)) *)
    induction H.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
(* Goal: @Reflect Tn P P' A B *)
(* Goal: @Reflect Tn P P' A B *)
      apply image_in_is_image_spec in H0.
(* Goal: @Reflect Tn A B' C D *)
      unfold Reflect.
(* Goal: or (and (not (@eq (@Tpoint Tn) C D)) (@ReflectL Tn A B' C D)) (and (@eq (@Tpoint Tn) C D) (@Midpoint Tn C B' A)) *)
      tauto.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    subst.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    subst.
(* Goal: @Reflect Tn A B' C D *)
    unfold Reflect.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    right.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
    auto.
Qed.

Lemma image_image_in : forall A B P P' M,
 P <> P'-> ReflectL P P' A B -> Col A B M -> Col P M P' ->
 ReflectL_at M P P' A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
    unfold ReflectL_at.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
        assert(HH:=H0).
        unfold ReflectL in H0.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
        ex_and H0 M'.
        induction H3.
          assert (Perp P M' A B).
            eapply perp_col.
              intro.
              subst P.
              apply l7_2 in H0.
              apply is_midpoint_id in H0.
              subst P'.
              apply perp_distinct in H3.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
              spliter.
              absurde.
(* Goal: @Perp Tn A B X Y *)
              apply perp_sym.
(* Goal: @Perp Tn A B P P' *)
(* Goal: or (@Perp Tn A B P P') (@eq (@Tpoint Tn) P P') *)
              apply perp_right_comm.
              apply H3.
            unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
            right; left.
            apply midpoint_bet.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
          assert (M'=M).
            eapply l6_21.
              2: apply H.
              2: apply H4.
              induction (eq_dec_points A M').
                subst M'.
                assert (~ Col A B P /\ Per P A B).
                  eapply l8_16_1.
                    apply col_trivial_3.
                    apply col_trivial_2.
                    apply perp_distinct in H3.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
                    spliter.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
                    auto.
(* Goal: @Perp Tn A B X Y *)
                  apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
                  assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
                spliter.
                intro.
                apply H6.
(* Goal: @Midpoint Tn A P' P *)
                assumption.
              assert (~ Col A B P /\ Per P M' A).
                eapply l8_16_1.
(* Goal: @Midpoint Tn A P' P *)
                  assumption.
                  apply col_trivial_3.
(* Goal: @Perp Tn A B X Y *)
                apply perp_sym.
(* Goal: @Midpoint Tn A P' P *)
                assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
              spliter.
              intro.
              apply H7.
(* Goal: @Midpoint Tn A P' P *)
              assumption.
(* Goal: @Midpoint Tn A P' P *)
              assumption.
              unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
              right; left.
              apply midpoint_bet.
              apply H0.
              apply col_permutation_5.
(* Goal: @Midpoint Tn A P' P *)
              assumption.
            apply perp_distinct in H3.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
            spliter.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
            auto.
          subst M'.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        subst P'.
        absurde.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    assert (HH:=H0).
    unfold ReflectL in H0.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter.
    induction H3.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      left.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    right.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma image_in_col0 : forall A B P P' Y : Tpoint,
 ReflectL_at Y P P' A B -> Col P P' Y.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @Col Tn P P' Y *)
    unfold ReflectL_at in *.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter.
(* Goal: @Col Tn P P' Y *)
    assert_cols.
(* Goal: @Col Tn B B A *)
    Col.
Qed.

Lemma is_image_spec_rev : forall P P' A B, ReflectL P P' A B -> ReflectL P P' B A.
Proof.
(* Goal: @ReflectL Tn X X A B *)
    unfold ReflectL.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X P' P) (@Col Tn B A X)) *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
      ex_and H M0.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X P' P) (@Col Tn B A X)) *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
      exists M0.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @Col Tn B A M0 *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
      apply col_permutation_4.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
    induction H0.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      left.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
      apply perp_left_comm.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    right.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma is_image_rev : forall P P' A B,
 Reflect P P' A B -> Reflect P P' B A.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @Reflect Tn P P' B A *)
    unfold Reflect in *.
(* Goal: or (and (not (@eq (@Tpoint Tn) B A)) (@ReflectL Tn P P' B A)) (and (@eq (@Tpoint Tn) B A) (@Midpoint Tn B P' P)) *)
    induction H.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      left.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
        auto.
(* Goal: @ReflectL Tn P P' B A *)
(* Goal: or (and (not (@eq (@Tpoint Tn) B A)) (@ReflectL Tn P P' B A)) (and (@eq (@Tpoint Tn) B A) (@Midpoint Tn B P' P)) *)
      apply is_image_spec_rev.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    right.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter. subst. tauto.
Qed.

Lemma midpoint_preserves_per : forall A B C A1 B1 C1 M,
 Per A B C ->
 Midpoint M A A1 ->
 Midpoint M B B1 ->
 Midpoint M C C1 ->
 Per A1 B1 C1.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
    unfold Per in *.
    ex_and H C'.
    double C' M C1'.
    exists C1'.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
      eapply symmetry_preserves_midpoint.
        apply H2.
        apply H1.
        apply H4.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    eapply l7_16.
      apply H0.
      apply H2.
      apply H0.
      apply H4.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma col__image_spec : forall A B X, Col A B X -> ReflectL X X A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @ReflectL Tn X X A B *)
    unfold ReflectL.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 X X) (@Col Tn A B X0)) *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
      exists X.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: @Midpoint Tn X X X *)
(* Goal: @Col Tn A B X *)
(* Goal: or (@Perp Tn A B X X) (@eq (@Tpoint Tn) X X) *)
        apply l7_3_2.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    right.
(* Goal: @eq (@Tpoint Tn) X X *)
    reflexivity.
Qed.

Lemma image_triv : forall A B, Reflect A A A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @Reflect Tn Y X A B *)
    induction (eq_dec_points A B).
(* Goal: @Reflect Tn A A A B *)
(* Goal: @Reflect Tn A A A B *)
      right; split; Midpoint.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    left; split.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
      auto.
(* Goal: @Col Tn B B A *)
    apply col__image_spec; Col.
Qed.

Lemma cong_midpoint__image : forall A B X Y, Cong A X A Y -> Midpoint B X Y -> Reflect Y X A B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @Reflect Tn Y X A B *)
    induction (eq_dec_points A B).
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
      right; subst; split; auto.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
    left; repeat split; auto.
(* Goal: @Col Tn B B A *)
      exists B; split; Col.
(* Goal: or (@Perp Tn A B X Y) (@eq (@Tpoint Tn) X Y) *)
    induction(eq_dec_points X Y).
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      right.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    left.
(* Goal: @Perp Tn A B X Y *)
    apply perp_sym.
(* Goal: @Perp Tn X Y A B *)
    assert(B <> X /\ B <> Y).
(* Goal: and (not (@eq (@Tpoint Tn) B X)) (not (@eq (@Tpoint Tn) B Y)) *)
(* Goal: @Perp Tn X Y A B *)
      apply midpoint_distinct_1.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter.
(* Goal: @Col Tn B B A *)
      apply col_per_perp; Col.
(* Goal: @Per Tn A B X *)
    exists Y.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma col_image_spec__eq : forall A B P P', Col A B P -> ReflectL P P' A B -> P = P'.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @eq (@Tpoint Tn) P P' *)
    apply (l10_6_uniqueness_spec A B P).
(* Goal: @Midpoint Tn A P' P *)
      apply col__image_spec; assumption.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
Qed.

Lemma image_spec_triv : forall A B, ReflectL A A B B.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: @ReflectL Tn A A B B *)
    apply col__image_spec.
(* Goal: @Col Tn B B A *)
    Col.
Qed.

Lemma image_spec__eq : forall A P P', ReflectL P P' A A -> P = P'.
Proof.
(* Goal: @Col Tn B B A *)
    intros A P P'; apply col_image_spec__eq; Col.
Qed.

Lemma image__midpoint : forall A P P', Reflect P P' A A -> Midpoint A P' P.
Proof.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    induction 1; spliter.
(* Goal: @Midpoint Tn A P' P *)
(* Goal: @Midpoint Tn A P' P *)
      contradiction.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
Qed.

Lemma is_image_spec_dec :
  forall A B C D, ReflectL A B C D \/ ~ ReflectL A B C D.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    elim (eq_dec_points C D); intro HCD.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      subst.
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      elim (eq_dec_points A B); intro HAB.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        subst.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        left.
(* Goal: @ReflectL Tn B B D D *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        apply image_spec_triv.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      right.
(* Goal: not (@ReflectL Tn A B C D) *)
      intro H.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      unfold ReflectL in *.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      destruct H as [H HFalse].
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      elim HFalse; clear HFalse; intro HFalse.
(* Goal: False *)
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        apply perp_distinct in HFalse.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
        intuition.
(* Goal: False *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
      intuition.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    elim (l10_6_existence_spec C D A HCD); intros B' HB'.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    elim (eq_dec_points B B'); intro HBB'.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      subst.
(* Goal: or (and (not (@eq (@Tpoint Tn) C D)) (@ReflectL Tn A B' C D)) (and (@eq (@Tpoint Tn) C D) (@Midpoint Tn C B' A)) *)
      tauto.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
    right.
(* Goal: not (@ReflectL Tn A B C D) *)
    intro H.
(* Goal: False *)
    apply HBB'.
(* Goal: @eq (@Tpoint Tn) B B' *)
    apply l10_6_uniqueness with C D A.
(* Goal: @Reflect Tn A B' C D *)
      unfold Reflect.
(* Goal: or (and (not (@eq (@Tpoint Tn) C D)) (@ReflectL Tn A B' C D)) (and (@eq (@Tpoint Tn) C D) (@Midpoint Tn C B' A)) *)
      tauto.
(* Goal: @Reflect Tn A B' C D *)
    unfold Reflect.
(* Goal: or (and (not (@eq (@Tpoint Tn) C D)) (@ReflectL Tn A B' C D)) (and (@eq (@Tpoint Tn) C D) (@Midpoint Tn C B' A)) *)
    tauto.
Qed.

Lemma l10_14 : forall P P' A B, P <> P' -> A <> B ->
 Reflect P P' A B -> TS A B P P'.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
    rewrite is_image_is_image_spec in H1 by apply H0.
    unfold ReflectL in H1.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    spliter.
    ex_and H1 M0.
    induction H2.
      assert (P <> M0).
        intro.
        subst P.
        apply l7_2 in H1.
        apply is_midpoint_id in H1.
        subst P'.
        absurde.
      induction (eq_dec_points A M0).
        subst A.
        assert (Perp M0 B P M0).
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
          eapply (perp_col _ P').
(* Goal: @Midpoint Tn A P' P *)
            assumption.
(* Goal: @Perp Tn A B X Y *)
            apply perp_sym.
(* Goal: @Perp Tn A B P P' *)
(* Goal: or (@Perp Tn A B P P') (@eq (@Tpoint Tn) P P') *)
            apply perp_right_comm.
            apply H2.
          unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
          right; left.
          apply midpoint_bet.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        assert (Perp_at M0 M0 B P M0).
          eapply perp_perp_in.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        assert(Per B M0 P).
          eapply perp_in_per.
          apply perp_in_comm.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        assert (B <> M0).
          intro.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
          repeat split.
(* Goal: @Reflect Tn P' P A B *)
(* Goal: @Reflect Tn P' P A B *)
          subst B.
          apply perp_distinct in H2.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
          spliter.
          absurde.
        assert (~Col B M0 P).
          eapply per_not_col.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
            auto.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
        repeat split.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
          auto.
          intro.
          apply H9.
(* Goal: @Col Tn B B A *)
          Col.
          intro.
          apply H9.
          apply col_permutation_2.
          eapply (col_transitivity_1 _ P').
            intro.
            subst P'.
            apply is_midpoint_id in H1.
            subst P.
            absurde.
            unfold Col.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
            right; right.
            apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
            apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
(* Goal: @Col Tn B A M0 *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
          apply col_permutation_4.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X P' P) (@Col Tn B A X)) *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
        exists M0.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
        split.
          apply col_trivial_1.
        apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      induction (eq_dec_points B M0).
(* Goal: @Reflect Tn P' P A B *)
(* Goal: @Reflect Tn P' P A B *)
        subst B.
        assert (Perp M0 A P M0).
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
          eapply (perp_col _ P').
(* Goal: @Midpoint Tn A P' P *)
            assumption.
(* Goal: @Perp Tn A B X Y *)
            apply perp_sym.
            apply perp_comm.
            apply H2.
          unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
          right; left.
          apply midpoint_bet.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        assert (Perp_at M0 M0 A P M0).
          eapply perp_perp_in.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        assert(Per A M0 P).
          eapply perp_in_per.
          apply perp_in_comm.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
        repeat split.
          assert (~Col A M0 P).
            eapply per_not_col.
(* Goal: @Midpoint Tn A P' P *)
              assumption.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
              auto.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
          intro.
          apply H9.
          apply col_permutation_1.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
          intro.
          assert (Col M0 A P).
            eapply (col_transitivity_1 _ P').
              intro.
              subst P'.
              apply is_midpoint_id in H1.
              subst P.
              absurde.
              apply col_permutation_2.
(* Goal: @Midpoint Tn A P' P *)
              assumption.
            unfold Col.
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
            right; right.
            apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
            apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
          eapply (per_not_col ).
            3: apply H8.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
            auto.
(* Goal: @Col Tn B A M0 *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
          apply col_permutation_4.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X P' P) (@Col Tn B A X)) *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
        exists M0.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
        split.
          apply col_trivial_3.
        apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
        apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      repeat split.
        assert(Perp  P M0 A B).
          eapply perp_col.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
(* Goal: @Perp Tn A B X Y *)
            apply perp_sym.
(* Goal: @Perp Tn A B P P' *)
(* Goal: or (@Perp Tn A B P P') (@eq (@Tpoint Tn) P P') *)
            apply perp_right_comm.
            apply H2.
          unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
          right; left.
          apply midpoint_bet.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        assert (~ Col M0 P A).
          apply perp_not_col.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
          eapply perp_col.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
(* Goal: @Perp Tn A B X Y *)
            apply perp_sym.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
            apply perp_left_comm.
            apply H7.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        intro.
        apply H8.
        apply col_permutation_1.
        eapply col_transitivity_1.
          apply perp_distinct in H2.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
          spliter.
          apply H2.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        apply col_permutation_1.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
        assert(Perp  P' M0 A B).
          eapply perp_col.
            intro.
            subst P'.
            apply is_midpoint_id in H1.
            subst P.
            absurde.
(* Goal: @Perp Tn A B X Y *)
            apply perp_sym.
            apply H2.
          unfold Col.
(* Goal: or (@ReflectL Tn B B D D) (not (@ReflectL Tn B B D D)) *)
(* Goal: or (@ReflectL Tn A B D D) (not (@ReflectL Tn A B D D)) *)
(* Goal: or (@ReflectL Tn A B C D) (not (@ReflectL Tn A B C D)) *)
          right; left.
          apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
          apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        assert (~ Col M0 P' A).
          apply perp_not_col.
(* Goal: @Perp Tn A B X Y *)
          apply perp_sym.
          eapply perp_col.
(* Goal: @Midpoint Tn A P' P *)
            assumption.
(* Goal: @Perp Tn A B X Y *)
            apply perp_sym.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
            apply perp_left_comm.
            apply H7.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        intro.
        apply H8.
        apply col_permutation_1.
        eapply col_transitivity_1.
          apply perp_distinct in H2.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
          spliter.
          apply H2.
(* Goal: @Midpoint Tn A P' P *)
          assumption.
        apply col_permutation_1.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Midpoint Tn X P' P) (@Col Tn B A X)) *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
      exists M0.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
        apply col_permutation_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      apply midpoint_bet.
(* Goal: @Midpoint Tn A P P' *)
(* Goal: @Reflect Tn P' P A B *)
      apply l7_2.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    subst P'.
    absurde.
Qed.

Lemma l10_15 : forall A B C P,
 Col A B C -> ~ Col A B P ->
 exists Q, Perp A B Q C /\ OS A B P Q.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
    intros.
    assert (A<>B).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      intro;subst.
(* Goal: @Col Tn B B A *)
      Col.
    assert (exists X , TS A B P X).
      apply l9_10.
      intro.
      apply H0.
      apply col_permutation_1.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    ex_elim H2 X.
    induction (eq_dec_points A C).
      subst C.
      assert (exists Q, exists T, Perp A B Q A /\ Col A B T /\ Bet X T Q).
        apply l8_21.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      ex_elim H2 Q.
      ex_and H4 T.
      exists Q.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      eapply l9_8_1.
        apply H3.
      unfold TS.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      repeat split.
        apply perp_not_col in H2.
        intro.
        apply H2.
        apply col_permutation_1.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
        unfold TS in H3.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
        spliter.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      exists T.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
      split.
        apply col_permutation_2.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
      apply between_symmetry.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    assert (exists Q, exists T, Perp C A Q C /\ Col C A T /\ Bet X T Q).
      apply l8_21.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
      auto.
    ex_elim H4 Q.
    ex_and H5 T.
    exists Q.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
      eapply perp_col.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @Perp Tn B A P' P *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
        apply perp_left_comm.
        apply H4.
      apply col_permutation_5.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    eapply l9_8_1.
      apply H3.
    unfold TS.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    repeat split.
      eapply perp_not_col in H4.
      intro.
      apply H4.
      apply col_permutation_2.
      eapply col_transitivity_1.
        apply H1.
        apply col_permutation_1.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
      unfold TS in H3.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
      spliter.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    exists T.
(* Goal: and (@Midpoint Tn B X Y) (@Cong Tn A X A Y) *)
    split.
      apply col_permutation_2.
      eapply col_transitivity_1.
        apply H2.
        apply col_permutation_5.
(* Goal: @Midpoint Tn A P' P *)
        assumption.
(* Goal: @Col Tn B A M0 *)
(* Goal: or (@Perp Tn B A P' P) (@eq (@Tpoint Tn) P' P) *)
      apply col_permutation_4.
(* Goal: @Midpoint Tn A P' P *)
      assumption.
    apply between_symmetry.
(* Goal: @Midpoint Tn A P' P *)
    assumption.
Qed.

Lemma ex_per_cong : forall A B C D X Y,
 A <> B -> X <> Y -> Col A B C -> ~Col A B D ->
 exists P, Per P C A /\ Cong P C X Y /\ OS A B P D.
Proof.
(* Goal: @Col Tn B B A *)
    intros A B C D X Y HAB HXY HCol HNCol.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Per Tn P C A) (and (@Cong Tn P C X Y) (@OS Tn A B P D))) *)
    destruct (l10_15 A B C D) as [Q [HQ1 HQ2]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Per Tn P C A) (and (@Cong Tn P C X Y) (@OS Tn A B P D))) *)
    assert_diffs.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
    destruct (segment_construction_3 C Q X Y) as [P [HP1 HP2]]; auto.
    exists P; repeat split; Cong.
    - destruct (eq_dec_points A C).
(* Goal: @Per Tn P C A *)
(* Goal: @Per Tn P C A *)
        subst; Perp.
(* Goal: @Per Tn P C A *)
      apply perp_per_1.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: @ReflectL Tn A A A B *)
      apply perp_col1 with B; auto.
(* Goal: @Perp Tn C P A B *)
      assert_diffs; apply perp_sym, perp_col1 with Q; Col; Perp.
    - apply os_out_os with Q C; Side.
Qed.

Lemma exists_cong_per : forall A B X Y, exists C, Per A B C /\ Cong B C X Y.
Proof.
(* Goal: forall A B X Y : @Tpoint Tn, @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
destruct (eq_dec_points A B).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
subst.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn B B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
destruct (segment_construction X B X Y).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn B B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
exists x;split;spliter;finish.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
destruct (not_col_exists A B H) as [P HP].
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
destruct (eq_dec_points X Y).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
exists B;split;subst;finish.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
destruct (ex_per_cong A B B P X Y);finish.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
spliter.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => and (@Per Tn A B C) (@Cong Tn B C X Y)) *)
exists x;split;finish.
Qed.

End T10.
