Library GeoCoq.Tarski_dev.Ch11_angles

Require Export GeoCoq.Tarski_dev.Ch10_line_reflexivity_2D.

Ltac permut :=
match goal with
   |H : (Col ?X ?Y ?Z) |- Col ?X ?Y ?Zassumption
   |H : (Col ?X ?Y ?Z) |- Col ?Y ?Z ?Xapply col_permutation_1; assumption
   |H : (Col ?X ?Y ?Z) |- Col ?Z ?X ?Yapply col_permutation_2; assumption
   |H : (Col ?X ?Y ?Z) |- Col ?X ?Z ?Yapply col_permutation_5; assumption
   |H : (Col ?X ?Y ?Z) |- Col ?Y ?X ?Zapply col_permutation_4; assumption
   |H : (Col ?X ?Y ?Z) |- Col ?Z ?Y ?Xapply col_permutation_3; assumption
   |_ : _ |- _idtac
end.

Ltac bet :=
match goal with
   |H0 : Bet ?A ?B ?C |- Bet ?A ?B ?Cassumption
   |H0 : Bet ?A ?B ?C, H1 : Bet ?B ?C ?D , H : ?B ?C |- Bet ?A ?B ?Dapply (outer_transitivity_between _ _ _ _ H0 H1 H)
   |H0 : Bet ?A ?B ?C, H1 : Bet ?B ?C ?D , H : ?B ?C |- Bet ?A ?C ?Dapply (outer_transitivity_between2 _ _ _ _ H0 H1 H)
   |H0 : Bet ?A ?B ?D, H1 : Bet ?B ?C ?D |- Bet ?A ?B ?Capply (between_inner_transitivity _ _ _ _ H0 H1)
   |H0 : Bet ?A ?B ?C, H1 : Bet ?A ?C ?D |- Bet ?B ?C ?Dapply (between_exchange3 _ _ _ _ H0 H1)
   |H0 : Bet ?A ?B ?D, H1 : Bet ?B ?C ?D |- Bet ?A ?C ?Dapply (between_exchange2 _ _ _ _ H0 H1)
   |H0 : Bet ?A ?B ?C, H1 : Bet ?A ?C ?D |- Bet ?A ?B ?Dapply (between_exchange4 _ _ _ _ H0 H1)

   |H0 : Bet ?A ?B ?C |- Bet ?A ?B ?Cassumption
   |H0 : Bet ?A ?B ?C, H1 : Bet ?B ?C ?D , H : ?B ?C |- Bet ?D ?B ?Aapply between_symmetry; apply (outer_transitivity_between _ _ _ _ H0 H1 H)
   |H0 : Bet ?A ?B ?C, H1 : Bet ?B ?C ?D , H : ?B ?C |- Bet ?D ?C ?Aapply (outer_transitivity_between2 _ _ _ _ H0 H1 H)
   |H0 : Bet ?A ?B ?D, H1 : Bet ?B ?C ?D |- Bet ?C ?B ?Aapply between_symmetry; apply (between_inner_transitivity _ _ _ _ H0 H1)
   |H0 : Bet ?A ?B ?C, H1 : Bet ?A ?C ?D |- Bet ?D ?C ?Bapply between_symmetry; apply (between_exchange3 _ _ _ _ H0 H1)
   |H0 : Bet ?A ?B ?D, H1 : Bet ?B ?C ?D |- Bet ?D ?C ?Aapply between_symmetry; apply (between_exchange2 _ _ _ _ H0 H1)
   |H0 : Bet ?A ?B ?C, H1 : Bet ?A ?C ?D |- Bet ?D ?B ?Aapply between_symmetry; apply (between_exchange4 _ _ _ _ H0 H1)
   |H0 : Bet ?A ?B ?C |- Bet ?C ?B ?Aapply (between_symmetry _ _ _ H0)

   |H0 : Bet ?A ?B ?C |- Bet ?C ?B ?Aapply (between_symmetry _ _ _ H0)
   |_ : _ |- Bet ?A ?B ?Bapply between_trivial
   |_ : _ |- Bet ?A ?A ?Bapply between_trivial2
   |_ : _ |- _idtac
end.

Ltac cong :=
match goal with
   |_ : Cong ?A ?B ?C ?BD |- Cong ?A ?B ?C ?Dassumption
   |_ : _ |- Cong ?A ?B ?A ?Bapply cong_reflexivity
   |_ : _ |- Cong ?A ?A ?B ?Bapply cong_trivial_identity

   |H0 : Cong ?A ?B ?C ?D |- Cong ?A ?B ?C ?Cassumption
   |H0 : Cong ?A ?B ?C ?D |- Cong ?A ?B ?D ?Capply (cong_right_commutativity _ _ _ _ H0)
   |H0 : Cong ?A ?B ?C ?D |- Cong ?B ?A ?D ?Capply (cong_commutativity _ _ _ _ H0)
   |H0 : Cong ?A ?B ?C ?D |- Cong ?B ?A ?C ?Dapply (cong_left_commutativity _ _ _ _ H0)

   |H0 : Cong ?A ?B ?C ?D |- Cong ?C ?D ?A ?Bapply (cong_symmetry _ _ _ _ H0)
   |H0 : Cong ?A ?B ?C ?D |- Cong ?C ?D ?B ?Aapply (cong_symmetry _ _ _ _ (cong_left_commutativity _ _ _ _ H0))
   |H0 : Cong ?A ?B ?C ?D |- Cong ?D ?C ?B ?Bapply (cong_symmetry _ _ _ _ (cong_commutativity _ _ _ _ H0))
   |H0 : Cong ?A ?B ?C ?D |- Cong ?D ?C ?A ?Bapply (cong_symmetry _ _ _ _ (cong_right_commutativity _ _ _ _ H0))
   |_ : _ |- _idtac
end.

Section T11_1.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Definition CongA A B C D E F :=
  A B C B D E F E
   A', C', D', F',
  Bet B A A' Cong A A' E D
  Bet B C C' Cong C C' E F
  Bet E D D' Cong D D' B A
  Bet E F F' Cong F F' B C
  Cong A' C' D' F'.

Lemma l11_3 : A B C D E F,
 CongA A B C D E F
  A', C', D', F',
 Out B A' A Out B C C' Out E D' D Out E F F'
 Cong_3 A' B C' D' E F'.
Proof.
    intros.
    unfold CongA in H.
    spliter.
    ex_and H3 A'.
    ex_and H4 C'.
    ex_and H3 D'.
    ex_and H4 F'.
     A'.
     C'.
     D'.
     F'.
    repeat split.
      intro.
      subst A'.
      apply between_identity in H3.
      subst B.
      absurde.
      assumption.
      right.
      assumption.
      assumption.
      intro.
      subst C'.
      apply between_identity in H5.
      subst C.
      absurde.
      left.
      assumption.
      intro.
      subst D'.
      apply between_identity in H7.
      subst E.
      absurde.
      assumption.
      right.
      assumption.
      assumption.
      intro.
      subst F'.
      apply between_identity in H9.
      subst F.
      absurde.
      left.
      assumption.
      2:assumption.
      apply cong_left_commutativity.
      eapply l2_11.
        apply H3.
        apply between_symmetry.
        apply H7.
        Cong.
      Cong.
    apply cong_left_commutativity.
    eapply l2_11; eBetween;eCong.
Qed.

Lemma l11_aux : B A A' A0 E D D' D0,
      Out B A A' Out E D D' Cong B A' E D'
      Bet B A A0 Bet E D D0 Cong A A0 E D
       Cong D D0 B A Cong B A0 E D0 Cong A' A0 D' D0.
Proof.
    intros.
    assert (A B).
      unfold Out in H.
      spliter.
      assumption.
    assert(Cong B A0 E D0).
      apply cong_right_commutativity.
      eapply (l2_11).
        apply H2.
        apply between_symmetry.
        apply H3.
        apply cong_right_commutativity.
        apply cong_symmetry.
        apply H5.
      apply cong_right_commutativity.
      apply H4.
    split.
      apply H7.
    unfold Out in ×.
    spliter.
    induction H9; induction H11.
      assert(Bet B A' A0 Bet B A0 A').
        eapply l5_1.
          2:apply H11.
          auto.
        apply H2.
      induction H12.
        assert(Bet E D' D0).
          eapply cong_preserves_bet.
            2: apply H1.
            apply H12.
            assumption.
          unfold Out.
          repeat split.
            assumption.
            intro.
            subst D0.
            apply cong_identity in H7.
            subst A0.
            apply between_identity in H2.
            subst B.
            absurde.
          eapply l5_1.
            2:apply H9.
            auto.
          assumption.
        apply cong_commutativity.
        eapply l4_3.
          apply between_symmetry.
          apply H12.
          apply between_symmetry.
          apply H13.
          apply cong_commutativity.
          assumption.
        apply cong_commutativity.
        assumption.
      assert(Bet E D0 D').
        eapply cong_preserves_bet.
          2: apply H7.
          apply H12.
          assumption.
        unfold Out.
        repeat split.
          intro.
          subst D0.
          apply cong_identity in H7.
          subst A0.
          apply between_identity in H2.
          subst B.
          absurde.
          assumption.
        eapply l5_1.
          2:apply H3.
          auto.
        assumption.
      eapply l4_3.
        apply between_symmetry.
        apply H12.
        apply between_symmetry.
        apply H13.
        apply cong_commutativity.
        assumption.
      apply cong_commutativity.
      assumption.
      apply cong_commutativity.
      eapply l4_3.
        3:apply cong_commutativity.
        3:apply H7.
        apply between_symmetry.
        eapply between_exchange4.
          apply H11.
        assumption.
        apply between_symmetry.
        eapply cong_preserves_bet.
          2: apply H1.
          2: apply H7.
          eapply between_exchange4.
            apply H11.
          assumption.
        unfold Out.
        repeat split.
          assumption.
          intro.
          subst D0.
          apply cong_identity in H7.
          subst A0.
          apply between_identity in H2.
          subst B.
          absurde.
        eapply l5_1.
          2:apply H9.
          auto.
        assumption.
      apply cong_commutativity.
      assumption.
      apply cong_commutativity.
      eapply l4_3.
        3:apply cong_commutativity.
        3:apply H7.
        apply between_symmetry.
        eapply cong_preserves_bet.
          2:apply cong_symmetry.
          2:apply H1.
          2:apply cong_symmetry.
          2:apply H7.
          eapply between_exchange4.
            apply H9.
          assumption.
        unfold Out.
        repeat split.
          assumption.
          intro.
          subst A0.
          apply cong_symmetry in H7.
          apply cong_identity in H7.
          subst D0.
          apply between_identity in H2.
          subst B.
          absurde.
        eapply l5_1.
          2:apply H11.
          auto.
        assumption.
        apply between_symmetry.
        eapply between_exchange4.
          apply H9.
        assumption.
      apply cong_commutativity.
      assumption.
    apply cong_commutativity.
    eapply l4_3.
      3:apply cong_commutativity.
      3:apply H7.
      apply between_symmetry.
      eapply between_exchange4.
        apply H11.
      assumption.
      apply between_symmetry.
      eapply between_exchange4.
        apply H9.
      assumption.
    apply cong_commutativity.
    assumption.
Qed.

Lemma l11_3_bis : A B C D E F,
 ( A', C', D', F',
 Out B A' A Out B C' C Out E D' D Out E F' F
 Cong_3 A' B C' D' E F') CongA A B C D E F.
Proof.
    intros.
    unfold CongA.
    ex_and H A'.
    ex_and H0 C'.
    ex_and H D'.
    ex_and H0 F'.
    prolong B A A0 E D.
    prolong B C C0 E F.
    prolong E D D0 B A.
    prolong E F F0 B C.
    assert(HH0:=H0).
    assert(HH1:=H1).
    assert(HH2:=H2).
    assert(HH:=H).
    unfold Out in HH.
    unfold Out in HH0.
    unfold Out in HH1.
    unfold Out in HH2.
    spliter.
    repeat split;try assumption.
    repeat split;try assumption.
     A0.
     C0.
     D0.
     F0.
    repeat split; try (assumption).
    unfold Cong_3 in H3.
    spliter.
    assert(Cong B A0 E D0 Cong A' A0 D' D0).
      eapply l11_aux.
        apply l6_6.
        apply H.
        apply l6_6.
        apply H1.
        apply cong_commutativity.
        assumption.
        assumption.
        assumption.
        assumption.
      assumption.
    assert(Cong B C0 E F0 Cong C' C0 F' F0).
      eapply l11_aux.
        apply l6_6.
        apply H0.
        apply l6_6.
        apply H2.
        assumption.
        assumption.
        assumption.
        assumption.
      assumption.
    spliter.
    assert (Cong_3 B A' A0 E D' D0).
      repeat split.
        apply cong_commutativity.
        assumption.
        assumption.
      assumption.
    assert (Cong_3 B C' C0 E F' F0).
      repeat split.
        assumption.
        assumption.
      assumption.
    assert (Cong C0 A' F0 D').
      eapply l4_16.
        unfold FSC.
        split.
          2:split.
            2:apply H31.
          apply out_col in H0.
          apply bet_col in H6.
          ColR.
        split.
          Cong.
        Cong.
      auto.
    eapply l4_16.
      unfold FSC.
      split.
        2:split.
          2:apply H30.
        assert_cols.
        ColR.
      split.
        assumption.
      Cong.
    auto.
Qed.

Lemma l11_4_1 : A B C D E F,
  CongA A B C D E F AB CB DE FE
  ( A' C' D' F', Out B A' A Out B C' C Out E D' D Out E F' F
  Cong B A' E D' Cong B C' E F' Cong A' C' D' F').
Proof.
    intros.
    assert (HH:=H).
    apply l11_3 in HH.
    unfold CongA in H.
    spliter.
    repeat split; try assumption.
    clear H3.
    intros.
    ex_and HH A0.
    ex_and H4 C0.
    ex_and H10 D0.
    ex_and H4 F0.
    unfold Cong_3 in H13.
    spliter.
    assert (Out B A' A0).
      eapply l6_7.
        apply H3.
      apply l6_6.
      assumption.
    assert (Out E D' D0).
      eapply l6_7.
        apply H6.
      apply l6_6.
      assumption.
    assert(Cong A' A0 D' D0).
      eapply out_cong_cong.
        apply H16.
        apply H17.
        assumption.
      Cong.
    assert (Cong A' C0 D' F0).
      eapply (l4_16 B A0 A' C0 E D0 D' F0).
        unfold FSC.
        repeat split.
          assert_cols;Col.
          Cong.
          assumption.
          Cong.
          assumption.
        assumption.
      intro.
      subst A0.
      unfold Out in H4.
      spliter.
      absurde.
    assert (Out B C' C0).
      eapply l6_7.
        apply H5.
      assumption.
    assert (Out E F' F0).
      eapply l6_7.
        apply H7.
      assumption.
    assert(Cong C' C0 F' F0).
      eapply out_cong_cong.
        3:apply H9.
        assumption.
        assumption.
      assumption.
    apply cong_commutativity.
    eapply (l4_16 B C0 C' A' E F0 F' D').
      unfold FSC.
      repeat split.
        apply out_col.
        apply l6_6.
        assumption.
        assumption.
        assumption.
        Cong.
        assumption.
      Cong.
    intro.
    subst C0.
    unfold Out in H10.
    spliter.
    absurde.
Qed.

Lemma l11_4_2 : A B C D E F,
  (AB CB DE FE
  ( A' C' D' F', Out B A' A Out B C' C Out E D' D Out E F' F
  Cong B A' E D' Cong B C' E F' Cong A' C' D' F')) CongA A B C D E F.
Proof.
    intros.
    spliter.
    eapply l11_3_bis.
    prolong B A A' E D.
    prolong B C C' E F.
    prolong E D D' B A.
    prolong E F F' B C.
     A'.
     C'.
     D'.
     F'.
    assert(Cong A' B D' E).
      apply cong_right_commutativity.
      eapply l2_11.
        apply between_symmetry.
        apply H4.
        apply H8.
        Cong.
      Cong.
    assert (Cong B C' E F').
      apply cong_right_commutativity.
      eapply l2_11.
        apply H6.
        apply between_symmetry.
        apply H10.
        Cong.
      Cong.
    assert(Out B A' A Out B C' C Out E D' D Out E F' F).
      repeat split.
        intro.
        subst A'.
        treat_equalities;intuition.
        assumption.
        right.
        assumption.
        intro.
        subst C'.
        apply between_identity in H6.
        subst C.
        absurde.
        assumption.
        right.
        assumption.
        intro.
        subst D'.
        apply between_identity in H8.
        subst E.
        absurde.
        assumption.
        right.
        assumption.
        intro.
        subst F'.
        apply between_identity in H10.
        subst F.
        absurde.
        assumption.
      right.
      assumption.
    spliter.
    split.
      assumption.
    split.
      assumption.
    split.
      assumption.
    split.
      assumption.
    repeat split.
      assumption.
      2:assumption.
    apply H3.
    split.
      assumption.
    split.
      assumption.
    split.
      assumption.
    split.
      assumption.
    split.
      Cong.
    assumption.
Qed.

Lemma conga_refl : A B C, A B C B CongA A B C A B C.
Proof.
    intros.
    apply l11_3_bis.
     A.
     C.
     A.
     C.
    repeat split; try assumption; Between;Cong.
Qed.

Lemma conga_sym : A B C A' B' C', CongA A B C A' B' C' CongA A' B' C' A B C.
Proof.
    unfold CongA.
    intros.
    spliter.
    ex_and H3 A0.
    ex_and H4 C0.
    ex_and H3 D0.
    ex_and H4 F0.
    repeat split; try assumption.
     D0.
     F0.
     A0.
     C0.
    repeat split; try assumption;Cong.
Qed.

Lemma out_conga :
  A B C A' B' C' A0 C0 A1 C1,
 CongA A B C A' B' C'
 Out B A A0
 Out B C C0
 Out B' A' A1
 Out B' C' C1
 CongA A0 B C0 A1 B' C1.
Proof.
    intros.
    apply l11_4_1 in H.
    spliter.
    apply l11_4_2.
    repeat split.
      intro.
      subst A0.
      unfold Out in H0.
      spliter.
      absurde.
      intro.
      subst C0.
      unfold Out in H1.
      spliter.
      absurde.
      intro.
      subst A1.
      unfold Out in H2.
      spliter.
      absurde.
      intro.
      subst C1.
      unfold Out in H3.
      spliter.
      absurde.
    intros.
    spliter.
    apply H7.
    repeat split.
      intro.
      subst A'0.
      unfold Out in H8.
      spliter.
      absurde.
      assumption.
      eapply l6_7.
        apply H8.
      apply l6_6.
      assumption.
      intro.
      subst C'0.
      unfold Out in H9.
      spliter.
      absurde.
      assumption.
      eapply l6_7.
        apply H9.
      apply l6_6.
      assumption.
      intro.
      subst D'.
      unfold Out in H10.
      spliter.
      absurde.
      assumption.
      eapply l6_7.
        apply H10.
      apply l6_6.
      assumption.
      intro.
      subst F'.
      unfold Out in H11.
      spliter.
      absurde.
      assumption.
      eapply l6_7.
        apply H11.
      apply l6_6.
      assumption.
      assumption.
    assumption.
Qed.

Lemma cong3_diff : A B C A' B' C',
 AB Cong_3 A B C A' B' C' A' B'.
Proof.
unfold Cong_3 in ×.
intros.
spliter.
assert_diffs.
auto.
Qed.

Lemma cong3_diff2: A B C A' B' C',
 BC Cong_3 A B C A' B' C' B' C'.
Proof.
unfold Cong_3 in ×.
intros.
spliter.
assert_diffs.
auto.
Qed.

Lemma cong3_conga : A B C A' B' C',
 A B C B
 Cong_3 A B C A' B' C'
 CongA A B C A' B' C'.
Proof.
    intros.
    assert (A' B') by (eauto using cong3_diff).
    assert (B' C') by (eauto using cong3_diff2).
    apply (l11_3_bis A B C A' B' C').
     A. C. A'. C'.
    intuition (auto using out_trivial).
Qed.

Lemma cong3_conga2 : A B C A' B' C' A'' B'' C'',
  Cong_3 A B C A' B' C'
  CongA A B C A'' B'' C''
  CongA A' B' C' A'' B'' C''.
Proof.
    intros.
    unfold CongA in H0.
    spliter.
    ex_and H4 A0.
    ex_and H5 C0.
    ex_and H4 A2.
    ex_and H5 C2.
    unfold Cong_3 in H.
    spliter.
    unfold CongA.
    repeat split.
      intro.
      subst B'.
      apply cong_identity in H.
      subst B.
      absurde.
      intro.
      subst C'.
      apply cong_identity in H14.
      subst C.
      absurde.
      assumption.
      assumption.
    prolong B' A' A1 B'' A''.
    prolong B' C' C1 B'' C''.
     A1.
     C1.
     A2.
     C2.
    repeat split; try assumption.
      eapply cong_transitivity.
        apply H9.
      Cong.
      eapply cong_transitivity.
        apply H11.
      assumption.
    assert (Cong A A0 A' A1).
      eapply cong_transitivity.
        apply H5.
      Cong.
    assert(Cong B A0 B' A1).
      eapply l2_11.
        apply H4.
        apply H15.
        Cong.
      assumption.
    assert (Cong C C0 C' C1).
      eapply cong_transitivity.
        apply H7.
      Cong.
    assert(Cong B C0 B' C1).
      eapply l2_11.
        apply H6.
        apply H17.
        assumption.
      assumption.
    assert(FSC B A A0 C B' A' A1 C').
      unfold FSC.
      repeat split; try assumption.
        unfold Col.
        left.
        assumption.
      Cong.
    assert(Cong A0 C A1 C').
      eapply l4_16.
        apply H23.
      auto.
    apply cong_commutativity.
    assert(Cong C0 A0 C1 A1).
      eapply (l4_16 B C C0 A0 B' C' C1 A1).
        unfold FSC.
        assert_cols.
        repeat split;Cong.
      auto.
    eCong.
Qed.

Lemma conga_diff1 : A B C A' B' C', CongA A B C A' B' C' A B.
Proof.
    intros.
    unfold CongA in H.
    spliter.
    assumption.
Qed.

Lemma conga_diff2 : A B C A' B' C', CongA A B C A' B' C' C B.
Proof.
    intros.
    unfold CongA in H.
    spliter.
    assumption.
Qed.

Lemma conga_diff45 : A B C A' B' C', CongA A B C A' B' C' A' B'.
Proof.
  intros A B C A' B' C' H.
  apply (conga_diff1 A' B' C' A B C); apply conga_sym; auto.
Qed.

Lemma conga_diff56 : A B C A' B' C', CongA A B C A' B' C' C' B'.
Proof.
  intros A B C A' B' C' H.
  apply (conga_diff2 A' B' C' A B C); apply conga_sym; auto.
Qed.

Lemma conga_trans : A B C A' B' C' A'' B'' C'',
  CongA A B C A' B' C' CongA A' B' C' A'' B'' C''
  CongA A B C A'' B'' C''.
Proof.
    intros.
    assert (HH:=H).
    unfold CongA in H.
    spliter.
    ex_and H4 A0.
    ex_and H5 C0.
    ex_and H4 A1.
    ex_and H5 C1.
    assert(A'' B'' C'' B'').
      unfold CongA in H0.
      spliter.
      split; assumption.
    spliter.
    assert(A0 B).
      intro.
      subst A0.
      apply between_identity in H4.
      subst A.
      absurde.
    assert(C0 B).
      intro.
      subst C0.
      apply between_identity in H6.
      subst C.
      absurde.
    assert(A1 B').
      intro.
      subst A1.
      apply between_identity in H8.
      subst A'.
      absurde.
    assert(C1 B').
      intro.
      subst C1.
      apply between_identity in H10.
      subst C'.
      absurde.
    assert(CongA A1 B' C1 A'' B'' C'').
      eapply out_conga.
        apply H0.
        repeat split.
          assumption.
          assumption.
        left.
        assumption.
        repeat split.
          assumption.
          assumption.
        left.
        assumption.
        apply out_trivial.
        assumption.
      apply out_trivial.
      assumption.
    assert (CongA A0 B C0 A' B' C').
      eapply out_conga.
        apply HH.
        apply bet_out.
          assumption.
          assumption.
        assumption.
        apply bet_out.
          assumption.
          assumption.
        assumption.
        apply out_trivial.
        assumption.
      apply out_trivial.
      assumption.
    assert (Cong B A0 B' A1).
      apply cong_right_commutativity.
      eapply l2_11.
        apply H4.
        apply between_symmetry.
        apply H8.
        apply cong_right_commutativity.
        apply cong_symmetry.
        assumption.
      apply cong_right_commutativity.
      assumption.
    assert (Cong B C0 B' C1).
      apply cong_right_commutativity.
      eapply l2_11.
        apply H6.
        apply between_symmetry.
        apply H10.
        apply cong_right_commutativity.
        apply cong_symmetry.
        assumption.
      apply cong_right_commutativity.
      assumption.
    assert (Cong A0 C0 A1 C1).
      apply (l11_4_1) in H20.
      spliter.
      apply H26.
      repeat split.
        assumption.
        assumption.
        left.
        apply between_trivial.
        assumption.
        assumption.
        left.
        apply between_trivial.
        assumption.
        assumption.
        right.
        assumption.
        assumption.
        assumption.
        right.
        assumption.
        assumption.
      assumption.
    assert (Cong_3 A0 B C0 A1 B' C1).
      repeat split.
        apply cong_commutativity.
        assumption.
        assumption.
      assumption.
    apply cong3_symmetry in H24.
    assert( CongA A0 B C0 A'' B'' C'').
      eapply cong3_conga2.
        apply H24.
      assumption.
    eapply out_conga.
      apply H25.
      repeat split.
        assumption.
        assumption.
      right.
      assumption.
      repeat split.
        assumption.
        assumption.
      right.
      assumption.
      apply out_trivial.
      assumption.
    apply out_trivial.
    assumption.
Qed.

Lemma conga_pseudo_refl : A B C,
 A B C B CongA A B C C B A.
Proof.
    intros.
    unfold CongA.
    repeat split; try assumption.
    prolong B A A' B C.
    prolong B C C' B A.
    prolong B A A'' B C.
    prolong B C C'' B A.
     A'.
     C'.
     C''.
     A''.
    repeat split; try assumption.
    assert (A' = A'') by (eauto using (construction_uniqueness B A)).
    subst A''.
    assert (C' = C'') by (eauto using (construction_uniqueness B C)).
    subst C''.
    Cong.
Qed.

Lemma conga_trivial_1 : A B C D,
  AB CD CongA A B A C D C.
Proof.
    intros.
    unfold CongA.
    repeat split; try assumption.
    prolong B A A' D C.
    prolong D C C' B A.
     A'.
     A'.
     C'.
     C'.
    repeat split; try assumption.
    apply cong_trivial_identity.
Qed.

Lemma l11_10 : A B C D E F A' C' D' F',
  CongA A B C D E F Out B A' A Out B C' C Out E D' D Out E F' F
  CongA A' B C' D' E F'.
Proof.
    intros.
    eapply (out_conga A B C D E F); auto using l6_6.
Qed.

Lemma l11_13 : A B C D E F A' D',
 CongA A B C D E F Bet A B A' A' B Bet D E D' D' E CongA A' B C D' E F.
Proof.
    intros.
    unfold CongA in H.
    spliter.
    ex_and H7 A''.
    ex_and H8 C''.
    ex_and H7 D''.
    ex_and H8 F''.
    prolong B A' A0 E D'.
    prolong E D' D0 B A'.
    unfold CongA.
    repeat split; try assumption.
     A0.
     C''.
     D0.
     F''.
    repeat split; try assumption.
    eapply (five_segment_with_def A'' B A0 C'' D'' E D0 F'').
      unfold OFSC.
      repeat split.
        eapply outer_transitivity_between2.
          apply between_symmetry.
          apply H7.
          eapply outer_transitivity_between.
            apply H0.
            assumption.
          auto.
        assumption.
        eapply outer_transitivity_between2.
          apply between_symmetry.
          apply H11.
          eapply outer_transitivity_between.
            apply H2.
            assumption.
          auto.
        assumption.
        apply cong_left_commutativity.
        eapply l2_11.
          apply H7.
          apply between_symmetry.
          apply H11.
          Cong.
        Cong.
        apply cong_right_commutativity.
        eapply l2_11.
          apply H16.
          apply between_symmetry.
          apply H18.
          apply cong_symmetry.
          Cong.
        Cong.
        assumption.
      apply cong_right_commutativity.
      eapply l2_11 with C F;Between;Cong.
    intro.
    subst A''.
    apply between_identity in H7.
    subst A.
    absurde.
Qed.

Lemma conga_right_comm : A B C D E F, CongA A B C D E F CongA A B C F E D.
Proof.
    intros.
    apply conga_trans with D E F.
      apply H.
    unfold CongA in H.
    spliter.
    apply conga_pseudo_refl.
      assumption.
    assumption.
Qed.

Lemma conga_left_comm : A B C D E F, CongA A B C D E F CongA C B A D E F.
Proof.
    intros.
    apply conga_sym.
    apply conga_trans with A B C.
      apply conga_sym.
      apply H.
    unfold CongA in H.
    spliter.
    apply conga_pseudo_refl.
      assumption.
    assumption.
Qed.

Lemma conga_comm : A B C D E F, CongA A B C D E F CongA C B A F E D.
Proof.
    intros.
    apply conga_left_comm.
    apply conga_right_comm.
    assumption.
Qed.

Lemma conga_line : A B C A' B' C',
 A B B C A' B' B' C' Bet A B C Bet A' B' C'
 CongA A B C A' B' C'.
Proof.
    intros.
    assert (AC) by (intro; Between).
    assert (A'C') by (intro; Between).
    spliter.
    prolong B C C0 B' C'.
    prolong B' C' C1 B C.
    prolong B A A0 B' A'.
    prolong B' A' A1 B A.
    unfold CongA.
    repeat split; try assumption.
      auto.
      auto.
     A0.
     C0.
     A1.
     C1.
    repeat split; try assumption.
    apply (l2_11 A0 B C0 A1 B' C1).
      eapply outer_transitivity_between2.
        apply between_symmetry.
        apply H11.
        eapply outer_transitivity_between.
          apply H3.
          assumption.
        assumption.
      assumption.
      eapply outer_transitivity_between2.
        apply between_symmetry.
        apply H13.
        eapply outer_transitivity_between.
          apply H4.
          assumption.
        assumption.
      assumption.
      apply cong_right_commutativity.
      eapply l2_11.
        apply between_symmetry.
        apply H11.
        apply H13.
        apply cong_left_commutativity.
        assumption.
      apply cong_symmetry.
      apply cong_right_commutativity.
      assumption.
    apply cong_right_commutativity.
    eapply l2_11.
      apply H7.
      apply between_symmetry.
      apply H9.
      apply cong_symmetry.
      apply cong_left_commutativity.
      assumption.
    apply cong_right_commutativity.
    assumption.
Qed.

Lemma l11_14 : A B C A' C',
 Bet A B A' A B A' B Bet C B C' B C B C'
 CongA A B C A' B C'.
Proof.
    intros.
    assert (AA') by (intro; Between).
    assert (CC') by (intro; Between).
    spliter.
    assert (CongA A' B C C' B A).
      eapply l11_13.
        eapply conga_pseudo_refl.
          assumption.
        auto.
        assumption.
        assumption.
        assumption.
      auto.
    eapply l11_13.
      apply conga_right_comm.
      apply H7.
      apply between_symmetry.
      assumption.
      assumption.
      assumption.
    assumption.
Qed.

End T11_1.

Section T11_2.

Context `{T2D:Tarski_2D}.

Lemma l11_16 : A B C A' B' C',
 Per A B C A B C B
 Per A' B' C' A' B' C' B'
 CongA A B C A' B' C'.
Proof.
    intros.
    prolong B C C0 B' C'.
    prolong B' C' C1 B C.
    prolong B A A0 B' A'.
    prolong B' A' A1 B A.
    unfold CongA.
    repeat split; try assumption.
     A0.
     C0.
     A1.
     C1.
    repeat split; try assumption.
    eapply (l10_12 A0 B C0 A1 B' C1).
      eapply (per_col _ _ C).
        intro;subst.
        auto.
        apply l8_2.
        eapply (per_col _ _ A).
          auto.
          apply l8_2.
          assumption.
        unfold Col.
        left.
        assumption.
      unfold Col.
      left.
      assumption.
      eapply (per_col _ _ C').
        auto.
        apply l8_2.
        eapply (per_col _ _ A').
          auto.
          apply l8_2.
          assumption.
        unfold Col.
        left.
        assumption.
      unfold Col.
      left.
      assumption.
      apply cong_right_commutativity.
      eapply l2_11.
        apply between_symmetry.
        apply H9.
        apply H11.
        apply cong_left_commutativity.
        assumption.
      apply cong_symmetry.
      apply cong_right_commutativity.
      assumption.
    apply cong_right_commutativity.
    eapply l2_11.
      apply H5.
      apply between_symmetry.
      apply H7.
      apply cong_symmetry.
      apply cong_left_commutativity.
      assumption.
    apply cong_right_commutativity.
    assumption.
Qed.

Lemma l11_17 : A B C A' B' C',
  Per A B C CongA A B C A' B' C' Per A' B' C'.
Proof.
    intros.
    unfold CongA in H0.
    spliter.
    ex_and H4 A0.
    ex_and H5 C0.
    ex_and H4 A1.
    ex_and H5 C1.
    assert (Per A0 B C0).
      eapply (per_col _ _ C).
        auto.
        apply l8_2.
        eapply (per_col _ _ A).
          auto.
          apply l8_2.
          assumption.
        unfold Col.
        left.
        assumption.
      unfold Col.
      left.
      assumption.
    assert(Per A1 B' C1).
      eapply l8_10.
        apply H13.
      repeat split.
        apply cong_right_commutativity.
        eapply l2_11.
          apply between_symmetry.
          apply H4.
          apply H8.
          apply cong_left_commutativity.
          assumption.
        apply cong_symmetry.
        apply cong_right_commutativity.
        assumption.
        assumption.
      apply cong_right_commutativity.
      eapply l2_11.
        apply H6.
        apply between_symmetry.
        apply H10.
        apply cong_left_commutativity.
        apply cong_symmetry.
        apply cong_commutativity.
        assumption.
      apply cong_right_commutativity.
      assumption.
    eapply (per_col _ _ C1).
      intro.
      subst C1.
      apply between_identity in H10.
      subst C'.
      absurde.
      apply l8_2.
      eapply (per_col _ _ A1).
        intro.
        subst A1.
        apply between_identity in H8.
        subst A'.
        absurde.
        apply l8_2.
        assumption.
      unfold Col.
      right; left.
      apply between_symmetry.
      assumption.
    unfold Col.
    right; left.
    apply between_symmetry.
    assumption.
Qed.

Lemma l11_18_1 : A B C D,
  Bet C B D B C B D A B Per A B C CongA A B C A B D.
Proof.
    intros.
    spliter.
    assert (Per A B D).
      eapply per_col.
        apply H0.
        assumption.
      unfold Col.
      right; right.
      apply between_symmetry.
      assumption.
    eapply l11_16; try assumption.
      auto.
    auto.
Qed.

Lemma l11_18_2 : A B C D,
  Bet C B D CongA A B C A B D Per A B C.
Proof.
    intros.
    unfold CongA in H0.
    spliter.
    ex_and H4 A0.
    ex_and H5 C0.
    ex_and H4 A1.
    ex_and H5 D0.
    assert( A0 = A1).
      eapply construction_uniqueness.
        2: apply H4.
        auto.
        apply H5.
        assumption.
      assumption.
    subst A1.
    assert(Per A0 B C0).
      unfold Per.
       D0.
      repeat split.
        eapply outer_transitivity_between2.
          apply between_symmetry.
          apply H6.
          eapply outer_transitivity_between.
            apply H.
            assumption.
          auto.
        assumption.
        eapply l2_11.
          apply between_symmetry.
          apply H6.
          apply H10.
          apply cong_left_commutativity.
          assumption.
        apply cong_symmetry.
        apply cong_right_commutativity.
        assumption.
      assumption.
    eapply (per_col _ _ C0).
      intro.
      subst C0.
      apply between_identity in H6.
      subst C.
      absurde.
      apply l8_2.
      eapply (per_col _ _ A0).
        intro.
        subst A0.
        apply between_identity in H8.
        subst A.
        absurde.
        apply l8_2.
        assumption.
      unfold Col.
      right; left.
      apply between_symmetry.
      assumption.
    unfold Col.
    right; left.
    apply between_symmetry.
    assumption.
Qed.

Lemma cong3_preserves_out : A B C A' B' C',
  Out A B C Cong_3 A B C A' B' C' Out A' B' C'.
Proof.
    intros.
    unfold Out in ×.
    spliter.
    assert(HH:=H0).
    unfold Cong_3 in H0.
    spliter.
    repeat split.
      intro.
      subst A'.
      apply cong_identity in H0.
      subst A.
      absurde.
      intro.
      subst A'.
      apply cong_identity in H3.
      subst A.
      absurde.
    induction H2.
      left.
      eapply l4_6.
        2:apply HH.
      assumption.
    right.
    eapply l4_6.
      apply H2.
    unfold Cong_3.
    repeat split.
      assumption.
      assumption.
    apply cong_commutativity.
    assumption.
Qed.

Lemma l11_21_a : A B C A' B' C', Out B A C CongA A B C A' B' C' Out B' A' C'.
Proof.
    intros.
    unfold CongA in H0.
    spliter.
    ex_and H4 A0.
    ex_and H5 C0.
    ex_and H4 A1.
    ex_and H5 C1.
    assert (Out B A0 C0).
      unfold Out.
      repeat split.
        intro.
        subst A0.
        apply between_identity in H4.
        subst A.
        absurde.
        intro.
        subst C0.
        apply between_identity in H6.
        subst C.
        absurde.
      unfold Out in H.
      spliter.
      induction H14.
        eapply l5_1.
          2: apply H4.
          auto.
        eapply between_exchange4.
          apply H14.
        assumption.
      eapply l5_1.
        3: apply H6.
        auto.
      eapply between_exchange4.
        apply H14.
      assumption.
    assert (Out B' A1 C1).
      eapply cong3_preserves_out.
        apply H13.
      unfold Cong_3.
      repeat split.
        apply cong_right_commutativity.
        eapply l2_11.
          apply H4.
          apply between_symmetry.
          apply H8.
          apply cong_symmetry.
          apply cong_left_commutativity.
          assumption.
        apply cong_right_commutativity.
        assumption; apply H8.
        apply cong_right_commutativity.
        eapply l2_11.
          apply H6.
          apply between_symmetry.
          apply H10.
          apply cong_symmetry.
          apply cong_left_commutativity.
          assumption.
        apply cong_right_commutativity.
        assumption.
      assumption.
    eapply l6_7.
      apply l6_6.
      eapply l6_7.
        apply H14.
      eapply l6_7.
        apply l6_6.
        apply H14.
      unfold Out.
      repeat split.
        intro.
        subst A1.
        unfold Out in H14.
        spliter.
        absurde.
        assumption.
      right.
      assumption.
    eapply l6_7.
      apply H14.
    unfold Out.
    repeat split.
      intro.
      subst C1.
      unfold Out in H14.
      spliter.
      absurde.
      assumption.
    right.
    assumption.
Qed.

Lemma l11_21_b : A B C A' B' C',
 Out B A C Out B' A' C' CongA A B C A' B' C'.
Proof.
    intros.
    prolong A B A0 A B.
    prolong C B C0 B C.
    prolong A' B' A1 A' B'.
    prolong C' B' C1 B' C'.
    eapply l11_13.
      eapply conga_line.
        5: apply between_symmetry.
        5: apply H3.
        5: apply between_symmetry.
        5: apply H7.
        intro.
        subst C0.
        apply cong_symmetry in H4.
        apply cong_identity in H4.
        subst C.
        unfold Out in H.
        spliter.
        absurde.
        intro.
        subst C.
        unfold Out in H.
        spliter.
        absurde.
        intro.
        subst C1.
        apply cong_symmetry in H8.
        apply cong_identity in H8.
        subst C'.
        unfold Out in H0.
        spliter.
        absurde.
        intro.
        subst C'.
        unfold Out in H0.
        spliter.
        absurde.
      unfold Out in H0.
      spliter.
      auto.
      unfold Out in H.
      spliter.
      induction H12.
        eapply between_inner_transitivity.
          apply between_symmetry.
          apply H3.
        assumption.
      eapply outer_transitivity_between.
        apply between_symmetry.
        apply H3.
        assumption.
      auto.
      unfold Out in H.
      spliter.
      assumption.
      unfold Out in H0.
      spliter.
      induction H10.
        eapply between_inner_transitivity.
          apply between_symmetry.
          apply H7.
        assumption.
      eapply outer_transitivity_between.
        apply between_symmetry.
        apply H7.
        assumption.
      auto.
    unfold Out in H0.
    spliter.
    assumption.
Qed.

Lemma l11_22_aux : A B C C',
 CongA A B C A B C' Out B C C' TS A B C C'.
Proof.
    intros.
    unfold CongA in H.
    spliter.
    ex_and H3 A0.
    ex_and H4 C0.
    ex_and H3 A1.
    ex_and H4 C1.
    assert (A0=A1).
      eapply construction_uniqueness.
        3:apply H4.
        2:apply H3.
        auto.
        assumption.
      assumption.
    subst A1.
    induction (eq_dec_points C0 C1).
      subst C1.
      left.
      unfold Out.
      repeat split; try assumption.
      eapply l5_3.
        apply H5.
      assumption.
    right.
    assert( M, Midpoint M C0 C1).
      apply midpoint_existence.
    ex_and H13 M.
    assert(Cong B C0 B C1).
      apply cong_right_commutativity.
      eapply l2_11.
        apply H5.
        apply between_symmetry.
        apply H9.
        apply cong_symmetry.
        apply cong_left_commutativity.
        assumption.
      apply cong_right_commutativity.
      assumption.
    assert(Per A0 M C0).
      unfold Per.
       C1.
      split.
        assumption.
      assumption.
    assert(Per B M C0).
      unfold Per.
       C1.
      split.
        assumption.
      assumption.
    assert(Per A0 M C1).
      unfold Per.
       C0.
      split.
        apply l7_2.
        assumption.
      apply cong_symmetry.
      assumption.
    assert(Per B M C1).
      unfold Per.
       C0.
      split.
        apply l7_2.
        assumption.
      apply cong_symmetry.
      assumption.
    assert (B A0).
      intro.
      subst A0.
      apply between_identity in H7.
      subst A.
      absurde.
    assert (Cong A C0 A C1).
      eapply (l4_2 B A A0 C0 B A A0 C1).
      unfold IFSC.
      repeat split; try assumption.
        apply cong_reflexivity.
      apply cong_reflexivity.
    assert (Per A M C0).
      unfold Per.
       C1.
      split.
        assumption.
      assumption.
    assert (Per A M C1).
      unfold Per.
       C0.
      split.
        apply l7_2.
        assumption.
      apply cong_symmetry.
      assumption.
    assert(Col B A M).
      eapply per_per_col.
        apply H16.
        intro.
        subst M.
        apply is_midpoint_id in H14.
        contradiction.
      assumption.
    induction(eq_dec_points B M).
      subst M.
      assert(¬Col A B C).
        eapply per_not_col.
          assumption.
          auto.
        eapply per_col.
          2:apply H22.
          intro.
          subst C1.
          apply l7_2 in H14.
          apply is_midpoint_id in H14.
          subst C0.
          absurde.
        assert(Bet C B C1).
          eapply between_exchange3.
            apply between_symmetry.
            apply H5.
          apply midpoint_bet.
          assumption.
        unfold Col.
        right; right.
        assumption.
      assert(¬Col A B C').
        eapply per_not_col.
          assumption.
          auto.
        eapply per_col.
          2:apply H22.
          intro.
          subst C1.
          apply l7_2 in H14.
          apply is_midpoint_id in H14.
          subst C0.
          absurde.
        assert(Bet C' B C0).
          eapply between_exchange3.
            apply between_symmetry.
            apply H9.
          apply midpoint_bet.
          apply l7_2.
          assumption.
        unfold Col.
        right; left.
        apply between_symmetry.
        assumption.
      unfold TS.
      repeat split.
        Col.
        Col.
       B.
      split.
        Col.
      apply between_symmetry.
      eapply between_exchange3.
        apply between_symmetry.
        apply H9.
      apply between_symmetry.
      eapply between_exchange3.
        apply between_symmetry.
        apply H5.
      apply midpoint_bet.
      assumption.
    assert(TS B M C0 C1).
      unfold TS.
      repeat split.
        intro.
        apply per_not_col in H16.
          apply H16.
          apply col_permutation_1.
          assumption.
          assumption.
        intro.
        subst C0.
        apply is_midpoint_id in H14.
        subst C1.
        absurde.
        intro.
        apply per_not_col in H18.
          apply H18.
          Col.
          assumption.
        intro.
        subst C1.
        apply l7_2 in H14.
        apply is_midpoint_id in H14.
        subst C0.
        absurde.
       M.
      split.
        apply col_trivial_3.
      apply midpoint_bet.
      assumption.
    apply (col_two_sides _ _ A) in H25.
      apply invert_two_sides in H25.
      assert(TS A B C C1).
        eapply l9_5.
          apply H25.
          apply col_trivial_3.
        unfold Out.
        repeat split.
          intro.
          subst C0.
          apply cong_symmetry in H13.
          apply cong_identity in H13.
          subst C1.
          absurde.
          assumption.
        right.
        assumption.
      apply l9_2.
      eapply l9_5.
        apply l9_2.
        apply H26.
        apply col_trivial_3.
      unfold Out.
      repeat split.
        intro.
        subst C1.
        apply cong_identity in H13.
        subst C0.
        absurde.
        intro.
        subst C'.
        apply cong_identity in H6.
        subst C0.
        absurde.
      right.
      assumption.
      Col.
    auto.
Qed.

Lemma cong2_conga_cong : A B C A' B' C',
 CongA A B C A' B' C' Cong A B A' B' Cong B C B' C'
 Cong A C A' C'.
Proof.
    intros.
    unfold CongA in H.
    spliter.
    ex_and H5 A0.
    ex_and H6 C0.
    ex_and H5 A1.
    ex_and H6 C1.
    assert(Cong A C0 A' C1).
      eapply (l4_2 B A A0 C0 B' A' A1 C1).
      repeat split; try assumption.
        eapply l2_11.
          apply H5.
          apply H9.
          apply cong_commutativity.
          assumption.
        eapply cong_transitivity.
          apply H6.
        apply cong_commutativity.
        apply cong_symmetry.
        eapply cong_transitivity.
          2: apply H0.
        apply cong_commutativity.
        assumption.
        eapply cong_transitivity.
          apply H6.
        apply cong_commutativity.
        apply cong_symmetry.
        eapply cong_transitivity.
          2: apply H0.
        apply cong_commutativity.
        assumption.
      eapply cong_transitivity.
        eapply l2_11.
          apply H7.
          apply H11.
          assumption.
        eapply cong_transitivity.
          apply H8.
        apply cong_symmetry.
        eapply cong_transitivity.
          apply H12.
        assumption.
      apply cong_reflexivity.
    apply cong_commutativity.
    eapply (l4_2 B C C0 A B' C' C1 A').
    repeat split; try assumption.
      eapply l2_11.
        apply H7.
        apply H11.
        assumption.
      eapply cong_transitivity.
        apply H8.
      eapply cong_transitivity.
        apply cong_symmetry.
        apply H1.
      apply cong_symmetry.
      assumption.
      eapply cong_transitivity.
        apply H8.
      eapply cong_transitivity.
        apply cong_symmetry.
        apply H1.
      apply cong_symmetry.
      assumption.
      apply cong_commutativity.
      assumption.
    apply cong_commutativity.
    assumption.
Qed.

Lemma segment_construction_3 : A B X Y, A B X Y C, Out A B C Cong A C X Y.
Proof.
    intros.
    assert( C ,(Bet A B C Bet A C B) Cong A C X Y).
      apply segment_construction_2.
      auto.
    ex_and H1 C.
     C.
    repeat split.
      auto.
      intro.
      subst C.
      apply cong_symmetry in H2.
      apply cong_identity in H2.
      contradiction.
      assumption.
    assumption.
Qed.

Lemma ex_per_cong : A B C D X Y,
 A B X Y Col A B C ¬Col A B D
  P, Per P C A Cong P C X Y OS A B P D.
Proof.
    intros.
    assert ( D', TS A B D D').
      apply l9_10.
        assumption.
      intro.
      apply H2.
      apply col_permutation_1.
      assumption.
    ex_and H3 D'.
    induction (eq_dec_points A C).
      subst C.
      assert( P, T, Perp A B P A Col A B T Bet D' T P).
        apply l8_21.
        assumption.
      ex_and H3 P.
      ex_and H5 T.
      assert( P0, Out A P P0 Cong A P0 X Y).
        apply segment_construction_3.
          unfold Perp in H3.
          unfold Perp_at in H3.
          ex_and H3 Z.
          auto.
        assumption.
      ex_and H7 P0.
       P0.
      repeat split.
        eapply l8_5.
        apply cong_left_commutativity.
        assumption.
      unfold OS.
       D'.
      split.
        eapply l9_5.
          3: apply H7.
          unfold TS.
          repeat split.
            assert(¬Col A B P ¬Col P A B).
              intro.
              intro.
              apply H9.
              apply col_permutation_1.
              assumption.
            apply H9.
            eapply perp_not_col.
            assumption.
            unfold TS in H4.
            spliter.
            assumption.
           T.
          split.
            apply col_permutation_2.
            assumption.
          apply between_symmetry.
          assumption.
        apply col_trivial_1.
      assumption.
    assert( P, T, Perp C A P C Col C A T Bet D' T P).
      apply l8_21.
      auto.
    ex_and H5 P.
    ex_and H6 T.
    assert (HH5 := H5).
    assert( P0, Out C P P0 Cong C P0 X Y).
      apply segment_construction_3.
        unfold Perp in H5.
        unfold Perp_at in H5.
        ex_and H5 Z.
        auto.
      assumption.
    ex_and H8 P0.
     P0.
    repeat split.
      eapply perp_per_1 in H5.
        eapply l8_2.
        eapply per_col.
          2: apply H5.
          unfold Perp in HH5.
          unfold Perp_at in HH5.
          ex_and HH5 Z.
          auto.
        apply out_col.
        assumption.
      auto.
      apply cong_left_commutativity.
      assumption.
    unfold OS.
     D'.
    split.
      eapply l9_5.
        3: apply H8.
        unfold TS.
        repeat split.
          assert(¬Col C A P ¬Col P A B).
            intro.
            intro.
            apply H10.
            apply col_permutation_2.
            eapply col_transitivity_1.
              apply H.
              apply col_permutation_1.
              assumption.
            assumption.
          apply H10.
          eapply perp_not_col.
          assumption.
          unfold TS in H4.
          spliter.
          assumption.
         T.
        split.
          apply col_permutation_2.
          eapply col_transitivity_1.
            apply H3.
            apply col_permutation_5.
            assumption.
          apply col_permutation_4.
          assumption.
        apply between_symmetry.
        assumption.
      apply col_permutation_2.
      assumption.
    assumption.
Qed.

Lemma angle_construction_1 : A B C A' B' P,
 ¬Col A B C ¬Col A' B' P
  C', CongA A B C A' B' C' OS A' B' C' P.
Proof.
    intros.
    assert ( C0, Col B A C0 Perp B A C C0).
      eapply l8_18_existence.
      intro.
      apply H.
      apply col_permutation_4.
      assumption.
    ex_and H1 C0.
    induction(eq_dec_points B C0).
      subst C0.
      assert ( C', Per C' B' A' Cong C' B' C B OS A' B' C' P).
        apply ex_per_cong.
          intro.
          subst A'.
          apply H0.
          apply col_trivial_1.
          intro.
          subst C.
          apply H.
          apply col_trivial_2.
          apply col_trivial_2.
        assumption.
      ex_and H3 C'.
       C'.
      split.
        eapply l11_16.
          apply perp_perp_in in H2.
          apply perp_in_comm in H2.
          apply perp_in_per in H2.
          assumption.
          intro.
          subst A.
          apply H.
          apply col_trivial_1.
          intro.
          subst C.
          apply H.
          apply col_trivial_2.
          apply l8_2.
          assumption.
          intro.
          subst A'.
          apply H0.
          apply col_trivial_1.
        intro.
        subst C'.
        apply cong_symmetry in H4.
        apply cong_identity in H4.
        subst C.
        apply H.
        apply col_trivial_2.
      assumption.
    induction (out_dec B A C0).
      assert ( C0', Out B' A' C0' Cong B' C0' B C0).
        eapply segment_construction_3.
          intro.
          subst A'.
          apply H0.
          apply col_trivial_1.
        assert (Perp_at C0 C0 C B C0).
          eapply perp_perp_in.
          apply perp_sym.
          eapply perp_col.
            assumption.
            apply perp_right_comm.
            apply H2.
          assumption.
        assumption.
      ex_and H5 C0'.
      assert ( C' , Per C' C0' B' Cong C' C0' C C0 OS B' C0' C' P).
        apply ex_per_cong.
          intro.
          subst C0'.
          unfold Out in H5.
          spliter.
          absurde.
          intro.
          subst C0.
          unfold Perp in H2.
          ex_and H2 X.
          unfold Perp_at in H7.
          spliter.
          absurde.
          apply col_trivial_2.
        intro.
        apply H0.
        apply col_permutation_2.
        eapply (col_transitivity_1 _ C0').
          intro.
          subst C0'.
          unfold Out in H5.
          spliter.
          absurde.
          assumption.
        apply out_col.
        apply l6_6.
        assumption.
      ex_and H7 C'.
      assert (Cong_3 C0 B C C0' B' C').
        unfold Cong_3.
        repeat split.
          apply cong_symmetry.
          apply cong_commutativity.
          assumption.
          apply cong_symmetry.
          apply cong_commutativity.
          assumption.
        eapply (l10_12 _ C0).
          assert(Perp B C0 C C0 ).
            eapply perp_col.
              intro.
              subst C0.
              apply perp_distinct in H2.
              spliter.
              absurde.
              apply H2.
            assumption.
          apply perp_left_comm in H10.
          apply perp_perp_in in H10.
          apply perp_in_per.
          apply perp_in_comm.
          assumption.
          apply l8_2.
          apply H7.
          apply cong_symmetry.
          assumption.
        apply cong_symmetry.
        apply cong_commutativity.
        assumption.
       C'.
      split.
        eapply (l11_10 C0 _ _ C0').
          apply cong3_conga.
            3: apply H10.
            intro.
            subst C0.
            absurde.
          intro.
          subst C.
          apply H.
          apply col_trivial_2.
          assumption.
          apply out_trivial.
          intro.
          subst C.
          apply H.
          apply col_trivial_2.
          assumption.
        apply out_trivial.
        intro.
        subst C'.
        apply l8_8 in H7.
        subst C0'.
        unfold Out in H5.
        spliter.
        absurde.
      apply invert_one_side.
      eapply col_one_side.
        3: apply H9.
        apply out_col.
        apply l6_6.
        assumption.
      intro.
      subst A'.
      apply H0.
      apply col_trivial_1.
    apply not_out_bet in H4.
      prolong A' B' C0' B C0.
      assert ( C' , Per C' C0' B' Cong C' C0' C C0 OS B' C0' C' P).
        apply ex_per_cong.
          intro.
          subst C0'.
          apply cong_symmetry in H6.
          apply cong_identity in H6.
          subst C0.
          absurde.
          intro.
          subst C0.
          apply perp_distinct in H2.
          spliter.
          absurde.
          apply col_trivial_2.
        intro.
        apply H0.
        apply col_permutation_2.
        eapply col_transitivity_1.
          2:apply H7.
          intro.
          subst C0'.
          apply cong_symmetry in H6.
          apply cong_identity in H6.
          subst C0.
          absurde.
        unfold Col.
        right; right.
        assumption.
      ex_and H7 C'.
       C'.
      split.
        assert (Cong_3 C0 B C C0' B' C').
          repeat split.
            apply cong_symmetry.
            apply cong_commutativity.
            assumption.
            apply cong_symmetry.
            apply cong_commutativity.
            assumption.
          apply cong_commutativity.
          eapply (l10_12 _ C0 _ _ C0').
            assert(Perp B C0 C C0 ).
              eapply perp_col.
                intro.
                subst C0.
                apply perp_distinct in H2.
                spliter.
                absurde.
                apply H2.
              assumption.
            apply perp_left_comm in H10.
            apply perp_perp_in in H10.
            apply perp_in_per.
            apply perp_in_sym.
            assumption.
            assumption.
            apply cong_symmetry.
            assumption.
          apply cong_symmetry.
          apply cong_commutativity.
          assumption.
        eapply l11_13.
          apply cong3_conga.
            3: apply H10.
            auto.
          intro.
          subst C.
          apply H.
          apply col_trivial_2.
          apply between_symmetry.
          assumption.
          intro.
          subst A.
          apply H.
          apply col_trivial_1.
          apply between_symmetry.
          assumption.
        intro.
        subst A'.
        apply H0.
        apply col_trivial_1.
      apply invert_one_side.
      eapply col_one_side.
        3: apply H9.
        unfold Col.
        right; right.
        assumption.
      intro.
      subst A'.
      apply H0.
      apply col_trivial_1.
    apply col_permutation_4.
    assumption.
Qed.

Lemma angle_construction_2 : A B C A' B' P,
 A B A C B C A' B' ¬Col A' B' P
  C', CongA A B C A' B' C' (OS A' B' C' P Col A' B' C').
Proof.
    intros.
    spliter.
    induction (Col_dec A B C).
      induction (out_dec B A C).
         A'.
        split.
          assert(CongA A B A A B C).
            eapply l11_10.
              apply conga_refl.
                3: apply H5.
              auto.
              2: apply H5.
              auto.
              assumption.
            apply out_trivial.
            auto.
          assert (CongA A B A A' B' A').
            apply conga_trivial_1.
              assumption.
            assumption.
          apply conga_sym.
          eapply conga_trans.
            apply conga_sym.
            apply H7.
          assumption.
        right.
        apply col_trivial_3.
      apply not_out_bet in H5.
        prolong A' B' C' A' B'.
         C'.
        split.
          eapply conga_line; try assumption.
            intro.
            subst C'.
            apply cong_symmetry in H7.
            apply cong_identity in H7.
            subst A'.
            absurde.
        right.
        unfold Col.
        left.
        assumption.
      assumption.
    assert( C' , CongA A B C A' B' C' OS A' B' C' P).
      apply angle_construction_1.
        assumption.
      assumption.
    ex_and H5 C'.
     C'.
    split.
      assumption.
    left.
    assumption.
Qed.

Lemma ex_conga_ts : A B C A' B' P,
    ¬ Col A B C
    ¬ Col A' B' P
     C' : Tpoint, CongA A B C A' B' C' TS A' B' C' P.
Proof.
  intros A B C A' B' P HNCol HNCol'.
  assert (HP' : P', Midpoint A' P P') by (apply symmetric_point_construction).
  destruct HP' as [P' HMid].
  assert (¬ Col A' B' P').
  { intro HCol.
    apply HNCol'.
    assert (Col A' P P') by (apply midpoint_col; auto).
    apply (col3 A' P'); Col.
    intro; treat_equalities; Col.
  }
  assert (HC' : C', CongA A B C A' B' C' OS A' B' C' P').
  apply (angle_construction_1 A B C A' B' P'); auto.
  destruct HC' as [C' [HConga HOne]].
   C'.
  split; auto.
  apply (l9_8_2 A' B' P'); Side.
  split; Col; split; Col.
   A'.
  split; Col.
  destruct HMid; Between.
Qed.

Lemma l11_15 : A B C D E P, ¬ Col A B C ¬ Col D E P
  F, CongA A B C D E F OS E D F P
          ( F1 F2, ((CongA A B C D E F1 OS E D F1 P)
                          (CongA A B C D E F2 OS E D F2 P)) Out E F1 F2).
Proof.
    intros.
    assert( F, CongA A B C D E F OS D E F P)
      by (apply angle_construction_1; assumption).
    ex_and H1 F.
     F.
    split.
      assumption.
    split.
      apply invert_one_side.
      assumption.
    intros.
    spliter.
    assert(Out E F1 F2 TS D E F1 F2).
      apply l11_22_aux.
      eapply conga_trans.
        apply conga_sym.
        apply H3.
      assumption.
    induction H7.
      assumption.
    assert(OS E D F1 F2).
      eapply one_side_transitivity.
        apply H6.
      apply one_side_symmetry.
      assumption.
    apply l9_9_bis in H8.
    apply invert_two_sides in H7.
    contradiction.
Qed.

Lemma l11_19 : A B P1 P2,
  Per A B P1 Per A B P2 OS A B P1 P2
  Out B P1 P2.
Proof.
    intros.
    induction (Col_dec A B P1).
      induction (l8_9 A B P1 H H2).
        subst.
        unfold OS in ×.
        decompose [ex and] H1.
        unfold TS in ×.
        intuition.
      subst.
      unfold OS in ×.
      decompose [ex and] H1.
      unfold TS in ×.
      spliter.
      assert (Col B A B) by Col.
      intuition.
    induction (Col_dec A B P2).
      induction (l8_9 A B P2 H0 ).
        subst.
        unfold OS in ×.
        decompose [ex and] H1.
        unfold TS in ×.
        intuition.
        subst.
        unfold OS in ×.
        decompose [ex and] H1.
        unfold TS in ×.
        spliter.
        assert (Col B A B) by Col.
        intuition.
      Col.
    assert (T:=l11_15 A B P1 A B P2 H2 H3).
    decompose [ex and] T.
    apply H7.
    split.
      split.
        apply conga_refl.
          intro;subst;Col.
        intro;subst;Col.
      apply invert_one_side;auto.
    split.
      apply l11_16;try assumption.
        intro;subst;Col.
        intro;subst;Col.
        intro;subst;Col.
      intro;subst;Col.
    apply one_side_reflexivity.
    Col.
Qed.

Lemma l11_22_bet :
  A B C P A' B' C' P',
  Bet A B C
  TS P' B' A' C'
  CongA A B P A' B' P' CongA P B C P' B' C'
  Bet A' B' C'.
Proof.
    intros.
    spliter.
    prolong A' B' C'' B C.
    assert(CongA C B P C'' B' P').
      eapply l11_13.
        2:apply H.
        apply H1.
        unfold CongA in H2.
        spliter.
        assumption.
        assumption.
      intro.
      subst C''.
      apply cong_symmetry in H4.
      apply cong_identity in H4.
      subst C.
      unfold CongA in H2.
      spliter.
      absurde.
    assert (CongA C'' B' P' C' B' P').
      eapply conga_trans.
        apply conga_sym.
        apply H5.
      apply conga_comm.
      assumption.
    assert(Out B' C' C'' TS P' B' C' C'').
      apply l11_22_aux.
      apply conga_comm.
      apply conga_sym.
      assumption.
    induction H7.
      unfold Out in H7.
      spliter.
      induction H9.
        eapply between_inner_transitivity.
          apply H3.
        assumption.
      eapply outer_transitivity_between.
        apply H3.
        assumption.
      auto.
    induction (Col_dec C' B' P').
      unfold TS in H7.
      spliter.
      apply False_ind.
      apply H7.
      apply col_permutation_5.
      assumption.
    assert (B' P').
      intro.
      subst P'.
      apply H8.
      apply col_trivial_2.
    assert (TS B' P' A' C'').
      unfold TS.
      repeat split.
        unfold TS in H0.
        spliter.
        intro.
        apply H0.
        apply col_permutation_5.
        assumption.
        intro.
        unfold TS in H7.
        spliter.
        apply H11.
        apply col_permutation_5.
        assumption.
       B'.
      split.
        apply col_trivial_1.
      assumption.
    assert (OS B' P' C' C'').
      eapply l9_8_1.
        apply l9_2.
        apply invert_two_sides.
        apply H0.
      apply l9_2.
      assumption.
    apply l9_9_bis in H11.
    apply invert_two_sides in H7.
    contradiction.
Qed.

Lemma l11_22a :
  A B C P A' B' C' P',
 TS B P A C TS B' P' A' C'
 CongA A B P A' B' P' CongA P B C P' B' C'
 CongA A B C A' B' C'.
Proof.
    intros.
    spliter.
    assert (A B A' B' P B P' B' C B C' B').
      unfold CongA in ×.
      spliter.
      repeat split; assumption.
    assert(A C A' C').
      unfold TS in ×.
      spliter.
      ex_and H12 T.
      ex_and H10 T'.
      split.
        intro.
        subst C.
        apply between_identity in H13.
        subst T.
        contradiction.
      intro.
      subst C'.
      apply between_identity in H14.
      subst T'.
      contradiction.
    spliter.
    assert( A'', Out B' A' A'' Cong B' A'' B A).
      eapply segment_construction_3; auto.
    ex_and H11 A''.
    unfold TS in H.
    assert (¬ Col A B P).
      spliter.
      assumption.
    spliter.
    ex_and H15 T.
    induction (eq_dec_points B T).
      subst T.
      assert(Bet A' B' C').
        eapply l11_22_bet.
          apply H16.
          apply invert_two_sides.
          apply H0.
        split.
          apply H1.
        assumption.
      apply conga_line.
        assumption.
        auto.
        assumption.
        auto.
      assumption.
      assumption.
    induction(bet_dec P B T).
      assert( T'', Col B' P' T'' (Out B' P' T'' Out B P T) Cong B' T'' B T).
        prolong P' B' T'' B T.
         T''.
        split.
          unfold Col.
          right; right.
          apply between_symmetry.
          assumption.
        split.
          split.
            intro.
            assert(Bet P' B' T'' Out B' P' T'').
              split; assumption.
            apply (not_bet_and_out _ _ _)in H22.
            contradiction.
          intro.
          assert(Bet P B T Out B P T).
            split; assumption.
          apply (not_bet_and_out _ _ _)in H22.
          contradiction.
        assumption.
      ex_and H19 T''.
      destruct H20.
      assert (B' T'').
        intro.
        subst T''.
        apply cong_symmetry in H21.
        apply cong_identity in H21.
        contradiction.
      assert( C'', Bet A'' T'' C'' Cong T'' C'' T C).
        prolong A'' T'' C'' T C.
         C''.
        split; assumption.
      ex_and H24 C''.
      assert(CongA A B T A' B' T'').
        apply conga_comm.
        eapply l11_13.
          apply conga_comm.
          apply H1.
          assumption.
          auto.
          eapply out_to_bet.
            apply col_permutation_4.
            assumption.
            split.
              apply H22.
            assumption.
          assumption.
        auto.
      assert(CongA A B T A'' B' T'').
        eapply l11_10.
          apply H26.
          apply out_trivial.
          auto.
          apply out_trivial.
          auto.
          apply l6_6.
          assumption.
        apply out_trivial.
        auto.
      assert(Cong A T A'' T'').
        assert(HH:= l11_4_1 A B T A'' B' T'' H27).
        spliter.
        apply H32.
        split.
          apply out_trivial.
          auto.
        split.
          apply out_trivial.
          auto.
        split.
          apply out_trivial.
          intro.
          subst A''.
          absurde.
        split.
          apply out_trivial.
          assumption.
        split.
          apply cong_symmetry.
          assumption.
        apply cong_symmetry.
        assumption.
      assert(Cong A C A'' C'').
        eapply l2_11.
          apply H16.
          apply H24.
          assumption.
        apply cong_symmetry.
        assumption.
      assert(Cong C B C'' B').
        eapply (five_segment).
          5:apply H16.
          5: apply H24.
          assumption.
          apply cong_symmetry.
          assumption.
          apply cong_symmetry.
          apply cong_commutativity.
          assumption.
          apply cong_symmetry.
          apply cong_commutativity.
          assumption.
        intro.
        subst T.
        apply H13.
        assumption.
      assert(CongA A B C A'' B' C'').
        apply cong3_conga.
          assumption.
          assumption.
        repeat split.
          apply cong_commutativity.
          apply cong_symmetry.
          assumption.
          assumption.
        apply cong_commutativity.
        assumption.
      assert(CongA C B T C'' B' T'').
        apply cong3_conga.
          assumption.
          auto.
        repeat split.
          assumption.
          apply cong_symmetry.
          apply cong_commutativity.
          assumption.
        apply cong_symmetry.
        assumption.
      assert (CongA P B C P' B' C'').
        eapply l11_13.
          apply conga_comm.
          apply H32.
          apply between_symmetry.
          assumption.
          assumption.
          apply between_symmetry.
          eapply out_to_bet.
            eapply col_permutation_4.
            assumption.
            split.
              apply H22.
            assumption.
          assumption.
        assumption.
      assert(CongA P' B' C' P' B' C'').
        eapply conga_trans.
          apply conga_sym.
          apply H2.
        assumption.
      assert(Out B' C' C'' TS P' B' C' C'').
        apply l11_22_aux.
        assumption.
      induction H35.
        eapply l11_10.
          apply H31.
          apply out_trivial.
          auto.
          apply out_trivial.
          auto.
          assumption.
        assumption.
      assert(TS B' P' A'' C').
        apply l9_2.
        eapply l9_5.
          eapply l9_2.
          eapply l9_5.
            apply H0.
            apply col_trivial_1.
          assumption.
          apply col_trivial_1.
        apply out_trivial.
        auto.
      apply invert_two_sides in H35.
      apply l9_2 in H35.
      assert(OS B' P' A'' C'').
        unfold OS.
         C'.
        split; assumption.
      assert (TS B' P' A'' C'').
        unfold TS.
        repeat split.
          intro.
          unfold TS in H0.
          assert (¬ Col A' B' P').
            spliter.
            assumption.
          spliter.
          apply H39.
          apply col_permutation_2.
          eapply (col_transitivity_1 _ A'').
            intro.
            subst A''.
            unfold Out in H11.
            spliter.
            absurde.
            apply col_permutation_4.
            assumption.
          apply out_col in H11.
          apply col_permutation_5.
          assumption.
          intro.
          unfold TS in H35.
          spliter.
          apply H35.
          assumption.
         T''.
        split.
          apply col_permutation_2.
          assumption.
        assumption.
      apply l9_9 in H38.
      contradiction.
    apply not_bet_out in H18.
      assert( T'', Col B' P' T'' (Out B' P' T'' Out B P T) Cong B' T'' B T).
        assert ( T'', Out B' P' T'' Cong B' T'' B T).
          apply segment_construction_3.
            auto.
          assumption.
        ex_and H19 T''.
         T''.
        split.
          apply out_col in H19.
          assumption.
        split.
          split.
            intro.
            assumption.
          intro.
          assumption.
        assumption.
      ex_and H19 T''.
      destruct H20.
      assert (B' T'').
        intro.
        subst T''.
        apply cong_symmetry in H21.
        apply cong_identity in H21.
        contradiction.
      assert( C'', Bet A'' T'' C'' Cong T'' C'' T C).
        prolong A'' T'' C'' T C.
         C''.
        split; assumption.
      ex_and H24 C''.
      assert(CongA A B T A' B' T'').
        eapply l11_10.
          apply H1.
          apply out_trivial.
          auto.
          apply l6_6.
          assumption.
          apply out_trivial.
          auto.
        apply l6_6.
        apply H22.
        assumption.
      assert(CongA A B T A'' B' T'').
        eapply l11_10.
          apply H26.
          apply out_trivial.
          auto.
          apply out_trivial.
          auto.
          apply l6_6.
          assumption.
        apply out_trivial.
        auto.
      assert(Cong A T A'' T'').
        assert(HH:= l11_4_1 A B T A'' B' T'' H27).
        spliter.
        apply H32.
        split.
          apply out_trivial.
          auto.
        split.
          apply out_trivial.
          assumption.
        split.
          apply out_trivial.
          intro.
          subst A''.
          absurde.
        split.
          apply out_trivial.
          assumption.
        split.
          apply cong_symmetry.
          assumption.
        apply cong_symmetry.
        assumption.
      assert(Cong A C A'' C'').
        eapply l2_11.
          apply H16.
          apply H24.
          assumption.
        apply cong_symmetry.
        assumption.
      assert(Cong C B C'' B').
        eapply (five_segment).
          5:apply H16.
          5: apply H24.
          assumption.
          apply cong_symmetry.
          assumption.
          apply cong_symmetry.
          apply cong_commutativity.
          assumption.
          apply cong_symmetry.
          apply cong_commutativity.
          assumption.
        intro.
        apply H13.
        subst T.
        assumption.
      assert(CongA A B C A'' B' C'').
        apply cong3_conga.
          assumption.
          assumption.
        repeat split.
          apply cong_commutativity.
          apply cong_symmetry.
          assumption.
          assumption.
        apply cong_commutativity.
        assumption.
      assert(CongA C B T C'' B' T'').
        apply cong3_conga.
          assumption.
          auto.
        repeat split.
          assumption.
          apply cong_symmetry.
          apply cong_commutativity.
          assumption.
        apply cong_symmetry.
        assumption.
      eapply l11_10.
        apply H31.
        apply out_trivial.
        auto.
        apply out_trivial.
        auto.
        assumption.
      assert(Out B' C' C'' TS P' B' C' C'').
        apply l11_22_aux.
        apply conga_comm.
        eapply conga_trans.
          apply conga_comm.
          apply conga_sym.
          apply H2.
        eapply l11_10.
          apply H32.
          apply out_trivial.
          auto.
          assumption.
          apply out_trivial.
          intro.
          subst C''.
          apply cong_identity in H30.
          contradiction.
        apply H22.
        assumption.
      induction H33.
        assumption.
      assert(TS B' P' A'' C').
        apply l9_2.
        eapply l9_5.
          eapply l9_2.
          eapply l9_5.
            apply H0.
            apply col_trivial_1.
          assumption.
          apply col_trivial_1.
        apply out_trivial.
        auto.
      assert(OS B' P' A'' C'').
        unfold OS.
         C'.
        split.
          assumption.
        apply invert_two_sides in H33.
        apply l9_2 in H33.
        assumption.
      assert (TS B' P' A'' C'').
        unfold TS.
        repeat split.
          intro.
          unfold TS in H34.
          spliter.
          apply H34.
          assumption.
          intro.
          unfold TS in H33.
          spliter.
          apply H37.
          apply col_permutation_5.
          assumption.
         T''.
        split.
          apply col_permutation_2.
          assumption.
        assumption.
      apply l9_9 in H36.
      contradiction.
      auto.
    apply col_permutation_3.
    assumption.
Qed.

Lemma l11_22b :
  A B C P A' B' C' P',
 OS B P A C OS B' P' A' C'
 CongA A B P A' B' P' CongA P B C P' B' C'
 CongA A B C A' B' C'.
Proof.
    intros.
    spliter.
    prolong A B D A B.
    prolong A' B' D' A' B'.
    assert(CongA D B P D' B' P').
      eapply l11_13.
        apply H1.
        assumption.
        intro.
        subst D.
        apply cong_symmetry in H4.
        apply cong_identity in H4.
        subst A.
        unfold CongA in H1.
        spliter.
        absurde.
        assumption.
      intro.
      subst D'.
      apply cong_symmetry in H6.
      apply cong_identity in H6.
      subst A'.
      unfold CongA in H1.
      spliter.
      absurde.
    assert (CongA D B C D' B' C').
      eapply (l11_22a _ _ _ P _ _ _ P').
      split.
        eapply l9_2.
        eapply l9_8_2.
          2: apply H.
        unfold OS in H.
        ex_and H T.
        unfold TS in H.
        unfold TS in H8.
        spliter.
        repeat split.
          assumption.
          intro.
          apply H.
          apply col_permutation_2.
          eapply (col_transitivity_1 _ D).
            intro.
            subst D.
            unfold CongA in H7.
            spliter.
            absurde.
            apply col_permutation_4.
            assumption.
          unfold Col.
          right; right.
          assumption.
         B.
        split.
          apply col_trivial_1.
        assumption.
      split.
        eapply l9_2.
        eapply l9_8_2.
          2: apply H0.
        unfold OS in H0.
        ex_and H0 T'.
        unfold TS in H0.
        unfold TS in H8.
        spliter.
        repeat split.
          assumption.
          intro.
          apply H0.
          apply col_permutation_2.
          eapply (col_transitivity_1 _ D').
            intro.
            subst D'.
            unfold CongA in H7.
            spliter.
            absurde.
            apply col_permutation_4.
            assumption.
          unfold Col.
          right; right.
          assumption.
         B'.
        split.
          apply col_trivial_1.
        assumption.
      split; assumption.
    eapply l11_13.
      apply H8.
      apply between_symmetry.
      assumption.
      intro.
      subst A.
      unfold CongA in H1.
      spliter.
      absurde.
      apply between_symmetry.
      assumption.
    intro.
    subst A'.
    unfold CongA in H1.
    spliter.
    absurde.
Qed.

Lemma l11_22 :
  A B C P A' B' C' P',
 ((TS B P A C TS B' P' A' C')\/
  (OS B P A C OS B' P' A' C'))
  CongA A B P A' B' P' CongA P B C P' B' C'
 CongA A B C A' B' C'.
Proof.
    intros.
    spliter.
    induction H.
      eapply (l11_22a _ _ _ P _ _ _ P');tauto.
    eapply (l11_22b _ _ _ P _ _ _ P');tauto.
Qed.

Definition InAngle P A B C :=
  A B C B P B X, Bet A X C (X = B Out B X P).

Lemma l11_24 :
  P A B C,
  InAngle P A B C
  InAngle P C B A.
Proof.
    unfold InAngle.
    intros.
    spliter.
    ex_and H2 X.
    repeat split; try assumption.
     X.
    split.
      apply between_symmetry.
      assumption.
    assumption.
Qed.

Lemma out_in_angle :
  A B C P,
  Out B A C
  Out B P A
  InAngle P A B C.
Proof.
    intros.
    unfold InAngle.
    unfold Out in H.
    unfold Out in H0.
    spliter.
    split.
      assumption.
    split.
      assumption.
    split.
      assumption.
    induction H4; induction H2.
      assert( X, Midpoint X A C).
        eapply midpoint_existence.
      ex_and H5 X.
       X.
      split.
        apply midpoint_bet.
        assumption.
      right.
      repeat split.
        intro.
        subst X.
        apply midpoint_bet in H6.
        assert (A = B).
          eapply between_equality.
            apply H6.
          assumption.
        contradiction.
        assumption.
      right.
      induction (eq_dec_points P A).
        subst P.
        eapply between_inner_transitivity.
          apply H4.
        apply midpoint_bet.
        assumption.
      assert(Bet P A C).
        eapply between_exchange3.
          apply H2.
        assumption.
      assert(Bet P A X).
        eapply between_inner_transitivity.
          apply H7.
        apply midpoint_bet.
        assumption.
      eapply outer_transitivity_between.
        apply H2.
        assumption.
      assumption.
      assert( X, Midpoint X A C).
        eapply midpoint_existence.
      ex_and H5 X.
       X.
      repeat split.
        apply midpoint_bet.
        assumption.
      right.
      repeat split.
        intro.
        subst X.
        apply midpoint_bet in H6.
        assert (A = B).
          eapply between_equality.
            apply H6.
          assumption.
        contradiction.
        assumption.
      assert(Bet B C P Bet B P C).
        eapply l5_1.
          2: apply H4.
          auto.
        assumption.
      induction H5.
        left.
        assert(Bet B X C).
          eapply between_exchange2.
            apply H4.
          apply midpoint_bet.
          assumption.
        eapply between_exchange4.
          apply H7.
        assumption.
      assert(Bet B A X).
        eapply between_inner_transitivity.
          apply H4.
        apply midpoint_bet.
        assumption.
      eapply l5_1.
        2:apply H7.
        auto.
      assumption.
      assert(Bet B P C Bet B C P).
        eapply l5_3.
          apply H2.
        assumption.
      induction H5.
        assert( X, Midpoint X A C).
          eapply midpoint_existence.
        ex_and H6 X.
         X.
        split.
          apply midpoint_bet.
          assumption.
        right.
        repeat split.
          intro.
          subst X.
          apply midpoint_bet in H7.
          apply between_symmetry in H7.
          assert (C = B).
            eapply between_equality.
              apply H7.
            assumption.
          contradiction.
          assumption.
        right.
        assert(Bet B C X).
          eapply between_inner_transitivity.
            apply H4.
          apply midpoint_bet.
          apply l7_2.
          assumption.
        eapply between_exchange4.
          apply H5.
        assumption.
      assert( X, Midpoint X A C).
        eapply midpoint_existence.
      ex_and H6 X.
       X.
      repeat split.
        apply midpoint_bet.
        assumption.
      right.
      repeat split.
        intro.
        subst X.
        apply midpoint_bet in H7.
        apply between_symmetry in H7.
        assert (C = B).
          eapply between_equality.
            apply H7.
          assumption.
        contradiction.
        assumption.
      assert (Bet B C X).
        eapply between_inner_transitivity.
          apply H4.
        apply midpoint_bet.
        eapply l7_2.
        assumption.
      eapply l5_1.
        2:apply H6.
        auto.
      assumption.
    assert( X, Midpoint X A C).
      eapply midpoint_existence.
    ex_and H5 X.
     X.
    split.
      apply midpoint_bet.
      assumption.
    right.
    repeat split.
      intro.
      subst X.
      apply midpoint_bet in H6.
      apply between_symmetry in H6.
      assert (C = B).
        eapply between_equality.
          apply H6.
        assumption.
      contradiction.
      assumption.
    left.
    assert(Bet B X A).
      eapply between_exchange2.
        apply H4.
      apply midpoint_bet.
      apply l7_2.
      assumption.
    eapply between_exchange4.
      apply H5.
    assumption.
Qed.

Lemma col_in_angle :
  A B C P,
  A B C B P B
  Out B A P Out B C P
  InAngle P A B C.
Proof.
    intros.
    induction H2.
      repeat split; try assumption.
       A.
      split.
        apply between_symmetry.
        apply between_trivial.
      right.
      assumption.
    repeat split; try assumption.
     C.
    split.
      apply between_trivial.
    right.
    assumption.
Qed.

Lemma in_angle_two_sides :
  A B C P,
  ¬ Col B A P ¬ Col B C P
  InAngle P A B C
  TS P B A C.
Proof.
    intros.
    unfold InAngle in H1.
    spliter.
    ex_and H4 X.
    induction H5.
      subst X.
      unfold TS.
      repeat split.
        intro.
        apply H.
        apply col_permutation_2.
        assumption.
        intro.
        apply H0.
        apply col_permutation_2.
        assumption.
       B.
      split.
        apply col_trivial_3.
      assumption.
    repeat split.
      intro.
      apply H.
      apply col_permutation_2.
      assumption.
      intro.
      apply H0.
      apply col_permutation_2.
      assumption.
     X.
    split.
      apply out_col in H5.
      apply col_permutation_1.
      assumption.
    assumption.
Qed.

Lemma in_angle_out :
  A B C P,
  Out B A C
  InAngle P A B C
  Out B A P.
Proof.
    intros.
    unfold InAngle in H0.
    spliter.
    ex_and H3 X.
    induction H4.
      subst X.
      assert( Bet A B C Out B A C).
        split; assumption.
      apply not_bet_and_out in H4.
      contradiction.
    unfold Out in ×.
    spliter.
    induction H8; induction H6.
      repeat split; try assumption.
      left.
      assert(Bet B A X).
        eapply between_inner_transitivity.
          apply H8.
        apply H3.
      eapply between_exchange4.
        apply H9.
      assumption.
      repeat split; try assumption.
      assert(Bet B A X).
        eapply between_inner_transitivity.
          apply H8.
        assumption.
      eapply l5_3.
        apply H9.
      assumption.
      repeat split; try assumption.
      assert(Bet B X A).
        eapply between_exchange2.
          apply H8.
        apply between_symmetry.
        assumption.
      eapply l5_1.
        2: apply H9.
        auto.
      assumption.
    repeat split; try assumption.
    right.
    assert(Bet B X A).
      eapply between_exchange2.
        apply H8.
      apply between_symmetry.
      assumption.
    eapply between_exchange4.
      apply H6.
    assumption.
Qed.

Lemma col_in_angle_out :
  A B C P,
  Col B A P
  ¬ Bet A B C
  InAngle P A B C
  Out B A P.
Proof.
    intros.
    unfold InAngle in H1.
    spliter.
    ex_and H4 X.
    induction H5.
      subst X.
      contradiction.
    induction (eq_dec_points A X).
      subst X.
      assumption.
    apply not_bet_out in H0.
      assert(Out B A P Out B C P).
        eapply out2_bet_out.
          assumption.
          apply H5.
        assumption.
      spliter.
      assumption.
    assert (Col B A X).
      eapply col_transitivity_1.
        2: apply col_permutation_5.
        2: apply H.
        auto.
      apply out_col in H5.
      apply col_permutation_5.
      assumption.
    eapply col_transitivity_2.
      2: apply col_permutation_3.
      2:apply H7.
      auto.
    unfold Col.
    right; right.
    apply between_symmetry.
    assumption.
Qed.

Lemma l11_25_aux : P A B C A' ,
 InAngle P A B C
 ¬ Bet A B C
 Out B A' A
 InAngle P A' B C.
Proof.
    intros.
    unfold Out in H1.
    unfold InAngle in H.
    spliter.
    repeat split ; try assumption.
    induction H3.
      ex_and H6 X.
      assert( T, Bet A' T C Bet X T B).
        eapply inner_pasch.
          apply H3.
        apply between_symmetry.
        assumption.
      ex_and H8 T.
       T.
      split.
        assumption.
      right.
      induction H7.
        subst B.
        contradiction.
      unfold Out in ×.
      spliter.
      repeat split.
        intro.
        subst T.
        apply H0.
        apply between_symmetry.
        eapply outer_transitivity_between.
          apply between_symmetry.
          apply H8.
          assumption.
        auto.
        assumption.
      induction H11.
        left.
        eapply between_exchange4.
          apply between_symmetry.
          apply H9.
        assumption.
      eapply l5_3.
        apply between_symmetry.
        apply H9.
      assumption.
    ex_and H6 X.
    induction H7.
      subst X.
      contradiction.
    assert( T, Bet A' T C Bet B X T).
      eapply outer_pasch.
        apply between_symmetry.
        apply H3.
      apply between_symmetry.
      assumption.
    ex_and H8 T.
     T.
    split.
      assumption.
    right.
    unfold Out in H7.
    spliter.
    repeat split.
      intro.
      subst T.
      apply between_identity in H9.
      subst X.
      absurde.
      assumption.
    induction H11.
      eapply l5_1.
        2: apply H9.
        auto.
      assumption.
    right.
    eapply between_exchange4.
      apply H11.
    assumption.
Qed.

Lemma l11_25 : P A B C A' C' P',
 InAngle P A B C
 Out B A' A
 Out B C' C
 Out B P' P
 InAngle P' A' B C'.
Proof.
    intros.
    induction (bet_dec A B C).
      repeat split.
        unfold Out in H0.
        spliter.
        assumption.
        unfold Out in H1.
        spliter.
        assumption.
        unfold Out in H2.
        spliter.
        assumption.
       B.
      split.
        eapply bet_out_out_bet.
          apply H3.
          apply l6_6.
          assumption.
        apply l6_6.
        assumption.
      left.
      reflexivity.
    assert(InAngle P A' B C).
      eapply l11_25_aux.
        apply H.
        assumption.
      assumption.
    assert(InAngle P A' B C').
      apply l11_24.
      eapply l11_25_aux.
        apply l11_24.
        apply H4.
        intro.
        apply H3.
        apply between_symmetry.
        eapply bet_out_out_bet.
          apply H5.
          apply out_trivial.
          unfold InAngle in H.
          spliter.
          auto.
        assumption.
      assumption.
    unfold InAngle in H5.
    spliter.
    ex_and H8 X.
    induction H9.
      subst X.
      apply False_ind.
      apply H3.
      eapply bet_out_out_bet.
        apply H8.
        assumption.
      assumption.
    repeat split.
      assumption.
      assumption.
      intro.
      subst P'.
      unfold Out in H2.
      spliter.
      absurde.
     X.
    split.
      assumption.
    right.
    eapply l6_7.
      apply H9.
    apply l6_6.
    assumption.
Qed.

Definition LeA A B C D E F := P, InAngle P D E F CongA A B C D E P.

Lemma segment_construction_0 : A B A', B', Cong A' B' A B.
Proof.
    intros.
    induction (eq_dec_points A B).
       A'.
      subst B.
      apply cong_trivial_identity.
    assert( X : Tpoint, A' X).
      apply another_point.
    ex_and H0 X.
    assert(HH:=segment_construction_3 A' X A B H1 H).
    ex_and HH B'.
     B'.
    assumption.
Qed.

Lemma angle_construction_3 :
  A B C A' B',
  A B C B A' B'
   C', CongA A B C A' B' C'.
Proof.
    intros.
    assert( P, ¬Col A' B' P).
      eapply l6_25.
      assumption.
    ex_and H2 P.
    induction (eq_dec_points A C).
      subst C.
       A'.
      apply conga_trivial_1; assumption.
    assert( C', CongA A B C A' B' C' (OS A' B' C' P Col A' B' C')).
      apply angle_construction_2.
        assumption.
        assumption.
        auto.
        assumption.
      assumption.
    ex_and H4 C'.
     C'.
    assumption.
Qed.

Lemma l11_28 : A B C D A' B' C',
 Cong_3 A B C A' B' C' Col A C D
  D', Cong A D A' D' Cong B D B' D' Cong C D C' D'.
Proof.
    intros.
    induction (eq_dec_points A C).
      subst C.
      unfold Cong_3 in H.
      spliter.
      apply cong_symmetry in H1.
      apply cong_identity in H1.
      subst C'.
      induction(eq_dec_points A B).
        subst B.
        apply cong_symmetry in H2.
        apply cong_identity in H2.
        subst B'.
        assert( D', Cong A' D' A D).
          apply segment_construction_0.
        ex_and H1 D'.
         D'.
        apply cong_symmetry in H2.
        repeat split; assumption.
      induction (eq_dec_points A D).
         A'.
        subst D.
        repeat split.
          apply cong_trivial_identity.
          assumption.
        apply cong_trivial_identity.
      induction (eq_dec_points B D).
        subst D.
         B'.
        repeat split.
          assumption.
          apply cong_trivial_identity.
        assumption.
      assert( D'', CongA B A D B' A' D'').
        eapply angle_construction_3.
          auto.
          auto.
        intro.
        subst B'.
        apply cong_identity in H.
        contradiction.
      ex_and H5 D''.
      assert( D', Out A' D'' D' Cong A' D' A D).
        apply segment_construction_3.
          unfold CongA in H6.
          spliter.
          auto.
        assumption.
      ex_and H5 D'.
       D'.
      repeat split.
        apply cong_symmetry.
        assumption.
        assert(CongA B A D B' A' D').
          eapply (l11_10 B A D B' A' D''); try apply out_trivial; try solve [auto].
            intro.
            subst B'.
            unfold CongA in H6.
            spliter.
            absurde.
          apply l6_6.
          assumption.
        eapply (cong2_conga_cong _ A _ _ A' _).
          apply H8.
          assumption.
        Cong.
      Cong.
    unfold Cong_3 in H.
    spliter.
    induction(eq_dec_points A D).
      subst D.
       A'.
      repeat split.
        apply cong_trivial_identity.
        apply cong_commutativity.
        assumption.
      apply cong_commutativity.
      assumption.
    unfold Col in H0.
    induction H0.
      prolong A' C' D' C D.
       D'.
      repeat split.
        eapply (l2_11 A C D A' C' D'); try assumption.
        apply cong_symmetry.
        assumption.
        apply cong_commutativity.
        eapply (five_segment_with_def A C D B A' C' D' B').
          repeat split; try assumption.
            apply cong_symmetry.
            assumption.
          apply cong_commutativity.
          assumption.
        assumption.
      apply cong_symmetry.
      assumption.
    induction H0.
      assert( D', Bet A' D' C' Cong_3 A D C A' D' C').
        eapply l4_5.
          apply between_symmetry.
          assumption.
        assumption.
      ex_and H5 D'.
      unfold Cong_3 in H6.
      spliter.
       D'.
      repeat split.
        assumption.
        apply cong_commutativity.
        eapply (l4_2 A D C B A' D' C' B').
        repeat split; try assumption.
          apply between_symmetry.
          assumption.
        apply cong_commutativity.
        assumption.
      apply cong_commutativity.
      assumption.
    prolong C' A' D' A D.
     D'.
    repeat split.
      apply cong_symmetry.
      assumption.
      apply cong_commutativity.
      eapply (five_segment_with_def C A D B C' A' D' B').
        repeat split; try assumption.
          apply between_symmetry.
          assumption.
          apply cong_commutativity.
          assumption.
          apply cong_symmetry.
          assumption.
        apply cong_commutativity.
        assumption.
      auto.
    eapply l2_11.
      apply between_symmetry.
      apply H0.
      apply H5.
      apply cong_commutativity.
      assumption.
    apply cong_symmetry.
    assumption.
Qed.

Lemma bet_conga_bet :
  A B C A' B' C',
  Bet A B C
  CongA A B C A' B' C'
  Bet A' B' C'.
Proof.
    intros.
    unfold CongA in H0.
    spliter.
    ex_and H4 A0.
    ex_and H5 C0.
    ex_and H4 A1.
    ex_and H5 C1.
    assert(Bet A0 B C0).
      eapply outer_transitivity_between.
        2:apply H6.
        apply between_symmetry.
        eapply outer_transitivity_between.
          2:apply H4.
          apply between_symmetry.
          assumption.
        auto.
      auto.
    assert(Cong_3 A0 B C0 A1 B' C1).
      repeat split.
        apply cong_right_commutativity.
        eapply l2_11.
          apply between_symmetry.
          apply H4.
          apply H8.
          apply cong_left_commutativity.
          assumption.
        apply cong_symmetry.
        apply cong_right_commutativity.
        assumption.
        assumption.
      apply cong_right_commutativity.
      eapply l2_11.
        apply H6.
        apply between_symmetry.
        apply H10.
        apply cong_symmetry.
        apply cong_left_commutativity.
        assumption.
      apply cong_right_commutativity.
      assumption.
    assert(Bet A1 B' C1).
      eapply l4_6.
        apply H13.
      assumption.
    eapply between_inner_transitivity.
      2:apply H10.
    eapply between_exchange3.
      apply between_symmetry.
      apply H8.
    assumption.
Qed.

Lemma out_in_angle_out :
  A B C P,
  Out B A C
  InAngle P A B C
  Out B A P.
Proof.
    intros.
    unfold InAngle in H0.
    spliter.
    ex_and H3 X.
    induction H4.
      subst X.
      unfold Out in H.
      spliter.
      induction H5.
        assert (A = B).
          eapply between_equality.
            apply H3.
          assumption.
        contradiction.
      assert (C = B).
        eapply between_equality.
          apply between_symmetry.
          apply H3.
        assumption.
      contradiction.
    unfold Out in H.
    spliter.
    induction H6.
      assert(Bet B A X).
        eapply between_inner_transitivity.
          apply H6.
        assumption.
      unfold Out in H4.
      spliter.
      induction H9.
        assert(Bet B A P).
          eapply between_exchange4.
            apply H7.
          assumption.
        apply bet_out; assumption.
      assert(Bet B A P Bet B P A).
        eapply l5_3.
          apply H7.
        assumption.
      unfold Out.
      repeat split; assumption.
    assert (Bet B X A).
      eapply between_exchange2.
        apply H6.
      apply between_symmetry.
      assumption.
    unfold Out in H4.
    spliter.
    induction H9.
      assert(Bet B A P Bet B P A).
        eapply l5_1.
          2: apply H7.
          auto.
        assumption.
      unfold Out.
      repeat split; try assumption.
    assert(Bet B P A).
      eapply between_exchange4.
        apply H9.
      assumption.
    eapply l6_6.
    apply bet_out; assumption.
Qed.

Lemma in_angle_one_side :
  A B C P,
  ¬ Col A B C
  ¬ Col B A P
  InAngle P A B C
  OS A B P C.
Proof.
    intros.
    unfold InAngle in H1.
    spliter.
    ex_and H4 X.
    induction H5.
      subst X.
      apply False_ind.
      apply H.
      unfold Col.
      left.
      assumption.
    unfold OS.
    prolong C A C' C A.
     C'.
    assert(TS A B X C').
      repeat split.
        intro.
        apply H0.
        eapply (col_transitivity_1 _ X).
          intro.
          subst X.
          apply H.
          left.
          assumption.
          eapply (col_transitivity_1 _ A).
            auto.
            apply col_permutation_3.
            assumption.
          apply col_trivial_2.
        apply out_col.
        assumption.
        intro.
        apply H.
        eapply (col_transitivity_1 _ C').
          intro.
          subst C'.
          apply cong_symmetry in H7.
          apply cong_identity in H7.
          subst C.
          apply H.
          apply col_trivial_3.
          apply col_permutation_4.
          assumption.
        unfold Col.
        right; right.
        assumption.
       A.
      split.
        apply col_trivial_1.
      eapply between_exchange3.
        2: apply H6.
      apply between_symmetry.
      assumption.
    split.
      eapply l9_5.
        apply H8.
        2: apply H5.
      apply col_trivial_3.
    repeat split.
      intro.
      apply H.
      apply col_permutation_1.
      assumption.
      intro.
      apply H.
      eapply (col_transitivity_1 _ C').
        intro.
        subst C'.
        unfold TS in H8.
        spliter.
        apply H10.
        apply col_trivial_1.
        apply col_permutation_4.
        assumption.
      unfold Col.
      right; right.
      assumption.
     A.
    split.
      apply col_trivial_1.
    assumption.
Qed.

Lemma in_angle_trivial_1 : A B C, A B C B InAngle A A B C.
Proof.
    intros.
    repeat split.
      assumption.
      assumption.
      assumption.
     A.
    split.
      apply between_symmetry.
      apply between_trivial.
    right.
    apply out_trivial.
    auto.
Qed.

Lemma in_angle_trivial_2 : A B C, A B C B InAngle C A B C.
Proof.
    intros.
    apply l11_24.
    apply in_angle_trivial_1; assumption.
Qed.

Lemma col_conga_col : A B C D E F, Col A B C CongA A B C D E F Col D E F.
Proof.
    intros.
    induction H.
      assert (Bet D E F).
        eapply bet_conga_bet.
          apply H.
        assumption.
      unfold Col.
      left.
      assumption.
    induction H.
      assert (Out E D F).
        eapply l11_21_a.
          2: apply H0.
        apply bet_out in H.
          apply l6_6.
          assumption.
          unfold CongA in H0.
          spliter.
          assumption.
        unfold CongA in H0.
        spliter.
        assumption.
      unfold Out in H1.
      spliter.
      unfold Col.
      induction H3.
        right; right.
        apply between_symmetry.
        assumption.
      right; left.
      assumption.
    assert (Out E D F).
      eapply l11_21_a.
        2: apply H0.
      apply between_symmetry in H.
      apply bet_out in H.
        assumption.
        unfold CongA in H0.
        spliter.
        assumption.
      unfold CongA in H0.
      spliter.
      assumption.
    unfold Out in H1.
    spliter.
    unfold Col.
    induction H3.
      right; right.
      apply between_symmetry.
      assumption.
    right; left.
    assumption.
Qed.

Lemma ncol_conga_ncol : A B C D E F, ¬Col A B C CongA A B C D E F ¬Col D E F.
Proof.
    intros.
    intro.
    apply H.
    eapply col_conga_col.
      apply H1.
    apply conga_sym.
    assumption.
Qed.

Lemma l11_29_a : A B C D E F, LeA A B C D E F Q, InAngle C A B Q CongA A B Q D E F.
Proof.
    intros.
    unfold LeA in H.
    ex_and H P.
    assert(E D B A E F E P B C).
      unfold CongA in ×.
      unfold InAngle in H.
      spliter.
      repeat split.
        auto.
        auto.
        auto.
        auto.
      auto.
    spliter.
    assert(A B C B).
      intuition.
    spliter.
    assert(HH:=or_bet_out A B C).
    induction HH.
      assert(Bet D E P).
        eapply bet_conga_bet.
          apply H8.
        assumption.
       C.
      split.
        apply in_angle_trivial_2; assumption.
      assert(HH:=H).
      unfold InAngle in HH.
      spliter.
      ex_and H13 X.
      induction H14.
        subst X.
        assert(Bet E F P Bet E P F).
          eapply (l5_2 D).
            auto.
            assumption.
          assumption.
        eapply l11_10.
          apply H0.
          apply out_trivial.
          auto.
          apply out_trivial.
          auto.
          apply out_trivial.
          assumption.
        repeat split.
          auto.
          auto.
        assumption.
      assert(Out E P F).
        unfold Out in H14.
        spliter.
        induction H16.
          assert( Bet D X P).
            eapply between_exchange2.
              apply H9.
            assumption.
          assert(Bet D E X).
            eapply between_inner_transitivity.
              apply H9.
            assumption.
          assert(Bet D E F).
            eapply between_exchange4.
              apply H18.
            assumption.
          unfold Out.
          repeat split.
            auto.
            auto.
          eapply l5_2.
            2:apply H9.
            auto.
          assumption.
        assert(Bet D P X).
          eapply outer_transitivity_between2.
            apply H9.
            assumption.
          assumption.
        assert(Bet D P F).
          eapply between_exchange4.
            apply H17.
          assumption.
        assert(Bet E P F).
          eapply between_exchange3.
            apply H9.
          assumption.
        repeat split.
          auto.
          auto.
        left.
        assumption.
      eapply l11_10.
        apply H0.
        apply out_trivial.
        auto.
        apply out_trivial.
        auto.
        apply out_trivial.
        assumption.
      eapply l6_6.
      assumption.
    induction H8.
      assert( Q, CongA D E F A B Q).
        apply angle_construction_3.
          auto.
          auto.
        assumption.
      ex_and H9 Q.
       Q.
      split.
        repeat split.
          assumption.
          intro.
          subst Q.
          unfold CongA in H10.
          spliter.
          intuition.
          auto.
         A.
        split.
          apply between_trivial2.
        right.
        assumption.
      apply conga_sym.
      assumption.
    assert(D E F E).
      intuition.
    spliter.
    assert(HH:=or_bet_out D E F).
    induction HH.
      prolong A B Q E F.
       Q.
      split.
        repeat split.
          assumption.
          intro.
          treat_equalities.
          auto.
          assumption.
         B.
        split.
          assumption.
        left.
        reflexivity.
      eapply conga_line; try assumption.
        intro.
        treat_equalities.
        auto.
    induction H11.
      assert(Out E D P).
        eapply in_angle_out.
          apply H11.
        assumption.
      assert (Out B A C).
        eapply l11_21_a.
          apply H12.
        apply conga_sym.
        assumption.
      apply False_ind.
      apply H8.
      apply out_col in H13.
      Col.
    assert( Q, CongA D E F A B Q OS A B Q C).
      apply angle_construction_1; assumption.
    ex_and H12 Q.
     Q.
    assert( DD, Out E D DD Cong E DD B A).
      eapply segment_construction_3; auto.
    ex_and H14 DD.
    assert( FF, Out E F FF Cong E FF B Q).
      eapply segment_construction_3.
        auto.
      unfold CongA in H12.
      spliter.
      auto.
    ex_and H16 FF.
    assert(InAngle P DD E FF).
      eapply l11_25.
        apply H.
        apply l6_6.
        assumption.
        apply l6_6.
        assumption.
      apply out_trivial.
      auto.
    assert(HH18:=H18).
    unfold InAngle in H18.
    spliter.
    ex_and H21 X.
    induction H22.
      subst X.
      assert (Bet D E F).
        eapply bet_out_out_bet.
          apply H21.
          apply l6_6.
          assumption.
        apply l6_6.
        assumption.
      apply False_ind.
      apply H11.
      unfold Col.
      left.
      assumption.
    assert( CC, Out B C CC Cong B CC E X).
      apply segment_construction_3.
        auto.
      unfold Out in H22.
      spliter.
      auto.
    ex_and H23 CC.
    assert (CongA A B CC DD E X).
      eapply l11_10.
        apply H0.
        apply out_trivial.
        auto.
        apply l6_6.
        assumption.
        apply