Library GeoCoq.Tarski_dev.Ch08_orthogonality

Require Export GeoCoq.Tarski_dev.Ch07_midpoint.
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 (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_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 :=
  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: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 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
 end.

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.
Section T8_1.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

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 → A≠B → 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.

Lemma col_col_per_per : ∀ 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.
    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.

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 ∧ U≠X ∧ V≠X ∧ 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.

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.
    apply (H5 Y Y) in H1.
      apply eq_sym, l8_8; assumption.
    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, A≠B → 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, A≠B → 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,
  A≠B → Col A B X → Col A B U → U≠X → 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,
  A≠B → Col A B X → Col A B U → U≠X → ¬ 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 midpoint_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 → B≠C → A≠P.
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_bets.
      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_bets;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,
 ¬ 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 H0 X.
    assert (Perp_at X A B C X).
      eapply l8_15_1; assert_diffs; auto.
    assert (Per A X C).
      unfold Perp_at in H2.
      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 (∃ P, Midpoint P C' C'').
      eapply l7_25.
      unfold Midpoint in ×.
      spliter.
      eapply cong_transitivity.
        apply cong_symmetry.
        apply H4.
      apply cong_left_commutativity.
      assumption; spliter.
    ex_elim H6 P.
    assert (Per X A P).
      eapply l8_20_1.
        apply HH.
        apply l7_2.
        apply H7.
        apply l7_2.
        apply H5.
      apply l7_2.
      assumption.
    assert (X ≠ C).
      intro.
      subst C.
      apply H.
      assumption.
    assert (A ≠ P).
      eapply l8_20_2.
        apply HH.
        apply l7_2.
        apply H7.
        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 H5.
        apply midpoint_bet.
        apply l7_2.
        apply H3.
      apply midpoint_bet.
      apply l7_2.
      apply H7.
    ex_and H10 T.
    induction (eq_dec_points A X).
      subst X.
      ∃ P.
      ∃ T.
      apply between_identity in H11.
      subst T.
      assert (C'= C'').
        eapply symmetric_point_uniqueness.
          apply H3.
        assumption.
      subst C''.
      apply l7_3 in H7.
      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.
        assert_diffs; auto.
        auto.
        apply col_trivial_1.
        apply col_trivial_3.
      unfold Perp_at in H2.
      spliter.
      intros.
      eapply per_col in H6.
        apply l8_2 in H6.
        eapply per_col in H6.
          eapply l8_2 in H6.
          apply H6.
          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 not_col_exists.
        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.
      ex_elim H1 P.
      ex_and H3 T.
      ∃ P.
      ∃ C.
      repeat split.
        assumption.
        assumption.
      apply between_trivial2.
    eapply l8_21_aux.
    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, 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 H0.
    spliter.
    apply H4.
    Col.
    Col.
Qed.

Lemma perp_per_2 : ∀ A B C, Perp A B A C → Per B A C.
Proof.
    intros.
    apply perp_right_comm in H.
    apply perp_per_1; assumption.
Qed.

Lemma perp_col : ∀ A B C D E, A≠E → 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 → A≠B.
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 → C≠D.
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 l8_8 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.
      eapply perp_per_1.
        auto.
      apply perp_left_comm;auto.
      assumption.
      assumption.
    assumption.
Qed.

Lemma midpoint_existence_aux : ∀ 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 →
  ∃ 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.
        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.