Require Export GeoCoq.Tarski_dev.Ch07_midpoint.
(*
We choose to use ColR as it is faster than CoincR.
*)
(*
Require Export GeoCoq.Tactics.Coinc.CoincR_for_col.
*)
Require Export GeoCoq.Tactics.Coinc.ColR.

Ltac not_exist_hyp_perm_ncol A B C := not_exist_hyp (~ Col A B C); not_exist_hyp (~ Col A C B);
                                 not_exist_hyp (~ Col B A C); not_exist_hyp (~ Col B C A);
                                 not_exist_hyp (~ Col C A B); not_exist_hyp (~ Col C B A).

Ltac assert_diffs_by_cases :=
 repeat match goal with
 | A: Tpoint, B: Tpoint |- _ => not_exist_hyp_comm A B;induction (eq_dec_points A B);[treat_equalities;solve [finish|trivial] |idtac]
end.

Ltac assert_cols :=
repeat
 match goal with
      | H:Bet ?X1 ?X2 ?X3 |- _ =>
     not_exist_hyp_perm_col X1 X2 X3;assert (Col X1 X2 X3) by (apply bet_col;apply H)

      | H:Midpoint ?X1 ?X2 ?X3 |- _ =>
     not_exist_hyp_perm_col X1 X2 X3;let N := fresh in assert (N := midpoint_col X2 X1 X3 H)

      | H:Out ?X1 ?X2 ?X3 |- _ =>
     not_exist_hyp_perm_col X1 X2 X3;let N := fresh in assert (N := out_col X1 X2 X3 H)
 end.

Ltac assert_bets :=
repeat
 match goal with
      | H:Midpoint ?B ?A ?C |- _ => let T := fresh in not_exist_hyp (Bet A B C); assert (T := midpoint_bet A B C H)
 end.

Ltac clean_reap_hyps :=
  clean_duplicated_hyps;
  repeat
  match goal with
   | H:(Midpoint ?A ?B ?C), H2 : Midpoint ?A ?C ?B |- _ => clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?A ?C ?B |- _ => clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?B ?A ?C |- _ => clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?B ?C ?A |- _ => clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?C ?B ?A |- _ => clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?C ?A ?B |- _ => clear H2
   | H:(Bet ?A ?B ?C), H2 : Bet ?C ?B ?A |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?D ?C |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?A ?B |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?B ?A |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?B ?A |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?A ?B |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?C ?D |- _ => clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?D ?C |- _ => clear H2
   | H:(?A<>?B), H2 : (?B<>?A) |- _ => clear H2
end.

Ltac assert_diffs :=
repeat
 match goal with
      | H:(~Col ?X1 ?X2 ?X3) |- _ =>
      let h := fresh in
      not_exist_hyp3 X1 X2 X1 X3 X2 X3;
      assert (h := not_col_distincts X1 X2 X3 H);decompose [and] h;clear h;clean_reap_hyps

      | H:(~Bet ?X1 ?X2 ?X3) |- _ =>
      let h := fresh in
      not_exist_hyp2 X1 X2 X2 X3;
      assert (h := not_bet_distincts X1 X2 X3 H);decompose [and] h;clear h;clean_reap_hyps
      | H:Bet ?A ?B ?C, H2 : ?A <> ?B |-_ =>
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= bet_neq12__neq A B C H H2);clean_reap_hyps
      | H:Bet ?A ?B ?C, H2 : ?B <> ?A |-_ =>
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= bet_neq21__neq A B C H H2);clean_reap_hyps
      | H:Bet ?A ?B ?C, H2 : ?B <> ?C |-_ =>
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= bet_neq23__neq A B C H H2);clean_reap_hyps
      | H:Bet ?A ?B ?C, H2 : ?C <> ?B |-_ =>
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= bet_neq32__neq A B C H H2);clean_reap_hyps

      | H:Cong ?A ?B ?C ?D, H2 : ?A <> ?B |-_ =>
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= cong_diff A B C D H2 H);clean_reap_hyps
      | H:Cong ?A ?B ?C ?D, H2 : ?B <> ?A |-_ =>
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= cong_diff_2 A B C D H2 H);clean_reap_hyps
      | H:Cong ?A ?B ?C ?D, H2 : ?C <> ?D |-_ =>
      let T:= fresh in (not_exist_hyp_comm A B);
        assert (T:= cong_diff_3 A B C D H2 H);clean_reap_hyps
      | H:Cong ?A ?B ?C ?D, H2 : ?D <> ?C |-_ =>
      let T:= fresh in (not_exist_hyp_comm A B);
        assert (T:= cong_diff_4 A B C D H2 H);clean_reap_hyps

      | H:Le ?A ?B ?C ?D, H2 : ?A <> ?B |-_ =>
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= le_diff A B C D H2 H);clean_reap_hyps
      | H:Lt ?A ?B ?C ?D |-_ =>
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= lt_diff A B C D H);clean_reap_hyps

      | H:Midpoint ?I ?A ?B, H2 : ?A<>?B |- _ =>
      let T:= fresh in (not_exist_hyp2 I B I A);
       assert (T:= midpoint_distinct_1 I A B H2 H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Midpoint ?I ?A ?B, H2 : ?B<>?A |- _ =>
      let T:= fresh in (not_exist_hyp2 I B I A);
       assert (T:= midpoint_distinct_1 I A B (swap_diff B A H2) H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:Midpoint ?I ?A ?B, H2 : ?I<>?A |- _ =>
      let T:= fresh in (not_exist_hyp2 I B A B);
       assert (T:= midpoint_distinct_2 I A B H2 H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Midpoint ?I ?A ?B, H2 : ?A<>?I |- _ =>
      let T:= fresh in (not_exist_hyp2 I B A B);
       assert (T:= midpoint_distinct_2 I A B (swap_diff A I H2) H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:Midpoint ?I ?A ?B, H2 : ?I<>?B |- _ =>
      let T:= fresh in (not_exist_hyp2 I A A B);
       assert (T:= midpoint_distinct_3 I A B H2 H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Midpoint ?I ?A ?B, H2 : ?B<>?I |- _ =>
      let T:= fresh in (not_exist_hyp2 I A A B);
       assert (T:= midpoint_distinct_3 I A B (swap_diff B I H2) H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:Out ?A ?B ?C |- _ =>
      let T:= fresh in (not_exist_hyp2 A B A C);
       assert (T:= out_distinct A B C H);
       decompose [and] T;clear T;clean_reap_hyps
 end.

Ltac clean_trivial_hyps :=
  repeat
  match goal with
   | H:(Cong ?X1 ?X1 ?X2 ?X2) |- _ => clear H
   | H:(Cong ?X1 ?X2 ?X2 ?X1) |- _ => clear H
   | H:(Cong ?X1 ?X2 ?X1 ?X2) |- _ => clear H
   | H:(Bet ?X1 ?X1 ?X2) |- _ => clear H
   | H:(Bet ?X2 ?X1 ?X1) |- _ => clear H
   | H:(Col ?X1 ?X1 ?X2) |- _ => clear H
   | H:(Col ?X2 ?X1 ?X1) |- _ => clear H
   | H:(Col ?X1 ?X2 ?X1) |- _ => clear H
   | H:(Midpoint ?X1 ?X1 ?X1) |- _ => clear H
end.

Ltac clean := clean_trivial_hyps;clean_reap_hyps.

Ltac treat_equalities :=
try treat_equalities_aux;
repeat
  match goal with
   | H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ =>
      apply cong_symmetry in H; apply cong_identity in H;
      smart_subst X2;clean_reap_hyps
   | H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ =>
      apply cong_identity in H;smart_subst X2;clean_reap_hyps
   | H:(Bet ?X1 ?X2 ?X1) |- _ =>
      apply  between_identity in H;smart_subst X2;clean_reap_hyps
   | H:(Midpoint ?X ?Y ?Y) |- _ => apply l7_3 in H; smart_subst Y;clean_reap_hyps
   | H : Bet ?A ?B ?C, H2 : Bet ?B ?A ?C |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T : A=B) by (apply (between_equality A B C); finish);
                       smart_subst A;clean_reap_hyps
   | H : Bet ?A ?B ?C, H2 : Bet ?A ?C ?B |- _ =>
     let T := fresh in not_exist_hyp (B=C); assert (T : B=C) by (apply (between_equality_2 A B C); finish);
                       smart_subst B;clean_reap_hyps
   | H : Bet ?A ?B ?C, H2 : Bet ?C ?A ?B |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T : A=B) by (apply (between_equality A B C); finish);
                       smart_subst A;clean_reap_hyps
   | H : Bet ?A ?B ?C, H2 : Bet ?B ?C ?A |- _ =>
     let T := fresh in not_exist_hyp (B=C); assert (T : B=C) by (apply (between_equality_2 A B C); finish);
                       smart_subst A;clean_reap_hyps
   | H:(Le ?X1 ?X2 ?X3 ?X3) |- _ =>
      apply le_zero in H;smart_subst X2;clean_reap_hyps
   | H : Midpoint ?P ?A ?P1, H2 : Midpoint ?P ?A ?P2 |- _ =>
     let T := fresh in not_exist_hyp (P1=P2);
                      assert (T := symmetric_point_uniqueness A P P1 P2 H H2);
                      smart_subst P1;clean_reap_hyps
   | H : Midpoint ?A ?P ?X, H2 : Midpoint ?A ?Q ?X |- _ =>
     let T := fresh in not_exist_hyp (P=Q); assert (T := l7_9 P Q A X H H2);
                       smart_subst P;clean_reap_hyps
   | H : Midpoint ?A ?P ?X, H2 : Midpoint ?A ?X ?Q |- _ =>
     let T := fresh in not_exist_hyp (P=Q); assert (T := l7_9_bis P Q A X H H2);
                       smart_subst P;clean_reap_hyps
   | H : Midpoint ?M ?A ?A |- _ =>
     let T := fresh in not_exist_hyp (M=A); assert (T : l7_3 M A H);
                       smart_subst M;clean_reap_hyps
   | H : Midpoint ?A ?P ?P', H2 : Midpoint ?B ?P ?P' |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T := l7_17 P P' A B H H2);
                       smart_subst A;clean_reap_hyps
   | H : Midpoint ?A ?P ?P', H2 : Midpoint ?B ?P' ?P |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T := l7_17_bis P P' A B H H2);
                       smart_subst A;clean_reap_hyps
   | H : Midpoint ?A ?B ?A |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id_2 A B H);
                       smart_subst A;clean_reap_hyps
   | H : Midpoint ?A ?A ?B |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id A B H);
                       smart_subst A;clean_reap_hyps
end.

Ltac ColR :=
 let tpoint := constr:(Tpoint) in
 let col := constr:(Col) in
   treat_equalities; assert_cols; assert_diffs; try (solve [Col]); Col_refl tpoint col.

Ltac search_contradiction :=
 match goal with
  | H: ?A <> ?A |- _ => exfalso;apply H;reflexivity
  | H: ~ Col ?A ?B ?C |- _ => exfalso;apply H;ColR
  | H: ~ ?P, H2 : ?P |- _ => exfalso;apply (H H2)
 end.

(* TODO replace show_distinct *)
Ltac show_distinct' X Y :=
 assert (X<>Y);
 [intro;treat_equalities; (solve [search_contradiction])|idtac].

Ltac assert_all_diffs_by_contradiction :=
repeat match goal with
 | A: Tpoint, B: Tpoint |- _ => not_exist_hyp_comm A B;show_distinct' A B
end.
(*
Ltac update_cols :=
 let tpoint := constr:(Tpoint) in
 let col := constr:(Col) in
   update_cols_gen tpoint col.

Ltac deduce_cols :=
 let tpoint := constr:(Tpoint) in
 let col := constr:(Col) in
   treat_equalities; deduce_cols_hide_gen tpoint col.

Ltac cols :=
 let tpoint := constr:(Tpoint) in
 let col := constr:(Col) in
   cols_gen tpoint col.

Ltac tag_hyps :=
 let tpoint := constr:(Tpoint) in
 let col := constr:(Col) in
   tag_hyps_gen tpoint col.

Ltac untag_hyps :=
 let tpoint := constr:(Tpoint) in
 let col := constr:(Col) in
   untag_hyps_gen tpoint col.

Ltac clear_cols :=
 let tpoint := constr:(Tpoint) in
 let col := constr:(Col) in
   clear_cols_gen tpoint col.

Ltac smart_subst' := update_cols;clean.

Ltac treat_equalities_aux' :=
  match goal with
   | H:(?X1 = ?X2) |- _ => smart_subst'
end.

Ltac treat_equalities' :=
try treat_equalities_aux';
repeat
  match goal with
   | H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ =>
      apply cong_symmetry in H; apply cong_identity in H; smart_subst'
   | H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ =>
      apply cong_identity in H; smart_subst'
   | H:(Bet ?X1 ?X2 ?X1) |- _ =>
      apply  between_identity in H; smart_subst'
   | H:(Midpoint ?X ?Y ?Y) |- _ => apply l7_3 in H; smart_subst'
   | H : Bet ?A ?B ?C, H2 : Bet ?B ?A ?C |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T : between_equality A B C H H2); smart_subst'
   | H : Midpoint ?P ?A ?P1, H2 : Midpoint ?P ?A ?P2 |- _ =>
     let T := fresh in not_exist_hyp (P1=P2); assert (T : symmetric_point_uniqueness A P P1 P2 H H2); smart_subst'
   | H : Midpoint ?A ?P ?X, H2 : Midpoint ?A ?Q ?X |- _ =>
     let T := fresh in not_exist_hyp (P=Q); assert (T : l7_9 P Q A X H H2); smart_subst'
   | H : Midpoint ?M ?A ?A |- _ =>
     let T := fresh in not_exist_hyp (M=A); assert (T : l7_3 M A H); smart_subst'
   | H : Midpoint ?A ?P ?P', H2 : Midpoint ?B ?P ?P' |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T := l7_17 P P' A B H H2); smart_subst'
   | H : Midpoint ?A ?B ?A |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id_2 A B H); smart_subst'
   | H : Midpoint ?A ?A ?B |- _ =>
     let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id A B H); smart_subst'
end.

Ltac search_contradiction' :=
 match goal with
  | H: ?A <> ?A |- _ => exfalso;apply H;reflexivity
  | H: ~ Col ?A ?B ?C |- _ => exfalso;apply H;cols
 end.

Ltac show_distinct'' X Y :=
 assert (X<>Y);
 [intro; treat_equalities'; (solve [search_contradiction'])|idtac].

Ltac show_not_col X Y Z :=
 assert (~ Col X Y Z);
 [intro; update_cols; (solve [search_contradiction'])|idtac].

Ltac assert_all_diffs_by_contradiction_aux :=
repeat match goal with
 | A: Tpoint, B: Tpoint |- _ => untag_hyps; not_exist_hyp_comm A B; tag_hyps; show_distinct'' A B
end.

Ltac assert_all_not_cols_by_contradiction_aux :=
repeat match goal with
 | A: Tpoint, B: Tpoint, C: Tpoint |- _ => untag_hyps; not_exist_hyp_perm_ncol A B C; tag_hyps; show_not_col A B C
end.

Ltac assert_all_diffs_by_contradiction' :=
  deduce_cols; assert_all_diffs_by_contradiction_aux; untag_hyps; clear_cols.

Ltac assert_all_not_cols_by_contradiction :=
  deduce_cols; assert_all_not_cols_by_contradiction_aux; untag_hyps; clear_cols.

Ltac assert_ndc_by_contradiction :=
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
  assert_all_diffs_by_contradiction'; assert_all_not_cols_by_contradiction.
*)
Section T8_1.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma per_dec : forall A B C, Per A B C \/ ~ Per A B C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @Per Tn A' B C) (_ : @Bet Tn A C A'), @eq (@Tpoint Tn) B C *)
    unfold Per.
(* Goal: or (@ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn B C C') (@Cong Tn A C A C'))) (not (@ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn B C C') (@Cong Tn A C A C')))) *)
    elim (symmetric_point_construction C B);intros C' HC'.
(* Goal: or (@ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn B C C') (@Cong Tn A C A C'))) (not (@ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn B C C') (@Cong Tn A C A C')))) *)
    elim (cong_dec A C A C');intro.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      left.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn B C C') (@Cong Tn A' C A' C')) *)
      exists C'.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
      intuition.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
    right.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
    intro.
(* Goal: False *)
    decompose [ex and] H0;clear H0.
(* Goal: False *)
    assert (C'=x) by (apply symmetric_point_uniqueness with C B;assumption).
(* Goal: False *)
    subst.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    intuition.
Qed.

Lemma l8_2 : forall A B C, Per A B C -> Per C B A.
Proof.
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @Per Tn A' B C) (_ : @Bet Tn A C A'), @eq (@Tpoint Tn) B C *)
    unfold Per.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @eq (@Tpoint Tn) B C *)
    ex_and H C'.
    assert (exists A', Midpoint B A A').
      apply symmetric_point_construction.
    ex_and H1 A'.
    exists A'.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    eapply cong_transitivity.
      apply cong_commutativity.
(* Goal: False *)
      apply H0.
    eapply l7_13.
(* Goal: False *)
      apply H.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
    apply l7_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

End T8_1.

Hint Resolve l8_2 : perp.

Ltac Perp := auto with perp.

Section T8_2.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma Per_cases :
 forall A B C,
 Per A B C \/ Per C B A ->
 Per A B C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp Tn A B B P *)
    decompose [or]  H;Perp.
Qed.

Lemma Per_perm :
 forall A B C,
 Per A B C ->
 Per A B C /\ Per C B A.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: and (@Per Tn A B C) (@Per Tn C B A) *)
    split; Perp.
Qed.

Lemma l8_3 : forall A B C A',
 Per A B C -> A<>B -> Col B A A' -> Per A' B C.
Proof.
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @Per Tn A' B C) (_ : @Bet Tn A C A'), @eq (@Tpoint Tn) B C *)
    unfold Per.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @eq (@Tpoint Tn) B C *)
    ex_and H C'.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn B C C') (@Cong Tn A' C A' C')) *)
    exists C'.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Cong Tn A' C A' C' *)
    unfold Midpoint in *;spliter.
(* Goal: @Cong Tn A' C A' C' *)
    eapply l4_17 with A B;finish.
Qed.

Lemma l8_4 : forall A B C C', Per A B C -> Midpoint B C C' -> Per A B C'.
Proof.
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @Per Tn A' B C) (_ : @Bet Tn A C A'), @eq (@Tpoint Tn) B C *)
    unfold Per.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C'0 : @Tpoint Tn => and (@Midpoint Tn B C' C'0) (@Cong Tn A C' A C'0)) *)
    ex_and H B'.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
    exists C.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    split.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
      apply l7_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Cong Tn A C' A C *)
    assert (B' = C') by (eapply symmetric_point_uniqueness;eauto).
(* Goal: @Cong Tn A C' A C *)
    subst B'.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
    Cong.
Qed.

Lemma l8_5 : forall A B, Per A B B.
Proof.
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @Per Tn A' B C) (_ : @Bet Tn A C A'), @eq (@Tpoint Tn) B C *)
    unfold Per.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn B B C') (@Cong Tn A B A C')) *)
    exists B.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    split.
(* Goal: @Midpoint Tn A A A *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
      apply l7_3_2.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
    Cong.
Qed.

Lemma l8_6 : forall A B C A', Per A B C -> Per A' B C -> Bet A C A' -> B=C.
Proof.
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @Per Tn A' B C) (_ : @Bet Tn A C A'), @eq (@Tpoint Tn) B C *)
    unfold Per.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @eq (@Tpoint Tn) B C *)
    ex_and H C'.
(* Goal: @eq (@Tpoint Tn) B C *)
    ex_and H0 C''.
(* Goal: @eq (@Tpoint Tn) B C *)
    assert (C'=C'') by (eapply symmetric_point_uniqueness;eauto).
(* Goal: @eq (@Tpoint Tn) B C *)
    subst C''.
(* Goal: @eq (@Tpoint Tn) B C *)
    assert (C = C') by (eapply l4_19;eauto).
(* Goal: False *)
    subst C'.
(* Goal: @eq (@Tpoint Tn) B C *)
    apply l7_3.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

End T8_2.

Hint Resolve l8_5 : perp.

Ltac let_symmetric C P A :=
let id1:=fresh in (assert (id1:(exists A', Midpoint P A A'));
[apply symmetric_point_construction|ex_and id1 C]).

Ltac symmetric B' A B :=
assert(sp:= symmetric_point_construction B A); ex_and sp B'.

Section T8_3.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma l8_7 : forall A B C, Per A B C -> Per A C B -> B=C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    unfold Per in H.
(* Goal: @eq (@Tpoint Tn) B C *)
    ex_and H C'.
    symmetric A' C A.
    induction (eq_dec_points B C).
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Per C' C A).
      eapply l8_3.
        eapply l8_2.
(* Goal: False *)
        apply H0.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      unfold Midpoint in H.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
      unfold Col.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      left.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Cong A C' A' C').
      unfold Per in H4.
      ex_and H4 Z.
      assert (A' = Z) by (eapply (symmetric_point_uniqueness A C A');auto).
      subst Z.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      Cong.
(* Goal: @Col Tn M A B *)
(* Goal: @Perp_at Tn M X M A B *)
    unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
    assert (Cong A' C A' C').
      eapply cong_transitivity.
        apply cong_symmetry.
        apply cong_commutativity.
        apply H6.
      eapply cong_transitivity.
        apply cong_commutativity.
        apply H1.
      apply cong_left_commutativity.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Per A' B C).
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @Per Tn A' B C) (_ : @Bet Tn A C A'), @eq (@Tpoint Tn) B C *)
      unfold Per.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn B C C') (@Cong Tn A' C A' C')) *)
      exists C'.
      unfold Midpoint.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C E)) (and (@Col Tn P A B) (and (@Col Tn P C E) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C E), @Per Tn U P V)))) *)
      repeat split;auto.
    eapply l8_6.
      apply H9.
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @Per Tn A' B C) (_ : @Bet Tn A C A'), @eq (@Tpoint Tn) B C *)
      unfold Per.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn B C C') (@Cong Tn A' C A' C')) *)
      exists C'.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
      split.
        unfold Midpoint;auto.
      apply H1.
    Between.
Qed.

Lemma l8_8 : forall A B, Per A B A -> A=B.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply l8_7 with A.
(* Goal: @Per Tn U X C *)
      apply l8_2.
(* Goal: @Per Tn B A A *)
(* Goal: @Per Tn A B A *)
      apply l8_5.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma per_distinct : forall A B C, Per A B C -> A <> B -> A <> C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
    intro.
(* Goal: False *)
    subst C.
(* Goal: False *)
    apply H0.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply (l8_8).
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma per_distinct_1 : forall A B C, Per A B C -> B <> C -> A <> C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
    intro.
(* Goal: False *)
    subst C.
(* Goal: False *)
    apply H0.
(* Goal: @eq (@Tpoint Tn) B A *)
    apply eq_sym.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply (l8_8).
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma l8_9 : forall A B C, Per A B C -> Col A B C -> A=B \/ C=B.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
    elim (eq_dec_points A B);intro.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
      tauto.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
    right.
    eapply l8_7.
      eapply l8_2.
(* Goal: @Per Tn B A A *)
(* Goal: @Per Tn A B A *)
      eapply l8_5.
    apply l8_3 with A; Col.
Qed.


Lemma l8_10 : forall A B C A' B' C',  Per A B C -> Cong_3 A B C A' B' C' -> Per A' B' C'.
Proof.
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @Per Tn A' B C) (_ : @Bet Tn A C A'), @eq (@Tpoint Tn) B C *)
    unfold Per.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    ex_and H D.
    prolong C' B' D' B' C'.
    exists D'.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    split.
      unfold Midpoint.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
      split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      Cong.
    unfold Cong_3, Midpoint in *.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
    induction (eq_dec_points C B).
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      treat_equalities;Cong.
    assert(OFSC C B D A C' B' D' A').
      unfold OFSC.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
      repeat split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
        Cong.
        eapply cong_transitivity.
          apply cong_symmetry.
(* Goal: @Per Tn B A C *)
          apply H4.
        eapply cong_transitivity.
          apply cong_commutativity.
          apply H6.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
        Cong.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
        Cong.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      Cong.
    assert (Cong D A D' A').
      eapply five_segment_with_def.
        apply H8.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    eapply cong_transitivity.
      apply cong_symmetry.
(* Goal: False *)
      apply H5.
    eapply cong_transitivity.
      apply H1.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
    Cong.
Qed.

Lemma col_col_per_per : forall A X C U V,
 A<>X -> C<>X ->
 Col U A X ->
 Col V C X ->
 Per A X C ->
 Per U X V.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Per Tn U X V *)
    assert (Per U X C) by (apply (l8_3 A X C U);Col).
(* Goal: @Per Tn U X V *)
    apply l8_2 in H4.
(* Goal: @Per Tn U X C *)
    apply l8_2 .
(* Goal: @Per Tn V X U *)
    apply (l8_3 C X U V);Col.
Qed.

Lemma perp_in_dec : forall X A B C D, Perp_at X A B C D \/ ~ Perp_at X A B C D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), and (@Col Tn A B X) (@Col Tn C D X) *)
    unfold Perp_at.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    elim (eq_dec_points A B);intro; elim (eq_dec_points C D);intro; elim (col_dec X A B);intro; elim (col_dec X C D);intro; try tauto.
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
    elim (eq_dec_points B X);intro; elim (eq_dec_points D X);intro;subst;treat_equalities.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      elim (per_dec A X C);intro.
(* Goal: or (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A X) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C X), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A X) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C X), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A X) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C X), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A X) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C X), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A X) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A X) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
        left;repeat split;Col;intros; apply col_col_per_per with A C;Col.
(* Goal: or (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A X) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C X), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A X) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C X), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A X) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A X) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
      right;intro;spliter;apply H3;apply H8;Col.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      elim (per_dec A X D);intro.
(* Goal: or (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A X) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A X) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A X) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A X) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
        left;repeat split;Col;intros; apply col_col_per_per with A D;Col;ColR.
(* Goal: or (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A X) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A X)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A X) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A X) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
      right;intro;spliter;apply H3;apply H9;Col.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      elim (per_dec B X C);intro.
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
        left;repeat split;Col;intros; apply col_col_per_per with B C;Col;ColR.
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C X)) (and (@Col Tn X A B) (and (@Col Tn X C X) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C X), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
      right;intro;spliter;apply H4;apply H9;Col.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
    elim (per_dec B X D);intro.
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
      left;repeat split;Col;intros; apply col_col_per_per with B D;Col;ColR.
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V))))) (not (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn X A B) (and (@Col Tn X C D) (forall (U V : @Tpoint Tn) (_ : @Col Tn U A B) (_ : @Col Tn V C D), @Per Tn U X V)))))) *)
    right;intro;spliter;apply H5;apply H10;Col.
Qed.

Lemma perp_distinct : forall A B C D, Perp A B C D -> A <> B /\ C <> D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    unfold Perp in H.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    ex_elim H X.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    unfold Perp_at in H0.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    tauto.
Qed.

Lemma l8_12 : forall A B C D X, Perp_at X A B C D -> Perp_at X C D A B.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), and (@Col Tn A B X) (@Col Tn C D X) *)
    unfold Perp_at.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    repeat split;try assumption.
(* Goal: forall (U V : @Tpoint Tn) (_ : @Col Tn U C D) (_ : @Col Tn V A B), @Per Tn U X V *)
    intros;eapply l8_2;eauto.
Qed.

Lemma per_col : forall A B C D,
 B <> C -> Per A B C -> Col B C D -> Per A B D.
Proof.
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @Per Tn A' B C) (_ : @Bet Tn A C A'), @eq (@Tpoint Tn) B C *)
    unfold Per.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    ex_and H0 C'.
    prolong D B D' D B.
    exists D'.
    assert (Midpoint B C C').
(* Goal: False *)
      apply H0.
    induction H5.
    assert (Midpoint B D D') by (unfold Midpoint;split;Cong).
    assert (Midpoint B D D').
      apply H7.
    induction H8.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    repeat split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      Cong.
    unfold Col in H1.
    induction H1.
      assert (Bet B C' D').
        eapply l7_15.
(* Goal: @Midpoint Tn A A A *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
          eapply l7_3_2.
(* Goal: False *)
          apply H0.
          apply H7.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      assert (Cong C D C' D').
        eapply l4_3_1.
          apply H1.
          apply H10.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
          Cong.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
        Cong.
      assert(OFSC B C D A B C' D' A) by (unfold OFSC;repeat split;Cong).
      apply cong_commutativity.
      eauto using five_segment_with_def.
    induction H1.
      assert (Bet C' D' B).
        eapply l7_15.
(* Goal: False *)
          apply H0.
          apply H7.
(* Goal: @Midpoint Tn A A A *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
          apply l7_3_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      assert (Cong C D C' D') by (eapply l4_3 with B B;Between;Cong).
      assert(IFSC B D C A B D' C' A) by (unfold IFSC;repeat split;Between;Cong).
      apply cong_commutativity.
      eauto using l4_2.
    assert (Bet D' B C').
      eapply l7_15.
        apply H7.
(* Goal: @Midpoint Tn A A A *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
        eapply l7_3_2.
(* Goal: False *)
        apply H0.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Cong C D C' D') by (eapply l2_11 with B B;Between;Cong).
    assert(OFSC C B D A C' B D' A) by (unfold OFSC;repeat split;Between;Cong).
    apply cong_commutativity.
    eauto using five_segment_with_def.
Qed.

Lemma l8_13_2 : forall A B C D X,
   A <> B -> C <> D -> Col X A B -> Col X C D ->
  (exists U, exists V :Tpoint, Col U A B /\ Col V C D /\ U<>X /\ V<>X /\ Per U X V) ->
  Perp_at X A B C D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    ex_and H3 U.
    ex_and H4 V.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), and (@Col Tn A B X) (@Col Tn C D X) *)
    unfold Perp_at.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    repeat split;try assumption.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    assert (Per V X U0).
      eapply l8_2.
      eapply l8_3.
        apply H7.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      eapply col3.
(* Goal: False *)
        apply H.
(* Goal: False *)
        Col.
(* Goal: False *)
        Col.
(* Goal: False *)
      Col.
    eapply per_col.
      2:eapply l8_2.
      2:apply H10.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
      auto.
    eapply col3.
(* Goal: False *)
      apply H0.
(* Goal: False *)
      Col.
(* Goal: False *)
      Col.
(* Goal: False *)
    Col.
Qed.

Lemma l8_14_1 : forall A B, ~ Perp A B A B.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp Tn A B C D *)
    unfold Perp.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
    intro.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    ex_and H X.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    unfold Perp_at in H0.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
    assert (Per A X A).
      apply H3.
(* Goal: False *)
        Col.
(* Goal: False *)
      Col.
    assert (A = X).
      eapply l8_7.
(* Goal: @Per Tn B A C *)
        2: apply H4.
(* Goal: @Per Tn U X C *)
      apply l8_2.
(* Goal: @Per Tn B A A *)
(* Goal: @Per Tn A B A *)
      apply l8_5.
    assert (Per B X B) by (apply H3;Col).
    assert (B = X).
      eapply l8_7 with B.
        2: apply H6.
(* Goal: @Per Tn U X C *)
      apply l8_2.
(* Goal: @Per Tn B A A *)
(* Goal: @Per Tn A B A *)
      apply l8_5.
(* Goal: False *)
    apply H0.
    congruence.
Qed.

Lemma l8_14_2_1a : forall X A B C D, Perp_at X A B C D -> Perp A B C D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp Tn A B C D *)
    unfold Perp.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
    exists X.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma perp_in_distinct : forall X A B C D , Perp_at X A B C D -> A <> B /\ C <> D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
    apply l8_14_2_1a in H.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C A)) *)
(* Goal: @eq (@Tpoint Tn) X A *)
    apply perp_distinct.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma l8_14_2_1b : forall X A B C D Y, Perp_at X A B C D -> Col Y A B -> Col Y C D -> X=Y.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @eq (@Tpoint Tn) X A *)
    unfold Perp_at in H.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: @eq (@Tpoint Tn) X Y *)
    apply (H5 Y Y) in H1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      apply eq_sym, l8_8; assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma l8_14_2_1b_bis : forall A B C D X, Perp A B C D -> Col X A B -> Col X C D -> Perp_at X A B C D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    unfold Perp in H.
(* Goal: @Col Tn X C D *)
    ex_and H Y.
(* Goal: @Perp_at Tn X A B C D *)
    assert (Y = X) by (eapply (l8_14_2_1b Y _ _ _ _ X) in H2;assumption).
(* Goal: @Col Tn X C D *)
    subst Y.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma l8_14_2_2 : forall X A B C D,
 Perp A B C D -> (forall Y, Col Y A B -> Col Y C D -> X=Y) ->  Perp_at X A B C D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp_at Tn X A B C D *)
    eapply l8_14_2_1b_bis.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
      unfold Perp in H.
(* Goal: @Col Tn X C D *)
      ex_and H Y.
(* Goal: @Col Tn X C D *)
      unfold Perp_at in H1.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assert (Col Y C D) by assumption.
(* Goal: @Col Tn X C D *)
      apply (H0 Y H2) in H3.
(* Goal: @Col Tn X C D *)
      subst Y.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    unfold Perp in H.
(* Goal: @Col Tn X C D *)
    ex_and H Y.
(* Goal: @Col Tn X C D *)
    unfold Perp_at in H1.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: @Col Tn X C D *)
    assert (Col Y C D).
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Col Tn X C D *)
    apply (H0 Y H2) in H3.
(* Goal: @Col Tn X C D *)
    subst Y.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma l8_14_3 : forall A B C D X Y, Perp_at X A B C D -> Perp_at Y A B C D -> X=Y.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    eapply l8_14_2_1b.
(* Goal: False *)
      apply H.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
      unfold Perp_at in H0.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
      intuition.
    eapply l8_12 in H0.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    unfold Perp_at in H0.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    intuition.
Qed.

Lemma l8_15_1 : forall A B C X, Col A B X -> Perp A B C X -> Perp_at X A B C X.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: False *)
    eapply l8_14_2_1b_bis;Col.
Qed.

Lemma l8_15_2 : forall A B C X, Col A B X ->  Perp_at X A B C X -> Perp A B C X.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    eapply l8_14_2_1a.
(* Goal: False *)
    apply H0.
Qed.

Lemma perp_in_per : forall A B C, Perp_at B A B B C-> Per A B C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @eq (@Tpoint Tn) X A *)
    unfold Perp_at in H.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: False *)
    apply H3;Col.
Qed.

Lemma perp_sym : forall A B C D, Perp A B C D -> Perp C D A B.
Proof.
(* Goal: @Perp Tn A B C D *)
    unfold Perp.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    ex_and H X.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
    exists X.
(* Goal: @Perp_at Tn X C D A B *)
    apply l8_12.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma perp_col0 : forall A B C D X Y, Perp A B C D -> X <> Y -> Col A B X -> Col A B Y -> Perp C D X Y.
Proof.
(* Goal: @Perp Tn A B C D *)
    unfold Perp.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    ex_and H X0.
    exists X0.
(* Goal: @Per Tn B X D *)
    unfold Perp_at in *.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    repeat split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
      eapply col3.
(* Goal: False *)
        apply H.
(* Goal: False *)
        Col.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    eapply l8_2.
    apply H6.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      2:assumption.
    assert(Col A X Y).
(* Goal: False *)
      eapply col3 with A B;Col.
    assert (Col B X Y).
(* Goal: False *)
      eapply col3 with A B;Col.
(* Goal: False *)
    eapply col3 with X Y;Col.
Qed.

Lemma per_perp_in : forall A B C, A <> B -> B <> C -> Per A B C -> Perp_at B A B B C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp Tn A B C D *)
    unfold Perp.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    repeat split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: False *)
      Col.
(* Goal: False *)
      Col.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    eapply per_col.
(* Goal: False *)
      apply H0.
      eapply l8_2.
      eapply per_col.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
        intro.
(* Goal: False *)
        apply H.
        apply sym_equal.
(* Goal: @Per Tn B A C *)
        apply H4.
(* Goal: @Per Tn U X C *)
        apply l8_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: False *)
      Col.
(* Goal: False *)
    Col.
Qed.

Lemma per_perp : forall A B C, A <> B -> B <> C -> Per A B C -> Perp A B B C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp Tn A B B C *)
    apply per_perp_in in H1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      eapply l8_14_2_1a with B;assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma perp_left_comm : forall A B C D, Perp A B C D -> Perp B A C D.
Proof.
(* Goal: @Perp Tn A B C D *)
    unfold Perp.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    ex_and H X.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
    exists X.
(* Goal: @Per Tn B X D *)
    unfold Perp_at in *.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    intuition.
Qed.

Lemma perp_right_comm : forall A B C D, Perp A B C D -> Perp A B D C.
Proof.
(* Goal: @Perp Tn A B C D *)
    unfold Perp.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    ex_and H X.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
    exists X.
(* Goal: @Per Tn B X D *)
    unfold Perp_at in *.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    intuition.
Qed.

Lemma perp_comm : forall A B C D, Perp A B C D -> Perp B A D C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp Tn B A D C *)
    apply perp_left_comm.
(* Goal: @Perp Tn A B C B *)
(* Goal: @Col Tn C B D *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
    apply perp_right_comm.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma perp_in_sym :
 forall A B C D X,
  Perp_at X A B C D -> Perp_at X C D A B.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), and (@Col Tn A B X) (@Col Tn C D X) *)
    unfold Perp_at.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    repeat split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Per Tn U X C *)
    apply l8_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    apply H3;assumption.
Qed.

Lemma perp_in_left_comm :
 forall A B C D X,
  Perp_at X A B C D -> Perp_at X B A C D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), and (@Col Tn A B X) (@Col Tn C D X) *)
    unfold Perp_at.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    intuition.
Qed.

Lemma perp_in_right_comm : forall A B C D X, Perp_at X A B C D -> Perp_at X A B D C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp_at Tn A P A A B *)
(* Goal: not (@Col Tn A B P) *)
    apply perp_in_sym.
(* Goal: @Perp_at Tn X B A D C *)
    apply perp_in_left_comm.
(* Goal: @Perp_at Tn A P A A B *)
(* Goal: not (@Col Tn A B P) *)
    apply perp_in_sym.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma perp_in_comm : forall A B C D X, Perp_at X A B C D -> Perp_at X B A D C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp_at Tn X B A D C *)
    apply perp_in_left_comm.
(* Goal: @Perp_at Tn A B A A P *)
    apply perp_in_right_comm.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

End T8_3.

Hint Resolve perp_sym perp_left_comm perp_right_comm perp_comm per_perp_in per_perp
             perp_in_per perp_in_left_comm perp_in_right_comm perp_in_comm perp_in_sym : perp.

Ltac double A B A' :=
   assert (mp:= symmetric_point_construction A B);
   elim mp; intros A' ; intro; clear mp.

Section T8_4.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma Perp_cases :
  forall A B C D,
  Perp A B C D \/ Perp B A C D \/ Perp A B D C \/ Perp B A D C \/
  Perp C D A B \/ Perp C D B A \/ Perp D C A B \/ Perp D C B A ->
  Perp A B C D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp_at Tn X A B C D *)
    decompose [or] H; Perp.
Qed.

Lemma Perp_perm :
  forall A B C D,
  Perp A B C D ->
  Perp A B C D /\ Perp B A C D /\ Perp A B D C /\ Perp B A D C /\
  Perp C D A B /\ Perp C D B A /\ Perp D C A B /\ Perp D C B A.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: and (@Per Tn A B C) (@Per Tn C B A) *)
    repeat split; Perp.
Qed.

Lemma Perp_in_cases :
  forall X A B C D,
  Perp_at X A B C D \/ Perp_at X B A C D \/ Perp_at X A B D C \/ Perp_at X B A D C \/
  Perp_at X C D A B \/ Perp_at X C D B A \/ Perp_at X D C A B \/ Perp_at X D C B A ->
  Perp_at X A B C D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp Tn A B B P *)
    decompose [or]  H; Perp.
Qed.

Lemma Perp_in_perm :
  forall X A B C D,
  Perp_at X A B C D ->
  Perp_at X A B C D /\ Perp_at X B A C D /\ Perp_at X A B D C /\ Perp_at X B A D C /\
  Perp_at X C D A B /\ Perp_at X C D B A /\ Perp_at X D C A B /\ Perp_at X D C B A.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: and (@Perp_at Tn X A B C D) (and (@Perp_at Tn X B A C D) (and (@Perp_at Tn X A B D C) (and (@Perp_at Tn X B A D C) (and (@Perp_at Tn X C D A B) (and (@Perp_at Tn X C D B A) (and (@Perp_at Tn X D C A B) (@Perp_at Tn X D C B A))))))) *)
    do 7 (split; Perp).
Qed.

Lemma perp_in_col : forall A B C D X, Perp_at X A B C D -> Col A B X /\ Col C D X.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), and (@Col Tn A B X) (@Col Tn C D X) *)
    unfold Perp_at.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    intuition.
Qed.

Lemma perp_perp_in : forall A B C, Perp A B C A -> Perp_at A A B C A.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp_at Tn A A B C A *)
    apply l8_15_1.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
      unfold Perp in H.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
      ex_and H X.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
      unfold Perp_at in H0.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
      intuition.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma perp_per_1 : forall A B C, Perp A B C A -> Per B A C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Per Tn B A C *)
    assert (Perp_at A A B C A).
(* Goal: @Perp_at Tn A A B P A *)
(* Goal: not (@Col Tn A B P) *)
      apply perp_perp_in.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    unfold Perp_at in H0.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: @Per Tn B A C *)
    apply H4.
(* Goal: False *)
    Col.
(* Goal: False *)
    Col.
Qed.

Lemma perp_per_2 : forall A B C, Perp A B A C -> Per B A C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Per Tn B A C *)
    apply perp_right_comm in H.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    apply perp_per_1; assumption.
Qed.

Lemma perp_col : forall A B C D E, A<>E -> Perp A B C D -> Col A B E -> Perp A E C D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp Tn A B C X *)
    apply perp_sym.
(* Goal: @Perp Tn C D A E *)
    apply perp_col0 with A B;finish.
Qed.

Lemma perp_col2 : forall A B C D  X Y,
  Perp A B X Y ->
  C <> D -> Col A B C -> Col A B D -> Perp C D X Y.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp Tn C D X Y *)
    assert(HH:=H).
(* Goal: @Perp Tn C D X Y *)
    apply perp_distinct in HH.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: @Perp Tn C D X Y *)
    induction (eq_dec_points A C).
(* Goal: @Perp Tn C D X Y *)
(* Goal: @Perp Tn C D X Y *)
      subst A.
(* Goal: @Perp Tn C D X Y *)
(* Goal: @Perp Tn C D X Y *)
      apply perp_col with B;finish.
(* Goal: @Perp Tn C D X Y *)
    assert(Perp A C X Y) by (eapply perp_col;eauto).
(* Goal: @Perp Tn C X A B *)
    eapply perp_col with A;finish.
(* Goal: @Perp Tn A B B P *)
      Perp.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
    ColR.
Qed.

Lemma perp_not_eq_1 : forall A B C D, Perp A B C D -> A<>B.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    unfold Perp in H.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    ex_elim H X.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    unfold Perp_at in H0.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    tauto.
Qed.

Lemma perp_not_eq_2 : forall A B C D, Perp A B C D -> C<>D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    apply perp_sym in H.
    eapply perp_not_eq_1.
(* Goal: False *)
    apply H.
Qed.

Lemma diff_per_diff : forall A B P R ,
      A <> B -> Cong A P B R -> Per B A P -> Per A B R -> P <> R.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
    intro.
(* Goal: False *)
    subst.
    assert (A = B).
      eapply l8_7.
(* Goal: @Per Tn U X C *)
        apply l8_2.
        apply H1.
(* Goal: @Per Tn U X C *)
      apply l8_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    intuition.
Qed.

Lemma per_not_colp : forall A B P R, A <> B -> A <> P -> B <> R -> Per B A P -> Per A B R -> ~Col P A R.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
    intro.
    assert (Perp A B P A).
(* Goal: @Perp Tn O P A B *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp Tn O X A B) *)
      apply perp_comm.
      apply per_perp;finish.
    assert (Perp A B B R).
      apply per_perp;finish.
    assert (Per B A R).
      eapply per_col.
(* Goal: False *)
        apply H0.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
      ColR.
    apply l8_2 in H3.
    apply l8_2 in H7.
    assert (A = B).
      eapply l8_7.
        apply H7.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
    contradiction.
Qed.

Lemma per_not_col : forall A B C, A <> B -> B <> C -> Per A B C -> ~Col A B C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
    intro.
(* Goal: False *)
    unfold Per in H1.
(* Goal: False *)
    ex_and H1 C'.
(* Goal: False *)
    assert (C = C' \/ Midpoint A C C').
(* Goal: or (@eq (@Tpoint Tn) C C') (@Midpoint Tn A C C') *)
(* Goal: False *)
      eapply l7_20.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
        assert_cols;ColR.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    induction H4;treat_equalities; intuition.
Qed.

Lemma perp_not_col2 : forall A B C D, Perp A B C D -> ~ Col A B C \/ ~ Col A B D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
    induction (col_dec A B C).
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
      right.
      assert(Perp_at C A B C D).
(* Goal: False *)
        apply l8_14_2_1b_bis; Col.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      assert(Perp_at D A B C D).
(* Goal: False *)
        apply l8_14_2_1b_bis; Col.
      assert(C = D).
        eapply l8_14_3.
          apply H1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply perp_not_eq_2 in H.
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      contradiction.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
    left.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma perp_not_col : forall A B P, Perp A B P A -> ~ Col A B P.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@Col Tn A B P) *)
    assert (Perp_at A A B P A).
(* Goal: @Perp_at Tn A A B P A *)
(* Goal: not (@Col Tn A B P) *)
      apply perp_perp_in.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: not (@Col Tn A B P) *)
    assert (Per P A B).
(* Goal: @Per Tn B A P *)
      apply perp_in_per.
(* Goal: @Perp_at Tn A P A A B *)
(* Goal: not (@Col Tn A B P) *)
      apply perp_in_sym.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: not (@Col Tn A B P) *)
    apply perp_in_left_comm in H0.
    assert (~ Col B A P  -> ~ Col A B P).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
(* Goal: @Perp Tn A B O X *)
      apply H2.
(* Goal: @Col Tn C B D *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      apply col_permutation_4.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Perp Tn A B O X *)
    apply H2.
(* Goal: not (@Col Tn B A P) *)
    apply perp_distinct in H.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: not (@Col Tn B A P) *)
    apply per_not_col.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
      auto.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
      auto.
(* Goal: @Per Tn B A P *)
    apply perp_in_per.
(* Goal: @Perp_at Tn A B A A P *)
    apply perp_in_right_comm.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma perp_in_col_perp_in : forall A B C D E P, C <> E -> Col C D E -> Perp_at P A B C D -> Perp_at P A B C E.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Per Tn B X D *)
    unfold Perp_at in *.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
    repeat split; auto.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
      ColR.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: False *)
    apply H5.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
    ColR.
Qed.

Lemma perp_col2_bis : forall A B C D P Q,
  Perp A B P Q ->
  Col C D P ->
  Col C D Q ->
  C <> D ->
  Perp A B C D.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @Perp Tn A B P Q) (_ : @Col Tn C D P) (_ : @Col Tn C D Q) (_ : not (@eq (@Tpoint Tn) C D)), @Perp Tn A B C D *)
intros A B C D P Q HPerp HCol1 HCol2 HCD.
(* Goal: @Perp Tn A B C X *)
apply perp_sym.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
apply perp_col2 with P Q; Perp; ColR.
Qed.

Lemma perp_in_perp_bis : forall A B C D X,
 Perp_at X A B C D -> Perp X B C D \/ Perp A X C D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    induction (eq_dec_points X A).
(* Goal: False *)
      subst X.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      left.
(* Goal: @Perp Tn A B C D *)
      unfold Perp.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A A) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
      exists A.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
    right.
(* Goal: @Perp Tn A B C D *)
    unfold Perp.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
    exists X.
(* Goal: @Per Tn B X D *)
    unfold Perp_at in *.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    repeat split.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
(* Goal: False *)
      apply H0.
(* Goal: False *)
      subst X.
      reflexivity.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
      apply col_trivial_3.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Per Tn B A C *)
    apply H4.
      apply col_permutation_2.
      eapply col_transitivity_1.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
        intro.
(* Goal: False *)
        apply H0.
        apply sym_equal.
        apply H7.
(* Goal: False *)
        Col.
(* Goal: False *)
      Col.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma col_per_perp : forall A B C D,
 A <> B -> B <> C -> D <> B -> D <> C ->
 Col B C D -> Per A B C -> Perp C D A B.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp_at Tn M X M A B *)
    apply per_perp_in in H4.
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      apply perp_in_perp_bis in H4.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn Q T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
      induction H4.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
        apply perp_distinct in H4.
(* Goal: @eq (@Tpoint Tn) X A *)
        spliter.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
        absurde.
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      eapply (perp_col _ B).
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
        auto.
(* Goal: @Perp Tn A B C X *)
        apply perp_sym.
(* Goal: @Perp Tn A B C B *)
(* Goal: @Col Tn C B D *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
        apply perp_right_comm.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Col Tn C B D *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      apply col_permutation_4.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma per_cong_mid : forall A B C H,
 B <> C -> Bet A B C -> Cong A H C H -> Per H B C ->
 Midpoint B A C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    induction (eq_dec_points H B).
      subst H.
      unfold Midpoint.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
      split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply cong_right_commutativity.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert(Per C B H).
(* Goal: @Per Tn U X C *)
      apply l8_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Per H B A).
      eapply per_col.
(* Goal: False *)
        apply H0.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      unfold Col.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
      right; right.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Per A B H).
(* Goal: @Per Tn U X C *)
      apply l8_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    unfold Per in *.
    ex_and H3 C'.
    ex_and H5 H'.
    ex_and H6 A'.
    ex_and H7 H''.
    assert (H' = H'').
      eapply construction_uniqueness.
        2: apply  midpoint_bet.
(* Goal: False *)
        2:apply H5.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        apply cong_commutativity.
        apply midpoint_cong.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
(* Goal: False *)
        apply H5.
        apply midpoint_bet.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply cong_commutativity.
      apply midpoint_cong.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
      apply l7_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    subst H''.
    assert(IFSC H B H' A H B H' C).
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
      repeat split.
        apply midpoint_bet.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        apply midpoint_bet.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        apply cong_reflexivity.
        apply cong_reflexivity.
        apply cong_commutativity.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply cong_commutativity.
      eapply cong_transitivity.
        apply cong_symmetry.
        apply H11.
      eapply cong_transitivity.
(* Goal: @Perp Tn A B O X *)
        apply H2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    eapply l4_2 in H12.
    unfold Midpoint.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    apply cong_left_commutativity.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma per_double_cong : forall A B C C',
 Per A B C -> Midpoint B C C' -> Cong A C A C'.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    unfold Per in H.
    ex_and H C''.
    assert (C' = C'').
      eapply l7_9.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
(* Goal: False *)
        apply H0.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
      apply l7_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @eq (@Tpoint Tn) B C *)
    subst C''.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma cong_perp_or_mid : forall A B M X, A <> B -> Midpoint M A B -> Cong A X B X ->
 X = M \/ ~Col A B X /\ Perp_at M X M A B.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
intros.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
induction(col_dec A B X).
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
left.
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
assert(A = B \/ Midpoint X A B).
(* Goal: False *)
apply l7_20; Col.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
Cong.
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
induction H3.
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
contradiction.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
apply (l7_17 A B); auto.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
right.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
split; auto.
(* Goal: @Perp_at Tn M X M A B *)
assert(Col M A B).
(* Goal: @Col Tn M A B *)
(* Goal: @Perp_at Tn M X M A B *)
unfold Midpoint in *.
(* Goal: False *)
spliter; Col.

(* Goal: @Perp_at Tn M X M A B *)
assert_diffs.
assert(Per X M A)
 by (unfold Per;exists B;split; Cong).
(* Goal: @Perp_at Tn M X M A B *)
apply per_perp_in in H4.
(* Goal: @Perp_at Tn M X M A B *)
(* Goal: not (@eq (@Tpoint Tn) X M) *)
(* Goal: not (@eq (@Tpoint Tn) M A) *)
apply perp_in_right_comm in H4.
(* Goal: False *)
apply(perp_in_col_perp_in X M A M B M); Col.

(* Goal: not (@eq (@Tpoint Tn) X M) *)
(* Goal: not (@eq (@Tpoint Tn) M A) *)
intro;treat_equalities.
(* Goal: False *)
apply H2; Col.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
auto.
Qed.

Lemma col_per2_cases : forall A B C D B', 
 B <> C -> B' <> C -> C <> D -> Col B C D -> Per A B C -> Per A B' C -> 
 B = B' \/ ~Col B' C D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
intros.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
induction(eq_dec_points B B').
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
left; auto.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
right.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
intro.
(* Goal: False *)
assert(Col C B B').
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
ColR.
(* Goal: False *)
assert(Per A B' B).
(* Goal: False *)
apply(per_col A B' C B H0 H4); Col.
(* Goal: False *)
assert(Per A B B').
(* Goal: False *)
apply(per_col A B C B' H H3); Col.
(* Goal: False *)
apply H5.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
apply (l8_7 A); auto.
Qed.

Lemma l8_16_1 : forall A B C U X,
  Col A B X -> Col A B U -> Perp A B C X -> ~ Col A B C /\ Per C X U.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
      intros.
      destruct (eq_dec_points U X).
(* Goal: False *)
        subst X.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
        split.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
          destruct (perp_not_col2 A B C U); auto.
(* Goal: @Per Tn B A A *)
(* Goal: @Per Tn A B A *)
        apply l8_5.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
      split.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
        intro.
        assert (Perp_at X A B C X).
(* Goal: @Perp_at Tn A A B C A *)
          eapply l8_15_1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
            assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
        assert (X = U).
          eapply l8_14_2_1b.
(* Goal: @Per Tn B A C *)
            apply H4.
(* Goal: False *)
            Col.
(* Goal: False *)
          eapply col3 with A B;Col.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
          apply perp_distinct in H1; spliter; auto.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
        intuition.
(* Goal: False *)
      apply l8_14_2_1b_bis with C X U X;try Col.
      assert (Col A X U).
(* Goal: False *)
        eapply (col3 A B);Col.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
        apply perp_distinct in H1; spliter; auto.
(* Goal: False *)
      eapply perp_col0 with A B;Col.
Qed.

Lemma l8_16_2 : forall A B C U X,
  Col A B X -> Col A B U -> U<>X -> ~ Col A B C -> Per C X U -> Perp A B C X.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp Tn A B C X *)
    assert (C <> X).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
(* Goal: False *)
      subst X.
(* Goal: @Perp Tn A B O X *)
      apply H2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Perp Tn A B C D *)
    unfold Perp.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
    exists X.
(* Goal: @Perp_at Tn X A B C X *)
    eapply l8_13_2.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
      assert_diffs; auto.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: False *)
      Col.
(* Goal: False *)
      Col.
(* Goal: @ex (@Tpoint Tn) (fun U : @Tpoint Tn => @ex (@Tpoint Tn) (fun V : @Tpoint Tn => and (@Col Tn U A B) (and (@Col Tn V C X) (and (not (@eq (@Tpoint Tn) U X)) (and (not (@eq (@Tpoint Tn) V X)) (@Per Tn U X V)))))) *)
    exists U.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
    exists C.
(* Goal: False *)
    repeat split; Col.
(* Goal: @Per Tn U X C *)
    apply l8_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma l8_18_uniqueness : forall A B C X Y,
  ~ Col A B C -> Col A B X -> Perp A B C X -> Col A B Y -> Perp A B C Y -> X=Y.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @eq (@Tpoint Tn) X Y *)
    show_distinct A B.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) X Y *)
      solve [intuition].
(* Goal: @eq (@Tpoint Tn) X Y *)
    assert (Perp_at X A B C X) by (eapply l8_15_1;assumption).
(* Goal: @eq (@Tpoint Tn) X Y *)
    assert (Perp_at Y A B C Y) by (eapply l8_15_1;assumption).
(* Goal: @Per Tn B X D *)
    unfold Perp_at in *.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: False *)
    apply l8_7 with C;apply l8_2;[apply H14 |apply H10];Col.
Qed.

Lemma midpoint_distinct : forall A B X C C', ~ Col A B C -> Col A B X -> Midpoint X C C' -> C <> C'.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
    intro.
(* Goal: False *)
    subst C'.
(* Goal: False *)
    apply H.
(* Goal: @Col Tn A B C *)
    unfold Midpoint in H1.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: @Col Tn A B C *)
    treat_equalities.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma l8_20_1 : forall A B C C' D P,
  Per A B C -> Midpoint P C' D -> Midpoint A C' C -> Midpoint B D C -> Per B A P.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    double B A B'.
    double D A D'.
    double P A P'.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
    induction (eq_dec_points A B).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
      subst B.
      unfold Midpoint in H5.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
      eapply l8_2.
(* Goal: @Per Tn B A A *)
(* Goal: @Per Tn A B A *)
      eapply l8_5.
    assert (Per B' B C).
      eapply l8_3.
(* Goal: False *)
        apply H.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      unfold Col.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      left.
      apply midpoint_bet.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Per B B' C').
      eapply l8_10.
        apply H7.
      unfold Cong_3.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
      repeat split.
        apply cong_pseudo_reflexivity.
        eapply l7_13.
          unfold Midpoint.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
          split.
            apply H3.
          apply midpoint_cong.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      eapply l7_13.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
        apply H3.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert(Midpoint B' D' C').
      eapply symmetry_preserves_midpoint.
(* Goal: @Per Tn B A C *)
        apply H4.
        apply H3.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
        apply H1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert(Midpoint P' C D').
      eapply symmetry_preserves_midpoint.
        apply H1.
(* Goal: False *)
        apply H5.
(* Goal: @Per Tn B A C *)
        apply H4.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @Per Tn A' B C) (_ : @Bet Tn A C A'), @eq (@Tpoint Tn) B C *)
    unfold Per.
    exists P'.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    unfold Per in H7.
    ex_and H7 D''.
    assert (D''= D).
      eapply symmetric_point_uniqueness.
        apply H7.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
      apply l7_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    subst D''.
    unfold Per in H8.
    ex_and H8 D''.
    assert (D' = D'').
      eapply symmetric_point_uniqueness.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
        apply H9.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    subst D''.
    assert (Midpoint P C' D).
      eapply symmetry_preserves_midpoint.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
        apply H1.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
(* Goal: False *)
        apply H5.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
(* Goal: @Per Tn B A C *)
        apply H4.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Cong C D C' D').
      eapply l7_13.
        apply H1.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
      apply l7_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Cong C' D C D').
      eapply l7_13.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
        apply H1.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
      apply l7_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert(Cong P D P' D').
      eapply l7_13.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
(* Goal: False *)
        apply H5.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
      apply l7_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Cong P D P' C).
      eapply cong_transitivity.
        apply H16.
      unfold Midpoint in H10.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
      apply cong_right_commutativity.
      apply cong_symmetry.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (IFSC C' P D B D' P' C B).
      unfold IFSC.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
      repeat split.
        apply midpoint_bet.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        apply midpoint_bet.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        apply cong_right_commutativity.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        apply cong_commutativity.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply cong_right_commutativity.
      apply midpoint_cong.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Cong P B P' B).
      eapply l4_2.
      apply H18.
    apply cong_commutativity.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma l8_20_2 : forall A B C C' D P,
  Per A B C -> Midpoint P C' D -> Midpoint A C' C -> Midpoint B D C -> B<>C -> A<>P.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
    intro.
    subst P.
    assert (C = D).
      eapply symmetric_point_uniqueness.
        apply H1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    subst D.
    assert (B = C).
(* Goal: @eq (@Tpoint Tn) B C *)
      apply l7_3.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: False *)
    subst C.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
    absurde.
Qed.

Lemma perp_col1 : forall A B C D X,
 C <> X -> Perp A B C D -> Col C D X -> Perp A B C X.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    assert (T:=perp_distinct A B C D H0).
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
    unfold Perp in *.
    ex_and H0 P.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
    exists P.
(* Goal: @Per Tn B X D *)
    unfold Perp_at in *.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    repeat split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
      apply col_permutation_2.
      eapply col_transitivity_2.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
        intro.
        apply H3.
        apply sym_equal.
        apply H8.
(* Goal: @Col Tn C B D *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
        apply col_permutation_4.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply col_permutation_3.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    apply H7.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    apply col_permutation_2.
    eapply col_transitivity_1.
(* Goal: False *)
      apply H.
      apply col_permutation_5.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    apply col_permutation_1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.




Lemma l8_18_existence : forall A B C, ~ Col A B C -> exists X, Col A B X /\ Perp A B C X.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    prolong B A Y A C.
    assert (exists P, Midpoint P C Y) by (apply l7_25 with A;Cong).
    ex_and H2 P.
    assert (Per A P Y) by (unfold Per;exists C;auto using l7_2).
    prolong A Y Z Y P.
    prolong P Y Q Y A.
    prolong Q Z Q' Q Z.
    assert (Midpoint Z Q Q') by (unfold Midpoint;split;Cong).
    prolong Q' Y C' Y C.
    assert (exists X, Midpoint X C C') by (apply l7_25 with Y;Cong).
    ex_and H13 X.
    assert (OFSC A Y Z Q Q Y P A) by (unfold OFSC;repeat split;Between;Cong).
    show_distinct A Y.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
      intuition.
    assert (Cong Z Q P A) by (eauto using five_segment_with_def).
    assert (Cong_3 A P Y Q Z Y) by (unfold Cong_3;repeat split;Cong).
    assert (Per Q Z Y) by (eauto using l8_10).
    assert (Per Y Z Q) by eauto using l8_2.
    (* diversion *)
    show_distinct P Y.
(* Goal: @Col Tn M A B *)
(* Goal: @Perp_at Tn M X M A B *)
      unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: @Col Tn A B C *)
      treat_equalities.
      assert_cols.
      Col5.
    unfold Per in H19.
    ex_and H19 Q''.
    assert (Q' = Q'').
      eapply symmetric_point_uniqueness.
        apply H10.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    subst Q''.
    assert (hy:Bet Z Y X).
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      apply (l7_22 Q C Q' C' Y Z X);Cong.
      assert (T:=outer_transitivity_between2 C P Y Q).
      assert_bets.
      apply between_symmetry.
      apply T;Between.
    show_distinct Q Y.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
      intuition.
    assert (Per Y X C) by (unfold Per;exists C';split;Cong).
(* Goal: @Perp_at Tn M X M A B *)
    assert_diffs.
    assert (Col P Y Q).
      unfold Col.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      left.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert(Col P Y C).
      unfold Midpoint in H3.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
      unfold Col.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
      right; right.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
    assert (Col P Q C) by ColR.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
    assert (Col Y Q C) by ColR.
    assert (Col A Y B) by (assert_cols;Col).
    assert (Col A Y Z) by (assert_cols;Col).
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
    assert (Col A B Z) by ColR.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
    assert (Col Y B Z) by ColR.
(* Goal: False *)
    assert (Col Q Y P) by Col.
    assert(Q <> C).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      subst Q.
(* Goal: @Col Tn M A B *)
(* Goal: @Perp_at Tn M X M A B *)
      unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: False *)
      apply H.
      assert (Bet B Y Z) by (apply outer_transitivity_between2 with A;auto).
      apply between_symmetry in H3.
      assert (Y = P).
        eapply between_equality.
          apply H3.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Col Tn A B C *)
      treat_equalities.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
      intuition.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
    assert (Col Y B Z) by ColR. 
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    show_distinct Y Q'. intuition.
    assert (Col Y Q' C') by (assert_cols;Col).
    assert (Q <> Q').
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      unfold OFSC, Cong_3 in *.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: @Col Tn A B C *)
      treat_equalities.
(* Goal: False *)
      apply H.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
      ColR.
    assert (C <> C').
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
(* Goal: False *)
      subst C'.
      apply l7_3 in H14.
(* Goal: False *)
      subst X.
      assert (Col Z Q Q') by (assert_cols;ColR).
      assert (Y <> Z).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
        intro.
        subst Z.
        unfold OFSC, Cong_3, Midpoint in *.
(* Goal: @eq (@Tpoint Tn) X A *)
        spliter.
(* Goal: @Col Tn A B C *)
        treat_equalities.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
        intuition.
(* Goal: False *)
      apply H.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
      ColR.
    (* end of C<>C' *)
    assert(OFSC Q Y C Z Q' Y C' Z).
      unfold OFSC.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      repeat split;Between;Cong.
      unfold OFSC, Midpoint in *.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      eapply outer_transitivity_between with P;Between;Cong.
    assert (Cong C Z C' Z) by (eauto using five_segment_with_def).
    assert (Col Z Y X) by (assert_cols;Col).
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    show_distinct Y Z. intuition.
(* Goal: @Perp Tn A B C X *)
    assert(C <> X).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
(* Goal: False *)
      subst X.
      unfold OFSC,Cong_3,Midpoint in *.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: @Col Tn A B C *)
      treat_equalities.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
      intuition.
    assert(X <> Y).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
(* Goal: False *)
      subst X.
      unfold OFSC,Cong_3,Midpoint in *.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
      clean_duplicated_hyps.
      clean_trivial_hyps.
      show_distinct C' Y.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
        intuition.
      assert (Col Y C' P ).
        eapply col_transitivity_1 with C.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
          intuition.
          unfold Col.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
          right;right.
          apply between_symmetry.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
        apply col_permutation_1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      show_distinct P Q.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
        intuition.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
      assert (Col Y P Q') by ColR.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
      assert (Col Y Q Q') by ColR.
      assert (Col Q Y Z) by (assert_cols;ColR).
      assert (Col Y Z C) by (assert_bets;assert_cols;ColR).
(* Goal: False *)
      apply H.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
      ColR.
    assert (Perp_at X Y Z C X).
(* Goal: False *)
      eapply l8_13_2;Col.
      exists Y.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
      exists C.
(* Goal: False *)
      repeat split;Col.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
    assert (Col A B X) by ColR.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
    exists X.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Perp Tn A B C D *)
    unfold Perp.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
    exists X.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), and (@Col Tn A B X) (@Col Tn C D X) *)
    unfold Perp_at.
(* Goal: False *)
    repeat split;Col.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    unfold Perp_at in H52.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
    apply H57;ColR.
Qed.


Lemma l8_21_aux : forall A B C,
 ~ Col A B C -> exists P, exists T, Perp A B P A /\ Col A B T /\ Bet C T P.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    assert (exists X : Tpoint, Col A B X /\ Perp A B C X).
      eapply l8_18_existence.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    ex_and H0 X.
    assert (Perp_at X A B C X).
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
      eapply l8_15_1; assert_diffs; auto.
    assert (Per A X C).
      unfold Perp_at in H2.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
      apply H6.
        apply col_trivial_1.
      apply col_trivial_1.
    assert(HH:= H3).
    unfold Per in H3.
    ex_and H3 C'.
    double C A C''.
    assert (exists P, Midpoint P C' C'').
      eapply l7_25.
(* Goal: @Col Tn M A B *)
(* Goal: @Perp_at Tn M X M A B *)
      unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
      eapply cong_transitivity.
        apply cong_symmetry.
(* Goal: @Per Tn B A C *)
        apply H4.
      apply cong_left_commutativity.
(* Goal: @eq (@Tpoint Tn) X A *)
      assumption; spliter.
    ex_elim H6 P.
    assert (Per X A P).
      eapply l8_20_1.
        apply HH.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
        apply H7.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
(* Goal: False *)
        apply H5.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
      apply l7_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (X <> C).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
(* Goal: False *)
      subst C.
(* Goal: False *)
      apply H.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (A <> P).
      eapply l8_20_2.
        apply HH.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
        apply H7.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (exists T, Bet P T C /\ Bet A T X).
      eapply l3_17.
        apply midpoint_bet.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
(* Goal: False *)
        apply H5.
        apply midpoint_bet.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
        apply l7_2.
        apply H3.
      apply midpoint_bet.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
      apply l7_2.
      apply H7.
    ex_and H10 T.
    induction (eq_dec_points A X).
(* Goal: False *)
      subst X.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
      exists P.
      exists T.
      apply between_identity in H11.
      subst T.
      assert (C'= C'').
        eapply symmetric_point_uniqueness.
          apply H3.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @eq (@Tpoint Tn) B C *)
      subst C''.
      apply l7_3 in H7.
      subst P.
      assert (Col A C C') by (assert_cols;ColR).
      repeat split;Col;Between.
(* Goal: False *)
      apply perp_col0 with C A;auto using perp_sym;assert_cols;Col.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
    exists P.
    exists T.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    repeat split.
(* Goal: @Perp Tn A B C D *)
      unfold Perp.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A A) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
      exists A.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), and (@Col Tn A B X) (@Col Tn C D X) *)
      unfold Perp_at.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
      repeat split.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
        assert_diffs; auto.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
        auto.
        apply col_trivial_1.
        apply col_trivial_3.
      unfold Perp_at in H2.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
      intros.
      eapply per_col in H6.
        apply l8_2 in H6.
        eapply per_col in H6.
          eapply l8_2 in H6.
          apply H6.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
        ColR.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
      ColR.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
      assert_cols;ColR.
    Between.
Qed.

Lemma l8_21 : forall A B C,
 A <> B -> exists P, exists T, Perp A B P A /\ Col A B T /\ Bet C T P.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
    induction(col_dec A B C).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
      assert (exists C', ~ Col A B C').
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => not (@Col Tn A B C')) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
        eapply not_col_exists.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
      ex_elim H1 C'.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
      assert ( exists P : Tpoint, (exists T : Tpoint, Perp A B P A /\ Col A B T /\ Bet C' T P)).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
        eapply l8_21_aux.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
      ex_elim H1 P.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
      ex_and H3 T.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
      exists P.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
      exists C.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
      repeat split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Bet Tn C C P *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
      apply between_trivial2.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn C T P)))) *)
    eapply l8_21_aux.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma per_cong : forall A B P R X ,
 A <> B -> A <> P ->
 Per B A P -> Per A B R ->
 Cong A P B R -> Col A B X -> Bet P X R ->
 Cong A R P B.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@Col Tn A B P) *)
    assert (Per P A B).
(* Goal: @Per Tn U X C *)
      apply l8_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    double B R Q.
    assert (B <> R).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      subst R.
      apply cong_identity in H3.
      subst P.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      absurde.
    assert (Per A B Q).
      eapply per_col.
        apply H8.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      unfold Col.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      left.
      apply midpoint_bet.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Per P A X).
      eapply per_col.
(* Goal: False *)
        apply H.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (B <> Q).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      subst Q.
      apply l7_3 in H7.
      subst R.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      absurde.
    assert (Per R B X).
      eapply per_col.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
        intro.
(* Goal: False *)
        apply H.
        apply sym_equal.
        apply H12.
(* Goal: @Per Tn U X C *)
        apply l8_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Col Tn C B D *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      apply col_permutation_4.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (X <> A).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
(* Goal: False *)
      subst X.
      assert (~Col P A R).
        eapply per_not_colp.
(* Goal: False *)
          apply H.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply H13.
      unfold Col.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      left.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    double P A P'.
    prolong P' X R' X R.
    assert (exists M, Midpoint M R R').
      eapply l7_25.
      apply cong_symmetry.
      apply H16.
    ex_elim H17 M.
    assert (Per X M R).
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @Per Tn A' B C) (_ : @Bet Tn A C A'), @eq (@Tpoint Tn) B C *)
      unfold Per.
      exists R'.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
      split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply cong_symmetry.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Cong X P X P').
      apply l8_2 in H10.
      unfold Per in H10.
      ex_and H10 P''.
      assert (P'=P'').
        eapply symmetric_point_uniqueness.
          apply H14.
        apply H10.
      subst P''.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (X <> P').
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      subst P'.
      apply cong_identity in H19.
(* Goal: False *)
      subst X.
      apply l7_3 in H14.
      subst P.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      absurde.
    assert (P <> P').
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      subst P'.
      eapply l7_3 in H14.
      subst P.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      absurde.
    assert(~Col X P P').
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      assert(Col X P A).
        eapply col3.
          apply H21.
          apply col_permutation_1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
          apply col_trivial_3.
        unfold Col.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
        right;left.
        apply between_symmetry.
        apply midpoint_bet.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply col_permutation_1 in H23.
      assert (P = A \/ X = A).
        eapply l8_9.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      induction H24.
        subst P.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
        absurde.
      apply H13.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Bet A X M).
      eapply l7_22.
        5:apply H14.
        5:apply H18.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply cong_symmetry.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (X <> R).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
(* Goal: @Col Tn A B C *)
      treat_equalities.
      apply l8_8 in H12.
(* Goal: @Col Tn A B C *)
      treat_equalities.
(* Goal: @Col Tn M A B *)
(* Goal: @Perp_at Tn M X M A B *)
      unfold Midpoint in *.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: @Col Tn A B C *)
      treat_equalities.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
      intuition.
    assert (X <> R').
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      subst R'.
      apply cong_symmetry in H16.
      apply cong_identity in H16.
      apply H24.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (M <> X).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      subst M.
      apply H22.
      eapply col_transitivity_1.
        apply H24.
        unfold Col.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
        right; right.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      eapply col_transitivity_1.
        apply H25.
        unfold Col.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
        right;right.
        apply midpoint_bet.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      unfold Col.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
      right; right.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (M = B).
      eapply (l8_18_uniqueness A X R).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
        intro.
        assert (Col A B R).
          eapply col_transitivity_1.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
            intro.
            apply H13.
            apply sym_equal.
            apply H28.
            apply col_permutation_5.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
            assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: not (@Col Tn B A P) *)
        eapply per_not_col.
          apply H; apply H12.
          apply H8.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        unfold Col.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
        left.
        assumption; eapply col_transitivity_1.
        apply per_perp in H17.
(* Goal: @Perp Tn O P A B *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp Tn O X A B) *)
          apply perp_comm.
          eapply perp_col.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
            assumption.
            apply H17.
          unfold Col.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
          right;right.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
          auto.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
        intro.
        subst M.
        apply (symmetric_point_uniqueness R R R R')  in H18.
          subst R'.
          apply H22.
          eapply col_transitivity_1.
            apply H25.
            unfold Col.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
            right;right.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
            assumption.
          unfold Col.
(* Goal: or (@eq (@Tpoint Tn) B B') (not (@Col Tn B' C D)) *)
          right; right.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Midpoint Tn A A A *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
        eapply l7_3_2.
        apply col_permutation_5.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply per_perp in H10.
(* Goal: @Perp Tn O P A B *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp Tn O X A B) *)
        apply perp_comm.
        eapply perp_col.
          apply H13.
(* Goal: @Perp Tn O P A B *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp Tn O X A B) *)
          apply perp_comm.
          eapply perp_col.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
            intro.
            apply H13.
            apply sym_equal.
            apply H27.
(* Goal: @Perp Tn A B C B *)
(* Goal: @Col Tn C B D *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
            apply perp_right_comm.
            apply per_perp in H2.
(* Goal: @Perp Tn A B O X *)
              apply H2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
              assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
            assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
        apply col_trivial_2.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
        auto.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      apply H13.
(* Goal: False *)
      subst X.
      reflexivity.
    subst M.
    assert(OFSC P X R P' P' X R' P).
      unfold OFSC.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
      repeat split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        apply cong_commutativity.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        apply cong_symmetry.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        apply cong_pseudo_reflexivity.
      apply cong_symmetry.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (Cong R P' R' P).
      eapply five_segment_with_def.
        apply H27.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
(* Goal: False *)
      subst X.
      apply H22.
      apply col_trivial_1.
    assert (IFSC P' A P R R' B R P).
      unfold IFSC.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
      repeat split.
        apply between_symmetry.
        apply midpoint_bet.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        apply between_symmetry.
        apply midpoint_bet.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        eapply l2_11.
          apply between_symmetry.
          apply midpoint_bet.
          apply H14.
          apply between_symmetry.
          apply midpoint_bet.
          apply H18.
          eapply cong_transitivity.
            apply midpoint_cong.
(* Goal: @Midpoint Tn B C' C *)
(* Goal: @Cong Tn A C' A C *)
            apply l7_2.
            apply H14.
          eapply cong_transitivity.
            apply H3.
          apply cong_commutativity.
          apply midpoint_cong.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Cong Tn X A X B *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
        Cong.
      apply cong_pseudo_reflexivity.
    eapply cong_right_commutativity.
    eapply l4_2.
    eapply H29.
Qed.


Lemma perp_cong : forall A B P R X,
 A <> B -> A <> P ->
 Perp A B P A -> Perp A B R B ->
 Cong A P B R -> Col A B X -> Bet P X R ->
 Cong A R P B.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Cong Tn A R P B *)
    apply (per_cong A B P R X).
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Per Tn B A P *)
(* Goal: @Per Tn A B R *)
(* Goal: @Cong Tn A P B R *)
(* Goal: @Col Tn A B X *)
(* Goal: @Bet Tn P X R *)
      apply perp_per_1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Per Tn B A P *)
(* Goal: @Per Tn A B R *)
(* Goal: @Cong Tn A P B R *)
(* Goal: @Col Tn A B X *)
(* Goal: @Bet Tn P X R *)
      eapply perp_per_1.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
        auto.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
      apply perp_left_comm;auto.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma perp_exists : forall O A B, A <> B -> exists X, Perp O X A B.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp Tn O X A B) *)
    induction(col_dec A B O).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp Tn O X A B) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp Tn O X A B) *)
      destruct (diff_col_ex3 A B O H0) as [C].
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp Tn O X A B) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp Tn O X A B) *)
      destruct (l8_21 O C O H3) as [P [T]].
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
      exists P.
(* Goal: @Perp Tn O P A B *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp Tn O X A B) *)
      apply perp_comm.
(* Goal: @Perp Tn A B C X *)
      apply perp_sym.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
      apply (perp_col2 O C); ColR.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp Tn O X A B) *)
    destruct (l8_18_existence A B O H0) as [X []].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
    exists X.
(* Goal: @Perp Tn A B C X *)
    apply perp_sym.
(* Goal: @Perp Tn A B O X *)
    apply H2.
Qed.

Lemma perp_vector : forall A B, A <> B -> (exists X, exists Y, Perp A B X Y).
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A A) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
    exists A.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
    destruct (perp_exists A A B) as [Y]; auto.
(* Goal: @Perp Tn A B B P *)
    exists Y; Perp.
Qed.

Lemma midpoint_existence_aux : forall A B P Q T,
  A<>B -> Perp A B Q B -> Perp A B P A ->
  Col A B T -> Bet Q T P -> Le A P B Q ->
  exists X : Tpoint, Midpoint X A B.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    unfold Le in H4.
    ex_and H4 R.
    assert (exists X, Bet T X B /\ Bet R X P).
      eapply inner_pasch.
        apply between_symmetry.
        apply H3.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
      auto.
    ex_and H6 X.
    assert (Col A B X).
      induction (eq_dec_points T B).
        subst T.
        apply between_identity in H6.
(* Goal: False *)
        subst X.
(* Goal: False *)
        Col.
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
     assert_cols;ColR.
     induction(col_dec A B P).
      assert (B=A \/ P=A).
        eapply l8_9.
(* Goal: @Per Tn B A P *)
(* Goal: @Per Tn A B R *)
(* Goal: @Cong Tn A P B R *)
(* Goal: @Col Tn A B X *)
(* Goal: @Bet Tn P X R *)
          apply perp_per_1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Col Tn C B D *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
        apply col_permutation_4.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      induction H10.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A A) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
        exists A.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
        subst B.
(* Goal: @Midpoint Tn A A A *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
        eapply l7_3_2.
(* Goal: @Col Tn A B C *)
      treat_equalities.
      apply perp_distinct in H1.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      absurde.
    assert (B <> R).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      subst R.
(* Goal: @Col Tn A B C *)
      treat_equalities.
      apply H9.
      apply col_trivial_3.
    assert (~Col A B Q).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      assert (A=B \/ Q=B).
        eapply l8_9.
          apply perp_per_2.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
            auto.
(* Goal: @Perp Tn O P A B *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp Tn O X A B) *)
          apply perp_comm.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      induction H12.
(* Goal: False *)
        apply H.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      subst Q.
(* Goal: @Col Tn A B C *)
      treat_equalities.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      absurde.
    assert (~Col A B R).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      assert (Col B A Q).
(* Goal: @Col Tn C B B' *)
(* Goal: False *)
        assert_cols;ColR.
(* Goal: False *)
      Col.
    show_distinct P R.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
      intuition.
    induction (eq_dec_points A P).
      subst P.
      apply perp_distinct in H1.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      absurde.
    assert (Perp A B R B).
      eapply perp_col.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Perp Tn A B C X *)
        apply perp_sym.
(* Goal: @Perp Tn B A D C *)
        apply perp_left_comm.
        eapply perp_col.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Perp Tn B A D C *)
          apply perp_left_comm.
(* Goal: @Perp Tn A B C X *)
          apply perp_sym.
(* Goal: False *)
          apply H0.
(* Goal: False *)
        assert_cols;Col.
(* Goal: False *)
      Col.
    apply between_symmetry in H7.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    assert (Cong A R P B).
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      apply (perp_cong A B P R X); assumption.
    assert (Midpoint X A B /\ Midpoint X P R).
      apply (l7_21 A P B R X);finish.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter. exists X.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

(** This following result is very important, it shows the existence of a midpoint.
 The proof is involved because we are not using continuity axioms.
*)

(** This corresponds to l8_22 in Tarski's book. *)

Lemma midpoint_existence : forall A B, exists X, Midpoint X A B.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
    induction (eq_dec_points A B).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
      subst B.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A A) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
      exists A.
(* Goal: @Midpoint Tn A A A *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
      apply l7_3_2.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
    cut(exists Q, Perp A B B Q).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
      ex_elim H0 Q.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
      cut(exists P, exists T, Perp A B P A /\ Col A B T /\ Bet Q T P).
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
        intros.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
        ex_elim H0 P.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn Q T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
        ex_and H2 T.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn Q T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
        assert (Le A P B Q \/ Le B Q A P) by (apply le_cases).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn Q T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
        induction H4.
(* Goal: @Perp Tn A B B P *)
          apply midpoint_existence_aux with P Q T;finish;Perp.
        assert (exists X : Tpoint, Midpoint X B A)
          by (apply (midpoint_existence_aux B A Q P T);finish;Perp;Between).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn Q T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
        ex_elim H5 X.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
        exists X.
(* Goal: @Midpoint Tn X A B *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn Q T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
        finish.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
       apply l8_21;assumption.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
    assert (exists P : Tpoint, (exists T : Tpoint, Perp B A P B /\ Col B A T /\ Bet A T P)) by (apply (l8_21 B A);auto).
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
    ex_elim H0 P.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
    ex_elim H1 T.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
    exists P.
(* Goal: @Perp Tn A B B P *)
    Perp.
Qed.


Lemma perp_in_id : forall A B C X, Perp_at X A B C A -> X = A.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @eq (@Tpoint Tn) X A *)
    assert (Perp A B C A).
(* Goal: @Perp Tn A B C D *)
      unfold Perp.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
      exists X.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @eq (@Tpoint Tn) X A *)
    assert (A <> B /\ C <> A).
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C A)) *)
(* Goal: @eq (@Tpoint Tn) X A *)
      apply perp_distinct.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: @eq (@Tpoint Tn) X A *)
    assert (HH:=H0).
(* Goal: @eq (@Tpoint Tn) X A *)
    apply perp_perp_in in HH.
(* Goal: @eq (@Tpoint Tn) X A *)
    assert (l8_16_1:=l8_16_1 A B C B A).
(* Goal: @eq (@Tpoint Tn) X A *)
    assert (~Col A B C /\ Per C A B).
(* Goal: False *)
      apply l8_16_1;Col.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: @eq (@Tpoint Tn) X A *)
    unfold Perp_at in H.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
(* Goal: @Midpoint Tn X A B *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn Q T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
    eapply l8_18_uniqueness with A B C;finish.
(* Goal: @Perp Tn A B C X *)
      apply perp_sym.
(* Goal: @Perp Tn C X A B *)
      eapply perp_col with A;finish.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
        intro.
(* Goal: False *)
        subst X.
(* Goal: False *)
        Col.
Qed.


Lemma l8_22 : forall A B P R X ,
 A <> B -> A <> P ->
 Per B A P -> Per A B R ->
 Cong A P B R -> Col A B X -> Bet P X R ->
 Cong A R P B /\ Midpoint X A B /\ Midpoint X P R.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    assert (Cong A R P B).
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      apply (per_cong A B P R X); assumption.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
    assert (~ Col B A P).
(* Goal: not (@Col Tn B A P) *)
      eapply per_not_col.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
        auto.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
    assert_all_diffs_by_contradiction.
(* Goal: @Midpoint Tn X A B *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn Q T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
    apply l7_21;finish.
Qed.

Lemma l8_22_bis : forall A B P R X,
 A <> B -> A <> P ->
 Perp A B P A -> Perp A B R B ->
 Cong A P B R -> Col A B X -> Bet P X R ->
 Cong A R P B /\ Midpoint X A B /\ Midpoint X P R.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Midpoint Tn X A B *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn Q T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
    apply l8_22;finish.
(* Goal: @Midpoint Tn X A B *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Perp Tn A B P A) (and (@Col Tn A B T) (@Bet Tn Q T P)))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Perp Tn A B B Q) *)
       apply perp_per_1;finish.
(* Goal: @Perp Tn A B B P *)
       apply perp_per_1;finish;Perp.
Qed.

Lemma perp_in_perp : forall A B C D X, Perp_at X A B C D -> Perp A B C D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Perp Tn A B C D *)
    unfold Perp.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
    exists X.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

End T8_4.

Hint Resolve perp_per_1 perp_per_2 perp_col perp_perp_in perp_in_perp : perp.

Section T8_5.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma perp_proj : forall A B C D, Perp A B C D -> ~Col A C D -> exists X, Col A B X /\ Perp A X C D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    unfold Perp in H.
(* Goal: @Col Tn A B A *)
(* Goal: @Perp Tn A B C A *)
    ex_and H X.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
    exists X.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    split.
(* Goal: @Col Tn X C D *)
      unfold Perp_at in H1.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
      apply col_permutation_1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    eapply perp_col.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
(* Goal: False *)
      subst X.
(* Goal: @Col Tn X C D *)
      unfold Perp_at in H1.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: False *)
      apply H0.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
      apply perp_in_perp in H1.
      apply H1.
(* Goal: @Col Tn X C D *)
    unfold Perp_at in H1.
(* Goal: @eq (@Tpoint Tn) X A *)
    spliter.
    apply col_permutation_1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma l8_24 : forall A B P Q R T,
 Perp P A A B ->
 Perp Q B A B ->
 Col A B T ->
 Bet P T Q ->
 Bet B R Q ->
 Cong A P B R ->
 exists X, Midpoint X A B /\ Midpoint X P R.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    unfold Le in H4.
    assert (exists X, Bet T X B /\ Bet R X P).
      eapply inner_pasch.
(* Goal: @Perp Tn A B O X *)
        apply H2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    ex_and H5 X.
    assert (Col A B X).
      induction (eq_dec_points T B).
        subst T.
        apply between_identity in H5.
(* Goal: False *)
        subst X.
        apply col_trivial_2.
      assert (Col T X B).
        unfold Col.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
        left.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Col Tn C B D *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      apply col_permutation_4.
      eapply col_transitivity_1.
(* Goal: not (@eq (@Tpoint Tn) C X) *)
        intro.
        apply H7.
        apply sym_equal.
        apply H9.
        apply col_permutation_1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply col_permutation_2.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (A <> B).
(* Goal: not (@Col Tn B A P) *)
      apply perp_distinct in H.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (A <> P).
(* Goal: not (@Col Tn B A P) *)
      apply perp_distinct in H.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
      auto.
    induction(col_dec A B P).
      assert (B=A \/ P=A).
        eapply l8_9.
(* Goal: @Per Tn B A P *)
(* Goal: @Per Tn A B R *)
(* Goal: @Cong Tn A P B R *)
(* Goal: @Col Tn A B X *)
(* Goal: @Bet Tn P X R *)
          apply perp_per_1.
(* Goal: @Perp Tn A B C X *)
          apply perp_sym.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Col Tn C B D *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
        apply col_permutation_4.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      induction H11.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A A) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
        exists A.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Midpoint Tn X A B) *)
        subst B.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
        absurde.
      subst P.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      absurde.
    assert (B <> R).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      subst R.
      apply cong_identity in H4.
      subst P.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      absurde.
    assert (Q <> B).
      apply perp_distinct in H0.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (~Col A B Q).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      assert (A=B \/ Q=B).
        eapply l8_9.
          apply perp_per_2.
(* Goal: not (@eq (@Tpoint Tn) B A) *)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: @Per Tn B A P *)
(* Goal: and (@Midpoint Tn X A B) (@Midpoint Tn X P R) *)
            auto.
(* Goal: @Perp Tn O P A B *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp Tn O X A B) *)
          apply perp_comm.
(* Goal: @Perp Tn A B C X *)
          apply perp_sym.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      induction H14.
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
        contradiction.
      subst Q.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      absurde.
    assert (~Col A B R).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      assert (Col B A Q).
        eapply col_transitivity_1.
          apply H11.
          apply col_permutation_1.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
        unfold Col.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
        left.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply H13.
(* Goal: @Col Tn C B D *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      apply col_permutation_4.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
    assert (P <> R).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
      intro.
      subst R.
      apply between_identity in H6.
(* Goal: False *)
      subst X.
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: @eq (@Tpoint Tn) X M *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      contradiction.
    induction (eq_dec_points A P).
      subst P.
(* Goal: not (@Col Tn B A P) *)
      apply perp_distinct in H.
(* Goal: @eq (@Tpoint Tn) X A *)
      spliter.
(* Goal: @Perp Tn C D A B *)
(* Goal: @Perp Tn C D A B *)
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) B C) *)
      absurde.
    assert (Perp A B R B).
      eapply perp_col.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Perp Tn A B C X *)
        apply perp_sym.
(* Goal: @Perp Tn B A D C *)
        apply perp_left_comm.
        eapply perp_col.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
          assumption.
(* Goal: @Perp Tn B A D C *)
          apply perp_left_comm.
(* Goal: False *)
          apply H0.
        unfold Col.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
        right; left.
        apply between_symmetry.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply col_trivial_2.
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    assert (Cong A R P B).
      apply (perp_cong A B P R X).
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Perp Tn A B C X *)
        apply perp_sym.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      apply between_symmetry.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
    assert (Midpoint X A B /\ Midpoint X P R).
      apply (l7_21 A P B R X).
(* Goal: not (@eq (@Tpoint Tn) C X) *)
        intro.
        apply H10.
        apply col_permutation_5.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        apply cong_right_commutativity.
        apply cong_symmetry.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
        apply col_permutation_5.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
        assumption.
      unfold Col.
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
(* Goal: or (@eq (@Tpoint Tn) X M) (and (not (@Col Tn A B X)) (@Perp_at Tn M X M A B)) *)
      left.
      apply between_symmetry.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Perp_at Tn X A B C D) *)
    exists X.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    assumption.
Qed.

Lemma col_per2__per : forall A B C P X, A <> B -> Col A B C -> Per A X P -> Per B X P -> Per C X P.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
    intros.
(* Goal: @Per Tn C X P *)
    destruct (symmetric_point_construction P X) as [Q].
(* Goal: and (@Cong Tn A R P B) (and (@Midpoint Tn X A B) (@Midpoint Tn X P R)) *)
    exists Q; split.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
      assumption.
(* Goal: @Midpoint Tn X P Q *)
(* Goal: @Cong Tn C P C Q *)
    apply (l4_17 A B); try apply per_double_cong with X; assumption.
Qed.

Lemma perp_in_per_1 :
 forall A B C D X,
  Perp_at X A B C D ->
  Per A X C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
intros.
(* Goal: @Per Tn B X D *)
unfold Perp_at in *.
(* Goal: @Per Tn B X D *)
decompose [and] H.
apply H5;
(* Goal: False *)
Col.
Qed.

Lemma perp_in_per_2 :
 forall A B C D X,
  Perp_at X A B C D ->
  Per A X D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
intros.
(* Goal: @Per Tn B X D *)
unfold Perp_at in *.
(* Goal: @Per Tn B X D *)
decompose [and] H.
apply H5;
(* Goal: False *)
Col.
Qed.

Lemma perp_in_per_3 :
 forall A B C D X,
  Perp_at X A B C D ->
  Per B X C.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
intros.
(* Goal: @Per Tn B X D *)
unfold Perp_at in *.
(* Goal: @Per Tn B X D *)
decompose [and] H.
apply H5;
(* Goal: False *)
Col.
Qed.

Lemma perp_in_per_4 :
 forall A B C D X,
  Perp_at X A B C D ->
  Per B X D.
Proof.
(* Goal: forall (A B C D X : @Tpoint Tn) (_ : @Perp_at Tn X A B C D), @Per Tn B X D *)
intros.
(* Goal: @Per Tn B X D *)
unfold Perp_at in *.
(* Goal: @Per Tn B X D *)
decompose [and] H.
apply H5;
(* Goal: False *)
Col.
Qed.

End T8_5.

Hint Resolve perp_in_per_1 perp_in_per_2 perp_in_per_3 perp_in_per_4 : perp.

Ltac midpoint M A B :=
 let T:= fresh in assert (T:= midpoint_existence A B);
 ex_and T M.

Tactic Notation "Name" ident(M) "the" "midpoint" "of" ident(A) "and" ident(B) :=
 midpoint M A B.
