Library GeoCoq.Tarski_dev.Ch08_orthogonality

Require Export GeoCoq.Tarski_dev.Ch07_midpoint.
Require Export GeoCoq.Tactics.Coinc.ColR.

Ltac not_exist_hyp_comm A B := not_exist_hyp (AB);not_exist_hyp (BA).

Ltac not_exist_hyp2 A B C D := first [not_exist_hyp_comm A B | not_exist_hyp_comm C D].

Ltac not_exist_hyp3 A B C D E F := first [not_exist_hyp_comm A B | not_exist_hyp_comm C D | not_exist_hyp_comm E F].

Ltac not_exist_hyp_perm_col 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 finish := match goal with
 | |- Col ?A ?B ?CCol
 | |- ¬ Col ?A ?B ?CCol
 | |- Cong ?A ?B ?C ?DCong
 | |- Midpoint ?A ?B ?CMidpoint
 | |- ?A?Bapply swap_diff;assumption
 | |- _try assumption
end.

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 (Col X1 X2 X3);assert (Col X1 X2 X3) by (apply bet_col;apply H)

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

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

Ltac assert_bet :=
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 :=
  repeat
  match goal with
   | H:(Midpoint ?A ?B ?C), H2 : Midpoint ?A ?C ?B |- _clear H2
   | H:(Midpoint ?A ?B ?C), H2 : Midpoint ?A ?B ?C |- _clear H2
   | H:(¬Col ?A ?B ?C), H2 : ¬Col ?A ?B ?C |- _clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?A ?C ?B |- _clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?A ?B ?C |- _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:(Bet ?A ?B ?C), H2 : Bet ?A ?B ?C |- _clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?D ?C |- _clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?C ?D |- _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
   | H:(?A?B), H2 : (?A?B) |- _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: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 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 := between_equality A B C H H2);
                       smart_subst A;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; 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
 end.

Ltac show_distinct' X Y :=
 assert (XY);
 [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.
Section T8_1.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Definition Per A B C := C', Midpoint B C C' Cong A C A C'.

Lemma Per_dec : A B C, Per A B C ¬ Per A B C.
Proof.
    intros.
    unfold Per.
    elim (symmetric_point_construction C B);intros C' HC'.
    elim (Cong_dec A C A C');intro.
      left.
       C'.
      intuition.
    right.
    intro.
    decompose [ex and] H0;clear H0.
    assert (C'=x) by (apply symmetric_point_uniqueness with C B;assumption).
    subst.
    intuition.
Qed.

Lemma l8_2 : A B C, Per A B C Per C B A.
Proof.
    unfold Per.
    intros.
    ex_and H C'.
    assert ( A', Midpoint B A A').
      apply symmetric_point_construction.
    ex_and H1 A'.
     A'.
    split.
      assumption.
    eapply cong_transitivity.
      apply cong_commutativity.
      apply H0.
    eapply l7_13.
      apply H.
    apply l7_2.
    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 :
  A B C,
 Per A B C Per C B A
 Per A B C.
Proof.
    intros.
    decompose [or] H;Perp.
Qed.

Lemma Per_perm :
  A B C,
 Per A B C
 Per A B C Per C B A.
Proof.
    intros.
    split; Perp.
Qed.

Lemma l8_3 : A B C A',
 Per A B C AB Col B A A' Per A' B C.
Proof.
    unfold Per.
    intros.
    ex_and H C'.
     C'.
    split.
      assumption.
    unfold Midpoint in *;spliter.
    eapply l4_17 with A B;finish.
Qed.

Lemma l8_4 : A B C C', Per A B C Midpoint B C C' Per A B C'.
Proof.
    unfold Per.
    intros.
    ex_and H B'.
     C.
    split.
      apply l7_2.
      assumption.
    assert (B' = C') by (eapply symmetric_point_uniqueness;eauto).
    subst B'.
    Cong.
Qed.

Lemma l8_5 : A B, Per A B B.
Proof.
    unfold Per.
    intros.
     B.
    split.
      apply l7_3_2.
    Cong.
Qed.

Lemma l8_6 : A B C A', Per A B C Per A' B C Bet A C A' B=C.
Proof.
    unfold Per.
    intros.
    ex_and H C'.
    ex_and H0 C''.
    assert (C'=C'') by (eapply symmetric_point_uniqueness;eauto).
    subst C''.
    assert (C = C') by (eapply l4_19;eauto).
    subst C'.
    apply l7_3.
    assumption.
Qed.

End T8_2.

Hint Resolve l8_5 : perp.

Ltac let_symmetric C P A :=
let id1:=fresh in (assert (id1:( 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 : A B C, Per A B C Per A C B B=C.
Proof.
    intros.
    unfold Per in H.
    ex_and H C'.
    symmetric A' C A.
    induction (eq_dec_points B C).
      assumption.
    assert (Per C' C A).
      eapply l8_3.
        eapply l8_2.
        apply H0.
        assumption.
      unfold Midpoint in H.
      spliter.
      unfold Col.
      left.
      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.
      Cong.
    unfold Midpoint in ×.
    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.
      assumption.
    assert (Per A' B C).
      unfold Per.
       C'.
      unfold Midpoint.
      repeat split;auto.
    eapply l8_6.
      apply H9.
      unfold Per.
       C'.
      split.
        unfold Midpoint;auto.
      apply H1.
    Between.
Qed.

Lemma l8_8 : A B, Per A B A A=B.
Proof.
    intros.
    apply l8_7 with A.
      apply l8_2.
      apply l8_5.
    assumption.
Qed.

Lemma l8_9 : A B C, Per A B C Col A B C A=B C=B.
Proof.
    intros.
    elim (eq_dec_points A B);intro.
      tauto.
    right.
    eapply l8_7.
      eapply l8_2.
      eapply l8_5.
    apply l8_3 with A; Col.
Qed.

Lemma l8_10 : A B C A' B' C', Per A B C Cong_3 A B C A' B' C' Per A' B' C'.
Proof.
    unfold Per.
    intros.
    ex_and H D.
    prolong C' B' D' B' C'.
     D'.
    split.
      unfold Midpoint.
      split.
        assumption.
      Cong.
    unfold Cong_3, Midpoint in ×.
    spliter.
    induction (eq_dec_points C B).
      treat_equalities;Cong.
    assert(OFSC C B D A C' B' D' A').
      unfold OFSC.
      repeat split.
        assumption.
        assumption.
        Cong.
        eapply cong_transitivity.
          apply cong_symmetry.
          apply H4.
        eapply cong_transitivity.
          apply cong_commutativity.
          apply H6.
        Cong.
        Cong.
      Cong.
    assert (Cong D A D' A').
      eapply five_segment_with_def.
        apply H8.
      assumption.
    eapply cong_transitivity.
      apply cong_symmetry.
      apply H5.
    eapply cong_transitivity.
      apply H1.
    Cong.
Qed.

Definition Perp_at X A B C D :=
  A B C D Col X A B Col X C D
  ( U V, Col U A B Col V C D Per U X V).

Lemma col_col_per_per : A X C U V,
 AX CX
 Col U A X
 Col V C X
 Per A X C
 Per U X V.
Proof.
    intros.
    assert (Per U X C) by (apply (l8_3 A X C U);Col).
    apply l8_2 in H4.
    apply l8_2 .
    apply (l8_3 C X U V);Col.
Qed.

Lemma Perp_in_dec : X A B C D, Perp_at X A B C D ¬ Perp_at X A B C D.
Proof.
    intros.
    unfold Perp_at.
    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.
    elim (eq_dec_points B X);intro; elim (eq_dec_points D X);intro;subst;treat_equalities.
      elim (Per_dec A X C);intro.
        left;repeat split;Col;intros; apply col_col_per_per with A C;Col.
      right;intro;spliter;apply H3;apply H8;Col.
      elim (Per_dec A X D);intro.
        left;repeat split;Col;intros; apply col_col_per_per with A D;Col;ColR.
      right;intro;spliter;apply H3;apply H9;Col.
      elim (Per_dec B X C);intro.
        left;repeat split;Col;intros; apply col_col_per_per with B C;Col;ColR.
      right;intro;spliter;apply H4;apply H9;Col.
    elim (Per_dec B X D);intro.
      left;repeat split;Col;intros; apply col_col_per_per with B D;Col;ColR.
    right;intro;spliter;apply H5;apply H10;Col.
Qed.

Definition Perp A B C D := X, Perp_at X A B C D.

Lemma perp_distinct : A B C D, Perp A B C D A B C D.
Proof.
    intros.
    unfold Perp in H.
    ex_elim H X.
    unfold Perp_at in H0.
    tauto.
Qed.

Lemma l8_12 : A B C D X, Perp_at X A B C D Perp_at X C D A B.
Proof.
    unfold Perp_at.
    intros.
    spliter.
    repeat split;try assumption.
    intros;eapply l8_2;eauto.
Qed.

Lemma per_col : A B C D,
 B C Per A B C Col B C D Per A B D.
Proof.
    unfold Per.
    intros.
    ex_and H0 C'.
    prolong D B D' D B.
     D'.
    assert (Midpoint B C C').
      apply H0.
    induction H5.
    assert (Midpoint B D D') by (unfold Midpoint;split;Cong).
    assert (Midpoint B D D').
      apply H7.
    induction H8.
    repeat split.
      assumption.
      Cong.
    unfold Col in H1.
    induction H1.
      assert (Bet B C' D').
        eapply l7_15.
          eapply l7_3_2.
          apply H0.
          apply H7.
        assumption.
      assert (Cong C D C' D').
        eapply l4_3_1.
          apply H1.
          apply H10.
          Cong.
        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.
          apply H0.
          apply H7.
          apply l7_3_2.
        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.
        eapply l7_3_2.
        apply H0.
      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 : A B C D X,
   A B C D Col X A B Col X C D
  ( U, V :Tpoint, Col U A B Col V C D UX VX Per U X V)
  Perp_at X A B C D.
Proof.
    intros.
    ex_and H3 U.
    ex_and H4 V.
    unfold Perp_at.
    repeat split;try assumption.
    intros.
    assert (Per V X U0).
      eapply l8_2.
      eapply l8_3.
        apply H7.
        assumption.
      eapply col3.
        apply H.
        Col.
        Col.
      Col.
    eapply per_col.
      2:eapply l8_2.
      2:apply H10.
      auto.
    eapply col3.
      apply H0.
      Col.
      Col.
    Col.
Qed.

Definition DistLn := fun A B C D
( X, Col X A B ¬Col X C D) ( X, ¬ Col X A B Col X C D).

Lemma perBAB : A B, Per B A B A = B.
Proof.
    intros.
    eapply l8_7.
      apply H.
    eapply l8_2.
    apply l8_5.
Qed.

Lemma l8_14_1 : A B, ¬ Perp A B A B.
Proof.
    intros.
    unfold Perp.
    intro.
    ex_and H X.
    unfold Perp_at in H0.
    spliter.
    assert (Per A X A).
      apply H3.
        Col.
      Col.
    assert (A = X).
      eapply l8_7.
        2: apply H4.
      apply l8_2.
      apply l8_5.
    assert (Per B X B) by (apply H3;Col).
    assert (B = X).
      eapply l8_7 with B.
        2: apply H6.
      apply l8_2.
      apply l8_5.
    apply H0.
    congruence.
Qed.

Lemma l8_14_2_1a : X A B C D, Perp_at X A B C D Perp A B C D.
Proof.
    intros.
    unfold Perp.
     X.
    assumption.
Qed.

Lemma perp_in_distinct : X A B C D , Perp_at X A B C D A B C D.
Proof.
    intros.
    apply l8_14_2_1a in H.
    apply perp_distinct.
    assumption.
Qed.

Lemma l8_14_2_1b : X A B C D Y, Perp_at X A B C D Col Y A B Col Y C D X=Y.
Proof.
    intros.
    unfold Perp_at in H.
    spliter.
    eapply (H5 Y Y) in H1.
      2:assumption.
    apply perBAB.
    assumption.
Qed.

Lemma l8_14_2_1b_bis : 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.
    intros.
    unfold Perp in H.
    ex_and H Y.
    assert (Y = X) by (eapply (l8_14_2_1b Y _ _ _ _ X) in H2;assumption).
    subst Y.
    assumption.
Qed.

Lemma l8_14_2_2 : X A B C D,
 Perp A B C D ( Y, Col Y A B Col Y C D X=Y) Perp_at X A B C D.
Proof.
    intros.
    eapply l8_14_2_1b_bis.
      assumption.
      unfold Perp in H.
      ex_and H Y.
      unfold Perp_at in H1.
      spliter.
      assert (Col Y C D) by assumption.
      apply (H0 Y H2) in H3.
      subst Y.
      assumption.
    unfold Perp in H.
    ex_and H Y.
    unfold Perp_at in H1.
    spliter.
    assert (Col Y C D).
      assumption.
    apply (H0 Y H2) in H3.
    subst Y.
    assumption.
Qed.

Lemma l8_14_3 : A B C D X Y, Perp_at X A B C D Perp_at Y A B C D X=Y.
Proof.
    intros.
    eapply l8_14_2_1b.
      apply H.
      unfold Perp_at in H0.
      intuition.
    eapply l8_12 in H0.
    unfold Perp_at in H0.
    intuition.
Qed.

Lemma l8_15_1 : A B C X, AB Col A B X Perp A B C X Perp_at X A B C X.
Proof.
    intros.
    eapply l8_14_2_1b_bis;Col.
Qed.

Lemma l8_15_2 : A B C X, AB Col A B X Perp_at X A B C X Perp A B C X.
Proof.
    intros.
    eapply l8_14_2_1a.
    apply H1.
Qed.

Lemma perp_in_per : A B C, Perp_at B A B B C Per A B C.
Proof.
    intros.
    unfold Perp_at in H.
    spliter.
    apply H3;Col.
Qed.

Lemma perp_sym : A B C D, Perp A B C D Perp C D A B.
Proof.
    unfold Perp.
    intros.
    ex_and H X.
     X.
    apply l8_12.
    assumption.
Qed.

Lemma perp_col0 : 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.
    unfold Perp.
    intros.
    ex_and H X0.
     X0.
    unfold Perp_at in ×.
    spliter.
    repeat split.
      assumption.
      assumption.
      assumption.
      eapply col3.
        apply H.
        Col.
        assumption.
      assumption.
    intros.
    eapply l8_2.
    apply H6.
      2:assumption.
    assert(Col A X Y).
      eapply col3 with A B;Col.
    assert (Col B X Y).
      eapply col3 with A B;Col.
    eapply col3 with X Y;Col.
Qed.

Lemma l8_16_1 : A B C U X,
  AB Col A B X Col A B U UX Perp A B C X ¬ Col A B C Per C X U.
Proof.
    intros.
    split.
      intro.
      assert (Perp_at X A B C X).
        eapply l8_15_1.
          assumption.
          assumption.
        assumption.
      assert (X = U).
        eapply l8_14_2_1b.
          apply H5.
          Col.
        eapply col3 with A B;Col.
      intuition.
    apply l8_14_2_1b_bis with C X U X;try Col.
    assert (Col A X U).
      eapply (col3 A B);Col.
    eapply perp_col0 with A B;Col.
Qed.

Lemma per_perp_in : A B C, A B B C Per A B C Perp_at B A B B C.
Proof.
    intros.
    unfold Perp.
    repeat split.
      assumption.
      assumption.
      Col.
      Col.
    intros.
    eapply per_col.
      apply H0.
      eapply l8_2.
      eapply per_col.
        intro.
        apply H.
        apply sym_equal.
        apply H4.
        apply l8_2.
        assumption.
      Col.
    Col.
Qed.

Lemma per_perp : A B C, A B B C Per A B C Perp A B B C.
Proof.
    intros.
    apply per_perp_in in H1.
      eapply l8_14_2_1a with B;assumption.
      assumption.
    assumption.
Qed.

Lemma perp_left_comm : A B C D, Perp A B C D Perp B A C D.
Proof.
    unfold Perp.
    intros.
    ex_and H X.
     X.
    unfold Perp_at in ×.
    intuition.
Qed.

Lemma perp_right_comm : A B C D, Perp A B C D Perp A B D C.
Proof.
    unfold Perp.
    intros.
    ex_and H X.
     X.
    unfold Perp_at in ×.
    intuition.
Qed.

Lemma perp_comm : A B C D, Perp A B C D Perp B A D C.
Proof.
    intros.
    apply perp_left_comm.
    apply perp_right_comm.
    assumption.
Qed.

Lemma perp_in_sym :
  A B C D X,
  Perp_at X A B C D Perp_at X C D A B.
Proof.
    unfold Perp_at.
    intros.
    spliter.
    repeat split.
      assumption.
      assumption.
      assumption.
      assumption.
    intros.
    apply l8_2.
    apply H3;assumption.
Qed.

Lemma perp_in_left_comm :
  A B C D X,
  Perp_at X A B C D Perp_at X B A C D.
Proof.
    unfold Perp_at.
    intuition.
Qed.

Lemma perp_in_right_comm : A B C D X, Perp_at X A B C D Perp_at X A B D C.
Proof.
    intros.
    apply perp_in_sym.
    apply perp_in_left_comm.
    apply perp_in_sym.
    assumption.
Qed.

Lemma perp_in_comm : A B C D X, Perp_at X A B C D Perp_at X B A D C.
Proof.
    intros.
    apply perp_in_left_comm.
    apply perp_in_right_comm.
    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 :
   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.
    intros.
    decompose [or] H; Perp.
Qed.

Lemma Perp_perm :
   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.
    intros.
    repeat split; Perp.
Qed.

Lemma Perp_in_cases :
   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.
    intros.
    decompose [or] H; Perp.
Qed.

Lemma Perp_in_perm :
   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.
    intros.
    do 7 (split; Perp).
Qed.

Lemma l8_16_2 : A B C U X,
  AB Col A B X Col A B U UX ¬ Col A B C Per C X U Perp A B C X.
Proof.
    intros.
    assert (C X).
      intro.
      subst X.
      apply H3.
      assumption.
    unfold Perp.
     X.
    eapply l8_13_2.
      assumption.
      assumption.
      Col.
      Col.
     U.
     C.
    repeat split; Col.
    apply l8_2.
    assumption.
Qed.

Lemma l8_18_uniqueness : 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.
    intros.
    show_distinct A B.
      solve [intuition].
    assert (Perp_at X A B C X) by (eapply l8_15_1;assumption).
    assert (Perp_at Y A B C Y) by (eapply l8_15_1;assumption).
    unfold Perp_at in ×.
    spliter.
    apply l8_7 with C;apply l8_2;[apply H14 |apply H10];Col.
Qed.

Lemma distinct : A B X C C', ¬ Col A B C Col A B X Midpoint X C C' C C'.
Proof.
    intros.
    intro.
    subst C'.
    apply H.
    unfold Midpoint in H1.
    spliter.
    treat_equalities.
    assumption.
Qed.

Lemma l8_20_1 : 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.
    intros.
    double B A B'.
    double D A D'.
    double P A P'.
    induction (eq_dec_points A B).
      subst B.
      unfold Midpoint in H5.
      spliter.
      eapply l8_2.
      eapply l8_5.
    assert (Per B' B C).
      eapply l8_3.
        apply H.
        assumption.
      unfold Col.
      left.
      apply midpoint_bet.
      assumption.
    assert (Per B B' C').
      eapply l8_10.
        apply H7.
      unfold Cong_3.
      repeat split.
        apply cong_pseudo_reflexivity.
        eapply l7_13.
          unfold Midpoint.
          split.
            apply H3.
          apply midpoint_cong.
          assumption.
        assumption.
      eapply l7_13.
        apply l7_2.
        apply H3.
      assumption.
    assert(Midpoint B' D' C').
      eapply symmetry_preserves_midpoint.
        apply H4.
        apply H3.
        apply l7_2.
        apply H1.
      assumption.
    assert(Midpoint P' C D').
      eapply symmetry_preserves_midpoint.
        apply H1.
        apply H5.
        apply H4.
      assumption.
    unfold Per.
     P'.
    split.
      assumption.
    unfold Per in H7.
    ex_and H7 D''.
    assert (D''= D).
      eapply symmetric_point_uniqueness.
        apply H7.
      apply l7_2.
      assumption.
    subst D''.
    unfold Per in H8.
    ex_and H8 D''.
    assert (D' = D'').
      eapply symmetric_point_uniqueness.
        apply l7_2.
        apply H9.
      assumption.
    subst D''.
    assert (Midpoint P C' D).
      eapply symmetry_preserves_midpoint.
        apply l7_2.
        apply H1.
        apply l7_2.
        apply H5.
        apply l7_2.
        apply H4.
      assumption.
    assert (Cong C D C' D').
      eapply l7_13.
        apply H1.
      apply l7_2.
      assumption.
    assert (Cong C' D C D').
      eapply l7_13.
        apply l7_2.
        apply H1.
      apply l7_2.
      assumption.
    assert(Cong P D P' D').
      eapply l7_13.
        apply l7_2.
        apply H5.
      apply l7_2.
      assumption.
    assert (Cong P D P' C).
      eapply cong_transitivity.
        apply H16.
      unfold Midpoint in H10.
      spliter.
      apply cong_right_commutativity.
      apply cong_symmetry.
      assumption.
    assert (IFSC C' P D B D' P' C B).
      unfold IFSC.
      repeat split.
        apply midpoint_bet.
        assumption.
        apply midpoint_bet.
        apply l7_2.
        assumption.
        apply cong_right_commutativity.
        assumption.
        assumption.
        apply cong_commutativity.
        assumption.
      apply cong_right_commutativity.
      apply midpoint_cong.
      assumption.
    assert (Cong P B P' B).
      eapply l4_2.
      apply H18.
    apply cong_commutativity.
    assumption.
Qed.

Lemma l8_20_2 : A B C C' D P,
  Per A B C Midpoint P C' D Midpoint A C' C Midpoint B D C BC AP.
Proof.
    intros.
    intro.
    subst P.
    assert (C = D).
      eapply symmetric_point_uniqueness.
        apply H1.
      assumption.
    subst D.
    assert (B = C).
      apply l7_3.
      assumption.
    subst C.
    absurde.
Qed.

Lemma perp_col1 : A B C D X,
 C X Perp A B C D Col C D X Perp A B C X.
Proof.
    intros.
    assert (T:=perp_distinct A B C D H0).
    spliter.
    unfold Perp in ×.
    ex_and H0 P.
     P.
    unfold Perp_at in ×.
    spliter.
    repeat split.
      assumption.
      assumption.
      assumption.
      apply col_permutation_2.
      eapply col_transitivity_2.
        intro.
        apply H3.
        apply sym_equal.
        apply H8.
        apply col_permutation_4.
        assumption.
      apply col_permutation_3.
      assumption.
    intros.
    apply H7.
      assumption.
    apply col_permutation_2.
    eapply col_transitivity_1.
      apply H.
      apply col_permutation_5.
      assumption.
    apply col_permutation_1.
    assumption.
Qed.

Lemma l8_18_existence : A B C, ¬ Col A B C X, Col A B X Perp A B C X.
Proof.
    intros.
    prolong B A Y A C.
    assert ( P, Midpoint P C Y) by (apply l7_25 with A;Cong).
    ex_and H2 P.
    assert (Per A P Y) by (unfold Per; 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 ( 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.
      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.
    show_distinct P Y.
      unfold Midpoint in ×.
      spliter.
      treat_equalities.
      assert_cols.
      Col5.
    unfold Per in H19.
    ex_and H19 Q''.
    assert (Q' = Q'').
      eapply symmetric_point_uniqueness.
        apply H10.
      assumption.
    subst Q''.
    assert (hy:Bet Z Y X).
      apply (l7_22 Q C Q' C' Y Z X);Cong.
      assert (T:=outer_transitivity_between2 C P Y Q).
      assert_bet.
      apply between_symmetry.
      apply T;Between.
    show_distinct Q Y.
      intuition.
    assert (Per Y X C) by (unfold Per; C';split;Cong).
    assert_diffs.
    assert (Col P Y Q).
      unfold Col.
      left.
      assumption.
    assert(Col P Y C).
      unfold Midpoint in H3.
      spliter.
      unfold Col.
      right; right.
      assumption.
    assert (Col P Q C) by ColR.
    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).
    assert (Col A B Z) by ColR.
    assert (Col Y B Z) by ColR.
    assert (Col Q Y P) by Col.
    assert(Q C).
      intro.
      subst Q.
      unfold Midpoint in ×.
      spliter.
      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.
        assumption.
      treat_equalities.
      intuition.
    assert (Col Y B Z) by ColR.
    show_distinct Y Q'. intuition.
    assert (Col Y Q' C') by (assert_cols;Col).
    assert (Q Q').
      intro.
      unfold OFSC, Cong_3 in ×.
      spliter.
      treat_equalities.
      apply H.
      ColR.
    assert (C C').
      intro.
      subst C'.
      apply l7_3 in H14.
      subst X.
      assert (Col Z Q Q') by (assert_cols;ColR).
      assert (Y Z).
        intro.
        subst Z.
        unfold OFSC, Cong_3, Midpoint in ×.
        spliter.
        treat_equalities.
        intuition.
      apply H.
      ColR.
    assert(OFSC Q Y C Z Q' Y C' Z).
      unfold OFSC.
      repeat split;Between;Cong.
      unfold OFSC, Midpoint in ×.
      spliter.
      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).
    show_distinct Y Z. intuition.
    assert(C X).
      intro.
      subst X.
      unfold OFSC,Cong_3,Midpoint in ×.
      spliter.
      treat_equalities.
      intuition.
    assert(X Y).
      intro.
      subst X.
      unfold OFSC,Cong_3,Midpoint in ×.
      spliter.
      clean_duplicated_hyps.
      clean_trivial_hyps.
      show_distinct C' Y.
        intuition.
      assert (Col Y C' P ).
        eapply col_transitivity_1 with C.
          intuition.
          unfold Col.
          right;right.
          apply between_symmetry.
          assumption.
        apply col_permutation_1.
        assumption.
      show_distinct P Q.
        intuition.
      assert (Col Y P Q') by ColR.
      assert (Col Y Q Q') by ColR.
      assert (Col Q Y Z) by (assert_cols;ColR).
      assert (Col Y Z C) by (assert_bet;assert_cols;ColR).
      apply H.
      ColR.
    assert (Perp_at X Y Z C X).
      eapply l8_13_2;Col.
       Y.
       C.
      repeat split;Col.
    assert (Col A B X) by ColR.
     X.
    split.
      assumption.
    unfold Perp.
     X.
    unfold Perp_at.
    repeat split;Col.
    intros.
    unfold Perp_at in H52.
    spliter.
    apply H57;ColR.
Qed.

Lemma l8_21_aux : A B C,
 A B ¬ Col A B C P, T, Perp A B P A Col A B T Bet C T P.
Proof.
    intros.
    assert ( X : Tpoint, Col A B X Perp A B C X).
      eapply l8_18_existence.
      assumption.
    ex_and H1 X.
    assert (Perp_at X A B C X).
      eapply l8_15_1; assumption.
    assert (Per A X C).
      unfold Perp_at in H3.
      spliter.
      apply H7.
        apply col_trivial_1.
      apply col_trivial_1.
    assert(HH:= H4).
    unfold Per in H4.
    ex_and H4 C'.
    double C A C''.
    assert ( P, Midpoint P C' C'').
      eapply l7_25.
      unfold Midpoint in ×.
      spliter.
      eapply cong_transitivity.
        apply cong_symmetry.
        apply H5.
      apply cong_left_commutativity.
      assumption; spliter.
    ex_elim H7 P.
    assert (Per X A P).
      eapply l8_20_1.
        apply HH.
        apply l7_2.
        apply H8.
        apply l7_2.
        apply H6.
      apply l7_2.
      assumption.
    assert (X C).
      intro.
      subst C.
      apply H0.
      assumption.
    assert (A P).
      eapply l8_20_2.
        apply HH.
        apply l7_2.
        apply H8.
        apply l7_2.
        assumption.
        apply l7_2.
        assumption.
      assumption.
    assert ( T, Bet P T C Bet A T X).
      eapply l3_17.
        apply midpoint_bet.
        apply l7_2.
        apply H6.
        apply midpoint_bet.
        apply l7_2.
        apply H4.
      apply midpoint_bet.
      apply l7_2.
      apply H8.
    ex_and H11 T.
    induction (eq_dec_points A X).
      subst X.
       P.
       T.
      apply between_identity in H12.
      subst T.
      assert (C'= C'').
        eapply symmetric_point_uniqueness.
          apply H4.
        assumption.
      subst C''.
      apply l7_3 in H8.
      subst P.
      assert (Col A C C') by (assert_cols;ColR).
      repeat split;Col;Between.
      apply perp_col0 with C A;auto using perp_sym;assert_cols;Col.
     P.
     T.
    repeat split.
      unfold Perp.
       A.
      unfold Perp_at.
      repeat split.
        assumption.
        auto.
        apply col_trivial_1.
        apply col_trivial_3.
      unfold Perp_at in H3.
      spliter.
      intros.
      eapply per_col in H7.
        apply l8_2 in H7.
        eapply per_col in H7.
          eapply l8_2 in H7.
          apply H7.
          assumption.
        ColR.
        assumption.
      ColR.
      assert_cols;ColR.
    Between.
Qed.

Lemma l8_21 : A B C,
 A B P, T, Perp A B P A Col A B T Bet C T P.
Proof.
    intros.
    induction(Col_dec A B C).
      assert ( C', ¬ Col A B C').
        eapply l6_25.
        assumption.
      ex_elim H1 C'.
      assert ( P : Tpoint, ( T : Tpoint, Perp A B P A Col A B T Bet C' T P)).
        eapply l8_21_aux.
          assumption.
        assumption.
      ex_elim H1 P.
      ex_and H3 T.
       P.
       C.
      repeat split.
        assumption.
        assumption.
      apply between_trivial2.
    eapply l8_21_aux.
      assumption.
    assumption.
Qed.

Lemma perp_in_col : A B C D X, Perp_at X A B C D Col A B X Col C D X.
Proof.
    unfold Perp_at.
    intuition.
Qed.

Lemma perp_perp_in : A B C, Perp A B C A Perp_at A A B C A.
Proof.
    intros.
    apply l8_15_1.
      unfold Perp in H.
      ex_and H X.
      unfold Perp_at in H0.
      intuition.
      apply col_trivial_3.
    assumption.
Qed.

Lemma perp_per_1 : A B C, AB Perp A B C A Per B A C.
Proof.
    intros.
    assert (Perp_at A A B C A).
      apply perp_perp_in.
      assumption.
    unfold Perp_at in H1.
    spliter.
    apply H5.
    Col.
    Col.
Qed.

Lemma perp_per_2 : A B C, AB Perp A B A C Per B A C.
Proof.
    intros.
    apply perp_right_comm in H0.
    apply perp_per_1; assumption.
Qed.

Lemma perp_col : A B C D E, AE Perp A B C D Col A B E Perp A E C D.
Proof.
    intros.
    apply perp_sym.
    apply perp_col0 with A B;finish.
Qed.

Lemma perp_col2 : 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.
    intros.
    assert(HH:=H).
    apply perp_distinct in HH.
    spliter.
    induction (eq_dec_points A C).
      subst A.
      apply perp_col with B;finish.
    assert(Perp A C X Y) by (eapply perp_col;eauto).
    eapply perp_col with A;finish.
      Perp.
    ColR.
Qed.

Lemma perp_not_eq_1 : A B C D, Perp A B C D AB.
Proof.
    intros.
    unfold Perp in H.
    ex_elim H X.
    unfold Perp_at in H0.
    tauto.
Qed.

Lemma perp_not_eq_2 : A B C D, Perp A B C D CD.
Proof.
    intros.
    apply perp_sym in H.
    eapply perp_not_eq_1.
    apply H.
Qed.

Lemma diff_per_diff : A B P R ,
      A B Cong A P B R Per B A P Per A B R P R.
Proof.
    intros.
    intro.
    subst.
    assert (A = B).
      eapply l8_7.
        apply l8_2.
        apply H1.
      apply l8_2.
      assumption.
    intuition.
Qed.

Lemma per_not_colp : A B P R, A B A P B R Per B A P Per A B R ¬Col P A R.
Proof.
    intros.
    intro.
    assert (Perp A B P A).
      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.
        apply H0.
        assumption.
      ColR.
    apply l8_2 in H3.
    apply l8_2 in H7.
    assert (A = B).
      eapply l8_7.
        apply H7.
      assumption.
    contradiction.
Qed.

Lemma per_not_col : A B C, A B B C Per A B C ¬Col A B C.
Proof.
    intros.
    intro.
    unfold Per in H1.
    ex_and H1 C'.
    assert (C = C' Midpoint A C C').
      eapply l7_20.
        assert_cols;ColR.
        assumption.
    induction H4;treat_equalities; intuition.
Qed.

Lemma per_cong : 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.
    intros.
    assert (Per P A B).
      apply l8_2.
      assumption.
    double B R Q.
    assert (B R).
      intro.
      subst R.
      apply cong_identity in H3.
      subst P.
      absurde.
    assert (Per A B Q).
      eapply per_col.
        apply H8.
        assumption.
      unfold Col.
      left.
      apply midpoint_bet.
      assumption.
    assert (Per P A X).
      eapply per_col.
        apply H.
        assumption.
      assumption.
    assert (B Q).
      intro.
      subst Q.
      apply l7_3 in H7.
      subst R.
      absurde.
    assert (Per R B X).
      eapply per_col.
        intro.
        apply H.
        apply sym_equal.
        apply H12.
        apply l8_2.
        assumption.
      apply col_permutation_4.
      assumption.
    assert (X A).
      intro.
      subst X.
      assert (¬Col P A R).
        eapply per_not_colp.
          apply H.
          assumption.
          assumption.
          assumption.
        assumption.
      apply H13.
      unfold Col.
      left.
      assumption.
    double P A P'.
    prolong P' X R' X R.
    assert ( M, Midpoint M R R').
      eapply l7_25.
      apply cong_symmetry.
      apply H16.
    ex_elim H17 M.
    assert (Per X M R).
      unfold Per.
       R'.
      split.
        assumption.
      apply cong_symmetry.
      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''.
      assumption.
    assert (X P').
      intro.
      subst P'.
      apply cong_identity in H19.
      subst X.
      apply l7_3 in H14.
      subst P.
      absurde.
    assert (P P').
      intro.
      subst P'.
      eapply l7_3 in H14.
      subst P.
      absurde.
    assert(¬Col X P P').
      intro.
      assert(Col X P A).
        eapply col3.
          apply H21.
          apply col_permutation_1.
          assumption.
          apply col_trivial_3.
        unfold Col.
        right;left.
        apply between_symmetry.
        apply midpoint_bet.
        assumption.
      apply col_permutation_1 in H23.
      assert (P = A X = A).
        eapply l8_9.
          assumption.
        assumption.
      induction H24.
        subst P.
        absurde.
      apply H13.
      assumption.
    assert (Bet A X M).
      eapply l7_22.
        5:apply H14.
        5:apply H18.
        assumption.
        assumption.
        assumption.
      apply cong_symmetry.
      assumption.
    assert (X R).
      intro.
      treat_equalities.
      apply perBAB in H12.
      treat_equalities.
      unfold Midpoint in ×.
      spliter.
      treat_equalities.
      intuition.
    assert (X R').
      intro.
      subst R'.
      apply cong_symmetry in H16.
      apply cong_identity in H16.
      apply H24.
      assumption.
    assert (M X).
      intro.
      subst M.
      apply H22.
      eapply col_transitivity_1.
        apply H24.
        unfold Col.
        right; right.
        assumption.
      eapply col_transitivity_1.
        apply H25.
        unfold Col.
        right;right.
        apply midpoint_bet.
        assumption.
      unfold Col.
      right; right.
      assumption.
    assert (M = B).
      eapply (l8_18_uniqueness A X R).
        intro.
        assert (Col A B R).
          eapply col_transitivity_1.
            intro.
            apply H13.
            apply sym_equal.
            apply H28.
            apply col_permutation_5.
            assumption.
          assumption.
        eapply per_not_col.
          apply H; apply H12.
          apply H8.
          assumption.
        assumption.
        unfold Col.
        left.
        assumption; eapply col_transitivity_1.
        apply per_perp in H17.
          apply perp_comm.
          eapply perp_col.
            assumption.
            apply H17.
          unfold Col.
          right;right.
          assumption.
          auto.
        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.
            right;right.
            assumption.
          unfold Col.
          right; right.
          assumption.
        eapply l7_3_2.
        apply col_permutation_5.
        assumption.
      apply per_perp in H10.
        apply perp_comm.
        eapply perp_col.
          apply H13.
          apply perp_comm.
          eapply perp_col.
            intro.
            apply H13.
            apply sym_equal.
            apply H27.
            apply perp_right_comm.
            apply per_perp in H2.
              apply H2.
              assumption.
            assumption.
          assumption.
        apply col_trivial_2.
        auto.
      intro.
      apply H13.
      subst X.
      reflexivity.
    subst M.
    assert(OFSC P X R P' P' X R' P).
      unfold OFSC.
      repeat split.
        assumption.
        assumption.
        apply cong_commutativity.
        assumption.
        apply cong_symmetry.
        assumption.
        apply cong_pseudo_reflexivity.
      apply cong_symmetry.
      assumption.
    assert (Cong R P' R' P).
      eapply five_segment_with_def.
        apply H27.
      intro.
      subst X.
      apply H22.
      apply col_trivial_1.
    assert (IFSC P' A P R R' B R P).
      unfold IFSC.
      repeat split.
        apply between_symmetry.
        apply midpoint_bet.
        assumption.
        apply between_symmetry.
        apply midpoint_bet.
        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.
            apply l7_2.
            apply H14.
          eapply cong_transitivity.
            apply H3.
          apply cong_commutativity.
          apply midpoint_cong.
          assumption.
        assumption.
        assumption.
        Cong.
      apply cong_pseudo_reflexivity.
    eapply cong_right_commutativity.
    eapply l4_2.
    eapply H29.
Qed.

Lemma perp_cong : 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.
    intros.
    apply (per_cong A B P R X).
      assumption.
      assumption.
      apply perp_per_1.
        assumption.
      assumption.
      eapply perp_per_1.
        auto.
      apply perp_left_comm;auto.
      assumption.
      assumption.
    assumption.
Qed.

Lemma midpoint_existence_aux : A B P Q T,
  AB Perp A B Q B Perp A B P A
  Col A B T Bet Q T P Le A P B Q
   X : Tpoint, Midpoint X A B.
Proof.
    intros.
    unfold Le in H4.
    ex_and H4 R.
    assert ( X, Bet T X B Bet R X P).
      eapply inner_pasch.
        apply between_symmetry.
        apply H3.
      auto.
    ex_and H6 X.
    assert (Col A B X).
      induction (eq_dec_points T B).
        subst T.
        apply between_identity in H6.
        subst X.
        Col.
     assert_cols;ColR.
     induction(Col_dec A B P).
      assert (B=A P=A).
        eapply l8_9.
          apply perp_per_1.
            assumption.
          assumption.
        apply col_permutation_4.
        assumption.
      induction H10.
         A.
        subst B.
        eapply l7_3_2.
      treat_equalities.
      apply perp_distinct in H1.
      spliter.
      absurde.
    assert (B R).
      intro.
      subst R.
      treat_equalities.
      apply H9.
      apply col_trivial_3.
    assert (¬Col A B Q).
      intro.
      assert (A=B Q=B).
        eapply l8_9.
          apply perp_per_2.
            auto.
          apply perp_comm.
          assumption.
        assumption.
      induction H12.
        apply H.
        assumption.
      subst Q.
      treat_equalities.
      absurde.
    assert (¬Col A B R).
      intro.
      assert (Col B A Q).
        assert_cols;ColR.
      Col.
    show_distinct P R.
      intuition.
    induction (eq_dec_points A P).
      subst P.
      apply perp_distinct in H1.
      spliter.
      absurde.
    assert (Perp A B R B).
      eapply perp_col.
        assumption.
        apply perp_sym.
        apply perp_left_comm.
        eapply perp_col.
          assumption.
          apply perp_left_comm.
          apply perp_sym.
          apply H0.
        assert_cols;Col.
      Col.
    apply between_symmetry in H7.
    assert (Cong A R P B).
      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.
    spliter. X.
    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 : A B, X, Midpoint X A B.
Proof.
    intros.
    induction (eq_dec_points A B).
      subst B.
       A.
      apply l7_3_2.
    cut( Q, Perp A B B Q).
      intro.
      ex_elim H0 Q.
      cut( P, T, Perp A B P A Col A B T Bet Q T P).
        intros.
        ex_elim H0 P.
        ex_and H2 T.
        assert (Le A P B Q Le B Q A P) by (apply le_cases).
        induction H4.
          apply midpoint_existence_aux with P Q T;finish;Perp.
        assert ( X : Tpoint, Midpoint X B A)
          by (apply (midpoint_existence_aux B A Q P T);finish;Perp;Between).
        ex_elim H5 X.
         X.
        finish.
       apply l8_21;assumption.
    assert ( P : Tpoint, ( T : Tpoint, Perp B A P B Col B A T Bet A T P)) by (apply (l8_21 B A);auto).
    ex_elim H0 P.
    ex_elim H1 T.
    spliter.
     P.
    Perp.
Qed.

Lemma perp_in_id : A B C X, Perp_at X A B C A X = A.
Proof.
    intros.
    assert (Perp A B C A).
      unfold Perp.
       X.
      assumption.
    assert (A B C A).
      apply perp_distinct.
      assumption.
    spliter.
    assert (HH:=H0).
    apply perp_perp_in in HH.
    assert (l8_16_1:=l8_16_1 A B C B A).
    assert (¬Col A B C Per C A B).
      apply l8_16_1;Col.
    spliter.
    unfold Perp_at in H.
    spliter.
    eapply l8_18_uniqueness with A B C;finish.
      apply perp_sym.
      eapply perp_col with A;finish.
        intro.
        subst X.
        Col.
        apply perp_sym.
        apply H0.
Qed.

Lemma l8_22 : 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.
    intros.
    assert (Cong A R P B).
      apply (per_cong A B P R X); assumption.
    split.
      assumption.
    assert (¬ Col B A P).
      eapply per_not_col.
        auto.
        assumption.
      assumption.
    assert_all_diffs_by_contradiction.
    apply l7_21;finish.
Qed.

Lemma l8_22_bis : 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.
    intros.
    apply l8_22;finish.
       apply perp_per_1;finish.
       apply perp_per_1;finish;Perp.
Qed.

Lemma perp_in_perp : A B C D X, Perp_at X A B C D Perp A B C D.
Proof.
    intros.
    unfold Perp.
     X.
    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 : A B C D, Perp A B C D ¬Col A C D X, Col A B X Perp A X C D.
Proof.
    intros.
    unfold Perp in H.
    ex_and H X.
     X.
    split.
      unfold Perp_at in H1.
      spliter.
      apply col_permutation_1.
      assumption.
    eapply perp_col.
      intro.
      subst X.
      unfold Perp_at in H1.
      spliter.
      apply H0.
      assumption.
      apply perp_in_perp in H1.
      apply H1.
    unfold Perp_at in H1.
    spliter.
    apply col_permutation_1.
    assumption.
Qed.

Lemma l8_24 : 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
  X, Midpoint X A B Midpoint X P R.
Proof.
    intros.
    unfold Le in H4.
    assert ( X, Bet T X B Bet R X P).
      eapply inner_pasch.
        apply H2.
      assumption.
    ex_and H5 X.
    assert (Col A B X).
      induction (eq_dec_points T B).
        subst T.
        apply between_identity in H5.
        subst X.
        apply col_trivial_2.
      assert (Col T X B).
        unfold Col.
        left.
        assumption.
      apply col_permutation_4.
      eapply col_transitivity_1.
        intro.
        apply H7.
        apply sym_equal.
        apply H9.
        apply col_permutation_1.
        assumption.
      apply col_permutation_2.
      assumption.
    assert (A B).
      apply perp_distinct in H.
      spliter.
      assumption.
    assert (A P).
      apply perp_distinct in H.
      spliter.
      auto.
    induction(Col_dec A B P).
      assert (B=A P=A).
        eapply l8_9.
          apply perp_per_1.
            assumption.
          apply perp_sym.
          assumption.
        apply col_permutation_4.
        assumption.
      induction H11.
         A.
        subst B.
        absurde.
      subst P.
      absurde.
    assert (B R).
      intro.
      subst R.
      apply cong_identity in H4.
      subst P.
      absurde.
    assert (Q B).
      apply perp_distinct in H0.
      spliter.
      assumption.
    assert (¬Col A B Q).
      intro.
      assert (A=B Q=B).
        eapply l8_9.
          apply perp_per_2.
            auto.
          apply perp_comm.
          apply perp_sym.
          assumption.
        assumption.
      induction H14.
        contradiction.
      subst Q.
      absurde.
    assert (¬Col A B R).
      intro.
      assert (Col B A Q).
        eapply col_transitivity_1.
          apply H11.
          apply col_permutation_1.
          assumption.
        unfold Col.
        left.
        assumption.
      apply H13.
      apply col_permutation_4.
      assumption.
    assert (P R).
      intro.
      subst R.
      apply between_identity in H6.
      subst X.
      contradiction.
    induction (eq_dec_points A P).
      subst P.
      apply perp_distinct in H.
      spliter.
      absurde.
    assert (Perp A B R B).
      eapply perp_col.
        assumption.
        apply perp_sym.
        apply perp_left_comm.
        eapply perp_col.
          assumption.
          apply perp_left_comm.
          apply H0.
        unfold Col.
        right; left.
        apply between_symmetry.
        assumption.
      apply col_trivial_2.
    assert (Cong A R P B).
      apply (perp_cong A B P R X).
        assumption.
        assumption.
        apply perp_sym.
        assumption.
        assumption.
        assumption.
        assumption.
      apply between_symmetry.
      assumption.
    intros.
    assert (Midpoint X A B Midpoint X P R).
      apply (l7_21 A P B R X).
        intro.
        apply H10.
        apply col_permutation_5.
        assumption.
        assumption.
        assumption.
        apply cong_right_commutativity.
        apply cong_symmetry.
        assumption.
        apply col_permutation_5.
        assumption.
      unfold Col.
      left.
      apply between_symmetry.
      assumption.
     X.
    assumption.
Qed.

Lemma perp_not_col2 : A B C D, Perp A B C D ¬ Col A B C ¬ Col A B D.
Proof.
    intros.
    induction (Col_dec A B C).
      right.
      assert(Perp_at C A B C D).
        apply l8_14_2_1b_bis; Col.
      intro.
      assert(Perp_at D A B C D).
        apply l8_14_2_1b_bis; Col.
      assert(C = D).
        eapply l8_14_3.
          apply H1.
        assumption.
      apply perp_not_eq_2 in H.
      contradiction.
    left.
    assumption.
Qed.

Lemma perp_not_col : A B P, Perp A B P A ¬ Col A B P.
Proof.
    intros.
    assert (Perp_at A A B P A).
      apply perp_perp_in.
      assumption.
    assert (Per P A B).
      apply perp_in_per.
      apply perp_in_sym.
      assumption.
    apply perp_in_left_comm in H0.
    assert (¬ Col B A P ¬ Col A B P).
      intro.
      intro.
      apply H2.
      apply col_permutation_4.
      assumption.
    apply H2.
    apply perp_distinct in H.
    spliter.
    apply per_not_col.
      auto.
      auto.
    apply perp_in_per.
    apply perp_in_right_comm.
    assumption.
Qed.

Lemma ex_col2 : A B, C, Col A B C A C B C.
Proof.
    intros.
    induction(eq_dec_points A B).
      subst B.
      assert(HH:=another_point A).
      ex_and HH B.
       B.
      split; Col.
    prolong A B C A B.
     C.
    split.
      apply bet_col.
      assumption.
    split.
      intro.
      subst C.
      apply between_identity in H0.
      contradiction.
    intro.
    subst C.
    apply cong_symmetry in H1.
    apply cong_identity in H1.
    contradiction.
Qed.

Lemma perp_in_col_perp_in : 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.
    intros.
    unfold Perp_at in ×.
    spliter.
    repeat split; auto.
      ColR.
    intros.
    apply H5.
      assumption.
    ColR.
Qed.

Lemma perp_col2_bis : 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.
intros A B C D P Q HPerp HCol1 HCol2 HCD.
apply perp_sym.
apply perp_col2 with P Q; Perp; ColR.
Qed.

Lemma perp_in_perp_bis : A B C D X,
 Perp_at X A B C D Perp X B C D Perp A X C D.
Proof.
    intros.
    induction (eq_dec_points X A).
      subst X.
      left.
      unfold Perp.
       A.
      assumption.
    right.
    unfold Perp.
     X.
    unfold Perp_at in ×.
    spliter.
    repeat split.
      intro.
      apply H0.
      subst X.
      reflexivity.
      assumption.
      apply col_trivial_3.
      assumption.
    intros.
    apply H4.
      apply col_permutation_2.
      eapply col_transitivity_1.
        intro.
        apply H0.
        apply sym_equal.
        apply H7.
        Col.
      Col.
    assumption.
Qed.

Lemma col_per_perp : 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.
    intros.
    apply per_perp_in in H4.
      apply perp_in_perp_bis in H4.
      induction H4.
        apply perp_distinct in H4.
        spliter.
        absurde.
      eapply (perp_col _ B).
        auto.
        apply perp_sym.
        apply perp_right_comm.
        assumption.
      apply col_permutation_4.
      assumption.
      assumption.
    assumption.
Qed.

Lemma per_cong_mid : A B C H,
 B C Bet A B C Cong A H C H Per H B C
 Midpoint B A C.
Proof.
    intros.
    induction (eq_dec_points H B).
      subst H.
      unfold Midpoint.
      split.
        assumption.
      apply cong_right_commutativity.
      assumption.
    assert(Per C B H).
      apply l8_2.
      assumption.
    assert (Per H B A).
      eapply per_col.
        apply H0.
        assumption.
      unfold Col.
      right; right.
      assumption.
    assert (Per A B H).
      apply l8_2.
      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.
        2:apply H5.
        assumption.
        apply cong_commutativity.
        apply midpoint_cong.
        apply l7_2.
        apply H5.
        apply midpoint_bet.
        assumption.
      apply cong_commutativity.
      apply midpoint_cong.
      apply l7_2.
      assumption.
    subst H''.
    assert(IFSC H B H' A H B H' C).
      repeat split.
        apply midpoint_bet.
        assumption.
        apply midpoint_bet.
        assumption.
        apply cong_reflexivity.
        apply cong_reflexivity.
        apply cong_commutativity.
        assumption.
      apply cong_commutativity.
      eapply cong_transitivity.
        apply cong_symmetry.
        apply H11.
      eapply cong_transitivity.
        apply H2.
      assumption.
    eapply l4_2 in H12.
    unfold Midpoint.
    split.
      assumption.
    apply cong_left_commutativity.
    assumption.
Qed.

Lemma per_double_cong : A B C C',
 Per A B C Midpoint B C C' Cong A C A C'.
Proof.
    intros.
    unfold Per in H.
    ex_and H C''.
    assert (C' = C'').
      eapply l7_9.
        apply l7_2.
        apply H0.
      apply l7_2.
      assumption.
    subst C''.
    assumption.
Qed.

End T8_5.

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.