Library GeoCoq.Tarski_dev.Coplanar_trans

Require Export GeoCoq.Tarski_dev.Coplanar_perm.

Section Coplanar_trans.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma coplanar_trans_1_aux_1_1_1 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  Col P Q X1
  Col P Q X2
  Bet R A X1
  Bet R B X2
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABQ HABR HAQR HBQR HCol1 HCol3 HCol2 HCol4.
assert (HQX1X2 : Col Q X1 X2) by (assert_diffs; ColR).
elim HQX1X2; clear HQX1X2; intro HQX1X2.

  {
  assert (H : TS A R B Q).
    {
    apply l9_8_2 with X2.

      {
      assert (R X2) by (intro; assert_cols; apply HABR; ColR).
      split; try (intro; assert_cols; apply HABR; ColR).
      split; Col.
       X1; assert_cols; Col; Between.
      }

      {
      assert (H1 : A R) by (assert_diffs; auto).
      assert (H2 : Col A R R) by Col.
      assert (H3 : Col X2 B R) by (assert_cols; Col).
      assert (H := l9_19 A R X2 B R H1 H2 H3); rewrite H.
      assert (R X2) by (intro; assert_cols; apply HABR; ColR).
      split; try (intro; assert_cols; apply HABR; ColR).
      split; try auto.
      split; try (intro; subst; apply HABR; Col).
      Between.
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }

  {
  elim HQX1X2; clear HQX1X2; intro HQX1X2.

    {
    assert (H : TS B R A Q).
      {
      apply l9_8_2 with X1.

        {
        assert (R X1) by (intro; assert_cols; apply HABR; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        split; Col.
         X2; assert_cols; Col; Between.
        }

        {
        assert (H1 : B R) by (assert_diffs; auto).
        assert (H2 : Col B R R) by Col.
        assert (H3 : Col X1 A R) by (assert_cols; Col).
        assert (H := l9_19 B R X1 A R H1 H2 H3); rewrite H.
        assert (R X1) by (intro; assert_cols; apply HABR; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        split; try auto.
        split; try (intro; subst; apply HABR; Col).
        Between.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }

    {
    assert (HTS1 : TS Q R X1 X2).
      {
      assert (R X1) by (intro; subst; apply HNC; ColR).
      split; try (intro; assert_cols; apply HAQR; ColR).
      assert (R X2) by (intro; subst; apply HNC; ColR).
      split; try (intro; assert_cols; apply HBQR; ColR).
       Q; Col; Between.
      }
    assert (HTS2 : TS Q R A X2).
      {
      apply l9_8_2 with X1; try assumption.
      assert (H1 : Q R) by (assert_diffs; auto).
      assert (H2 : Col Q R R) by Col.
      assert (H3 : Col X1 A R) by (assert_cols; Col).
      assert (H := l9_19 Q R X1 A R H1 H2 H3); rewrite H.
      assert (R X1) by (intro; subst; apply HNC; Col).
      split; try (intro; assert_cols; apply HAQR; ColR).
      split; try auto.
      split; try (intro; subst; apply HABR; Col).
      Between.
      }
    assert (H : TS Q R A B).
      {
      apply l9_2.
      apply l9_8_2 with X2; try (apply l9_2; assumption).
      assert (H1 : Q R) by (assert_diffs; auto).
      assert (H2 : Col Q R R) by Col.
      assert (H3 : Col X2 B R) by (assert_cols; Col).
      assert (H := l9_19 Q R X2 B R H1 H2 H3); rewrite H.
      assert (R X2) by (intro; subst; apply HNC; Col).
      split; try (intro; assert_cols; apply HBQR; ColR).
      split; try auto.
      split; try (intro; subst; apply HABR; Col).
      Between.
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_1_1_2 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  Col P Q X1
  Col P Q X2
  Bet R A X1
  Bet B X2 R
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABQ HABR HAQR HBQR HCol1 HCol3 HCol2 HCol4.
assert (HQX1X2 : Col Q X1 X2) by (assert_diffs; ColR).
elim HQX1X2; clear HQX1X2; intro HQX1X2.

  {
  assert (H : TS A R B Q).
    {
    apply l9_8_2 with X2.

      {
      assert (R X2) by (intro; assert_cols; apply HNC; ColR).
      split; try (intro; assert_cols; apply HABR; ColR).
      split; Col.
       X1; assert_cols; Col; Between.
      }

      {
      assert (H1 : A R) by (assert_diffs; auto).
      assert (H2 : Col A R R) by Col.
      assert (H3 : Col X2 B R) by (assert_cols; Col).
      assert (H := l9_19 A R X2 B R H1 H2 H3); rewrite H.
      assert (R X2) by (intro; assert_cols; apply HNC; ColR).
      split; try (intro; assert_cols; apply HABR; ColR).
      split; try auto.
      split; try (intro; subst; apply HABR; Col).
      Between.
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }

  {
  elim HQX1X2; clear HQX1X2; intro HQX1X2.

    {
    assert (H : TS B R A Q).
      {
      apply l9_8_2 with X1.

        {
        assert (R X1) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        split; Col.
         X2; assert_cols; Col; Between.
        }

        {
        assert (H1 : B R) by (assert_diffs; auto).
        assert (H2 : Col B R R) by Col.
        assert (H3 : Col X1 A R) by (assert_cols; Col).
        assert (H := l9_19 B R X1 A R H1 H2 H3); rewrite H.
        assert (R X1) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        split; try auto.
        split; try (intro; subst; apply HABR; Col).
        Between.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }

    {
    assert (H : TS R Q A B).
      {
      apply l9_31.

        {
        apply one_side_transitivity with X2.

          {
          assert (H1 : R A) by (assert_diffs; auto).
          assert (H2 : Col R A X1) by (assert_cols; Col).
          assert (H3 : Col Q X2 X1) by (assert_cols; Col).
          assert (H := l9_19 R A Q X2 X1 H1 H2 H3); rewrite H.
          split; Col.
          split; try (intro; subst; apply HAQR; Col).
          assert (R X1) by (intro; subst; treat_equalities; apply H1; reflexivity).
          split; try (intro; subst; apply HAQR; ColR).
          Between.
          }

          {
          assert (H1 : R A) by (assert_diffs; auto).
          assert (H2 : Col R A R) by Col.
          assert (H3 : Col X2 B R) by (assert_cols; Col).
          assert (H := l9_19 R A X2 B R H1 H2 H3); rewrite H.
          assert (R X2) by (intro; assert_cols; apply HNC; ColR).
          split; try (intro; assert_cols; apply HABR; ColR).
          split; try auto.
          split; try (intro; subst; apply HABR; Col).
          Between.
          }
        }

        {
        apply one_side_transitivity with X1.

          {
          assert (H1 : R B) by (assert_diffs; auto).
          assert (H2 : Col R B X2) by (assert_cols; Col).
          assert (H3 : Col Q X1 X2) by (assert_cols; Col).
          assert (H := l9_19 R B Q X1 X2 H1 H2 H3); rewrite H.
          split; Col.
          split; try (intro; subst; apply HBQR; Col).
          split; try (intro; treat_equalities; assert_cols; apply HAQR; Col).
          Between.
          }

          {
          assert (H1 : R B) by (assert_diffs; auto).
          assert (H2 : Col R B R) by Col.
          assert (H3 : Col X1 A R) by (assert_cols; Col).
          assert (H := l9_19 R B X1 A R H1 H2 H3); rewrite H.
          assert (R X1) by (intro; assert_cols; apply HNC; ColR).
          split; try (intro; assert_cols; apply HABR; ColR).
          split; try auto.
          split; try (intro; subst; apply HABR; Col).
          Between.
          }
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_1_1_3 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  Col P Q X1
  Col P Q X2
  Bet R A X1
  Bet X2 R B
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABQ HABR HAQR HBQR HCol1 HCol3 HCol2 HCol4.
assert (HQX1X2 : Col Q X1 X2) by (assert_diffs; ColR).
elim HQX1X2; clear HQX1X2; intro HQX1X2.

  {
  assert (H : TS R Q A B).
    {
    apply l9_31.

      {
       X2; split.

        {
        assert (R X1) by (intro; assert_cols; apply HNC; ColR).
        split; Col.
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
         X1; assert_cols; Col; Between.
        }

        {
        assert (R X1) by (intro; assert_cols; apply HNC; ColR).
        split; Col.
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
         R; assert_cols; Col; Between.
        }
      }

      {
      apply one_side_transitivity with X1.

        {
        assert (H1 : R B) by (assert_diffs; auto).
        assert (H2 : Col R B X2) by (assert_cols; Col).
        assert (H3 : Col Q X1 X2) by (assert_cols; Col).
        assert (H := l9_19 R B Q X1 X2 H1 H2 H3); rewrite H.
        split; Col.
        split; try (intro; subst; apply HBQR; Col).
        assert (R X1) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; treat_equalities; assert_cols; apply HABR; ColR).
        Between.
        }

        {
        assert (H1 : R B) by (assert_diffs; auto).
        assert (H2 : Col R B R) by Col.
        assert (H3 : Col X1 A R) by (assert_cols; Col).
        assert (H := l9_19 R B X1 A R H1 H2 H3); rewrite H.
        assert (R X1) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        split; try auto.
        split; try (intro; subst; apply HABR; Col).
        Between.
        }
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }

  {
  elim HQX1X2; clear HQX1X2; intro HQX1X2.

    {
    assert (H : TS A R Q B).
      {
      apply l9_8_2 with X2.

        {
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; assert_cols; apply HABR; ColR).
        split; Col.
         R; assert_cols; Col; Between.
        }

        {
        assert (H1 : A R) by (assert_diffs; auto).
        assert (H2 : Col A R X1) by (assert_cols; Col).
        assert (H3 : Col X2 Q X1) by (assert_cols; Col).
        assert (H := l9_19 A R X2 Q X1 H1 H2 H3); rewrite H.
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        assert (R X1) by (intro; assert_cols; apply HNC; ColR).
        assert (HX1X2 : X1 X2) by (intro; assert_cols; apply HABR; ColR).
        split; auto.
        split; try (intro; treat_equalities; apply HX1X2; reflexivity).
        Between.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }

    {
    assert (H : TS A R Q B).
      {
      apply l9_8_2 with X2.

        {
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; assert_cols; apply HABR; ColR).
        split; Col.
         R; assert_cols; Col; Between.
        }

        {
        assert (H1 : A R) by (assert_diffs; auto).
        assert (H2 : Col A R X1) by (assert_cols; Col).
        assert (H3 : Col X2 Q X1) by (assert_cols; Col).
        assert (H := l9_19 A R X2 Q X1 H1 H2 H3); rewrite H.
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        assert (R X1) by (intro; assert_cols; apply HNC; ColR).
        assert (HX1X2 : X1 X2) by (intro; assert_cols; apply HABR; ColR).
        split; auto.
        split; try (intro; subst; apply HAQR; Col).
        Between.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_1_2_2 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  Col P Q X1
  Col P Q X2
  Bet A X1 R
  Bet B X2 R
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABQ HABR HAQR HBQR HCol1 HCol3 HCol2 HCol4.
assert (HQX1X2 : Col Q X1 X2) by (assert_diffs; ColR).
elim HQX1X2; clear HQX1X2; intro HQX1X2.

  {
  assert (H : TS A R B Q).
    {
    apply l9_8_2 with X2.

      {
      assert (R X2) by (intro; assert_cols; apply HNC; ColR).
      split; try (intro; assert_cols; assert_cols; apply HABR; ColR).
      split; Col.
       X1; assert_cols; split; Col; Between.
      }

      {
      assert (H1 : A R) by (assert_diffs; auto).
      assert (H2 : Col A R R) by Col.
      assert (H3 : Col X2 B R) by (assert_cols; Col).
      assert (H := l9_19 A R X2 B R H1 H2 H3); rewrite H.
      assert (HRX2 : R X2) by (intro; assert_cols; apply HNC; ColR).
      split; try (intro; assert_cols; apply HABR; ColR).
      assert (HRX1 : R X1) by (intro; assert_cols; apply HNC; ColR).
      assert (HX1X2 : X1 X2) by (intro; assert_cols; apply HABR; ColR).
      split; auto.
      split; try (intro; treat_equalities; apply HRX2; reflexivity).
      Between.
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }

  {
  elim HQX1X2; clear HQX1X2; intro HQX1X2.

    {
    assert (H : TS B R A Q).
      {
      apply l9_8_2 with X1.

        {
        assert (R X1) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; assert_cols; apply HABR; ColR).
        split; Col.
         X2; assert_cols; split; Col; Between.
        }

        {
        assert (H1 : B R) by (assert_diffs; auto).
        assert (H2 : Col B R R) by Col.
        assert (H3 : Col X1 A R) by (assert_cols; Col).
        assert (H := l9_19 B R X1 A R H1 H2 H3); rewrite H.
        assert (HRX1 : R X1) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        assert (HRX2 : R X2) by (intro; assert_cols; apply HNC; ColR).
        assert (HX1X2 : X1 X2) by (intro; assert_cols; apply HABR; ColR).
        split; auto.
        split; try (intro; treat_equalities; apply HRX1; reflexivity).
        Between.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }

    {
    assert (H : TS R Q A B).
      {
      apply l9_31.

        {
        apply one_side_transitivity with X2.

          {
          assert (H1 : R A) by (assert_diffs; auto).
          assert (H2 : Col R A X1) by (assert_cols; Col).
          assert (H3 : Col Q X2 X1) by (assert_cols; Col).
          assert (H := l9_19 R A Q X2 X1 H1 H2 H3); rewrite H.
          split; Col.
          split; try (intro; subst; apply HAQR; Col).
          assert (R X1) by (intro; assert_cols; apply HNC; ColR).
          split; try (intro; treat_equalities; assert_cols; apply HABR; ColR).
          Between.
          }

          {
          assert (H1 : R A) by (assert_diffs; auto).
          assert (H2 : Col R A R) by Col.
          assert (H3 : Col X2 B R) by (assert_cols; Col).
          assert (H := l9_19 R A X2 B R H1 H2 H3); rewrite H.
          assert (R X2) by (intro; assert_cols; apply HNC; ColR).
          split; try (intro; assert_cols; apply HABR; ColR).
          split; try auto.
          split; try (intro; subst; apply HABR; Col).
          Between.
          }
        }

        {
        apply one_side_transitivity with X1.

          {
          assert (H1 : R B) by (assert_diffs; auto).
          assert (H2 : Col R B X2) by (assert_cols; Col).
          assert (H3 : Col Q X1 X2) by (assert_cols; Col).
          assert (H := l9_19 R B Q X1 X2 H1 H2 H3); rewrite H.
          split; Col.
          split; try (intro; subst; apply HBQR; Col).
          assert (R X2) by (intro; assert_cols; apply HNC; ColR).
          split; try (intro; treat_equalities; assert_cols; apply HABR; ColR).
          Between.
          }

          {
          assert (H1 : R B) by (assert_diffs; auto).
          assert (H2 : Col R B R) by Col.
          assert (H3 : Col X1 A R) by (assert_cols; Col).
          assert (H := l9_19 R B X1 A R H1 H2 H3); rewrite H.
          assert (R X1) by (intro; assert_cols; apply HNC; ColR).
          split; try (intro; assert_cols; apply HABR; ColR).
          split; try auto.
          split; try (intro; subst; apply HABR; Col).
          Between.
          }
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_1_2_3 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  Col P Q X1
  Col P Q X2
  Bet A X1 R
  Bet X2 R B
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABQ HABR HAQR HBQR HCol1 HCol3 HCol2 HCol4.
assert (HQX1X2 : Col Q X1 X2) by (assert_diffs; ColR).
elim HQX1X2; clear HQX1X2; intro HQX1X2.

  {
  assert (H : TS R Q A B).
    {
    apply l9_31.

      {
       X2; split.

        {
        assert (R X1) by (intro; assert_cols; apply HNC; ColR).
        split; Col.
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
         X1; assert_cols; Col; Between.
        }

        {
        assert (R X1) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; subst; apply HABR; Col).
        split; Col.
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        try (intro; assert_cols; apply HABR; ColR).
         R; assert_cols; Col; Between.
        }
      }

      {
      apply one_side_transitivity with X1.

        {
        assert (H1 : R B) by (assert_diffs; auto).
        assert (H2 : Col R B X2) by (assert_cols; Col).
        assert (H3 : Col Q X1 X2) by (assert_cols; Col).
        assert (H := l9_19 R B Q X1 X2 H1 H2 H3); rewrite H.
        split; Col.
        split; try (intro; subst; apply HBQR; Col).
        assert (R X1) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; treat_equalities; assert_cols; apply HABR; ColR).
        Between.
        }

        {
        assert (H1 : R B) by (assert_diffs; auto).
        assert (H2 : Col R B R) by Col.
        assert (H3 : Col X1 A R) by (assert_cols; Col).
        assert (H := l9_19 R B X1 A R H1 H2 H3); rewrite H.
        assert (R X1) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        split; try auto.
        split; try (intro; subst; apply HABR; Col).
        Between.
        }
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }

  {
  elim HQX1X2; clear HQX1X2; intro HQX1X2.

    {
    assert (H : TS A R Q B).
      {
      apply l9_8_2 with X2.

        {
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; assert_cols; apply HABR; ColR).
        split; Col.
         R; assert_cols; split; Col; Between.
        }

        {
        assert (H1 : A R) by (assert_diffs; auto).
        assert (H2 : Col A R X1) by Col.
        assert (H3 : Col X2 Q X1) by (assert_cols; Col).
        assert (H := l9_19 A R X2 Q X1 H1 H2 H3); rewrite H.
        assert (HRX2 : R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        assert (HRX1 : R X1) by (intro; assert_cols; apply HNC; ColR).
        assert (HX1X2 : X1 X2) by (intro; assert_cols; apply HABR; ColR).
        split; auto.
        split; try (intro; subst; assert_cols; apply HAQR; Col).
        Between.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }

    {
    assert (H : TS A R Q B).
      {
      apply l9_8_2 with X2.

        {
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; assert_cols; apply HABR; ColR).
        split; Col.
         R; assert_cols; split; Col; Between.
        }

        {
        assert (H1 : A R) by (assert_diffs; auto).
        assert (H2 : Col A R X1) by Col.
        assert (H3 : Col X2 Q X1) by (assert_cols; Col).
        assert (H := l9_19 A R X2 Q X1 H1 H2 H3); rewrite H.
        assert (HRX2 : R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        assert (HRX1 : R X1) by (intro; assert_cols; apply HNC; ColR).
        assert (HX1X2 : X1 X2) by (intro; assert_cols; apply HABR; ColR).
        split; auto.
        split; try (intro; subst; assert_cols; apply HAQR; Col).
        Between.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_1_3_3 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  Col P Q X1
  Col P Q X2
  Bet X1 R A
  Bet X2 R B
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABQ HABR HAQR HBQR HCol1 HCol3 HCol2 HCol4.
assert (HQX1X2 : Col Q X1 X2) by (assert_diffs; ColR).
elim HQX1X2; clear HQX1X2; intro HQX1X2.

  {
  assert (H : TS B R Q A).
    {
    apply l9_8_2 with X1.

      {
      assert (R X1) by (intro; assert_cols; apply HNC; ColR).
      split; try (intro; assert_cols; apply HABR; ColR).
      split; Col.
       R; assert_cols; split; Col; Between.
      }

      {
      assert (H1 : B R) by (assert_diffs; auto).
      assert (H2 : Col B R X2) by (assert_cols; Col).
      assert (H3 : Col X1 Q X2) by (assert_cols; Col).
      assert (H := l9_19 B R X1 Q X2 H1 H2 H3); rewrite H.
      assert (R X1) by (intro; assert_cols; apply HNC; ColR).
      split; try (intro; assert_cols; apply HABR; ColR).
      split; try (intro; assert_cols; apply HABR; ColR).
      split; try (intro; subst; apply HBQR; Col).
      Between.
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }

  {
  elim HQX1X2; clear HQX1X2; intro HQX1X2.

    {
    assert (H : TS A R Q B).
      {
      apply l9_8_2 with X2.

        {
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        split; Col.
         R; assert_cols; split; Col; Between.
        }

        {
        assert (H1 : A R) by (assert_diffs; auto).
        assert (H2 : Col A R X1) by (assert_cols; Col).
        assert (H3 : Col X2 Q X1) by (assert_cols; Col).
        assert (H := l9_19 A R X2 Q X1 H1 H2 H3); rewrite H.
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        split; try (intro; subst; apply HAQR; Col).
        Between.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }

    {
    assert (H : TS A R Q B).
      {
      apply l9_8_2 with X2.

        {
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        split; Col.
         R; assert_cols; split; Col; Between.
        }

        {
        assert (H1 : A R) by (assert_diffs; auto).
        assert (H2 : Col A R X1) by (assert_cols; Col).
        assert (H3 : Col X2 Q X1) by (assert_cols; Col).
        assert (H := l9_19 A R X2 Q X1 H1 H2 H3); rewrite H.
        assert (R X2) by (intro; assert_cols; apply HNC; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        split; try (intro; assert_cols; apply HABR; ColR).
        split; try (intro; subst; apply HAQR; Col).
        Between.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_1 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  Col P Q X1
  Col R A X1
  Col P Q X2
  Col R B X2
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABQ HABR HAQR HBQR HCol1 HCol2 HCol3 HCol4.
elim HCol2; clear HCol2; intro HCol2; elim HCol4; clear HCol4; intro HCol4.

  {
  apply coplanar_trans_1_aux_1_1_1 with P X1 X2; assumption.
  }

  {
  elim HCol4; clear HCol4; intro HCol4.

    {
    apply coplanar_trans_1_aux_1_1_2 with P X1 X2; assumption.
    }

    {
    apply coplanar_trans_1_aux_1_1_3 with P X1 X2; assumption.
    }
  }

  {
  elim HCol2; clear HCol2; intro HCol2.

    {
    assert (H : Coplanar Q R B A) by (apply coplanar_trans_1_aux_1_1_2 with P X2 X1; Col; Between); Cop.
    }

    {
    assert (H : Coplanar Q R B A) by (apply coplanar_trans_1_aux_1_1_3 with P X2 X1; Col; Between); Cop.
    }
  }

  {
  elim HCol2; clear HCol2; intro HCol2; elim HCol4; clear HCol4; intro HCol4.

    {
    apply coplanar_trans_1_aux_1_2_2 with P X1 X2; assumption.
    }

    {
    apply coplanar_trans_1_aux_1_2_3 with P X1 X2; assumption.
    }

    {
    assert (H : Coplanar Q R B A) by (apply coplanar_trans_1_aux_1_2_3 with P X2 X1; Col; Between); Cop.
    }

    {
    apply coplanar_trans_1_aux_1_3_3 with P X1 X2; assumption.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_2_1_1_1_1 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet P A X1
  Bet P B X2
  Bet Q X1 X2
  Bet R X1 X2
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
apply between_symmetry in HQX1X2.
apply between_symmetry in HRX1X2.
assert (H : X2 X1) by auto; assert (HQRX1 := l5_2 X2 X1 Q R H HQX1X2 HRX1X2); clear H.
elim HQRX1; clear HQRX1; intro HQRX1.

  {
  apply between_symmetry in HQX1X2.
  assert (H := inner_pasch P Q X2 B X1 HCol3 HQX1X2); destruct H as [U [HBUQ HPUX1]].
  apply between_symmetry in HPUX1.
  assert (H := l5_3 P A U X1 HCol1 HPUX1).
  elim H; clear H; intro HAPU.

    {
    assert (H : TS Q A R B).
      {
      apply l9_31.

        {
        apply one_side_transitivity with P.

          {
          assert (H1 : Q R) by (assert_diffs; auto).
          assert (H2 : Col Q R X1) by (assert_cols; Col).
          assert (H3 : Col A P X1) by (assert_cols; Col).
          assert (H := l9_19 Q R A P X1 H1 H2 H3); rewrite H.
          split; Col.
          split; try assumption.
          split; try (intro; treat_equalities; intuition).
          Between.
          }

          {
          assert (H1 : Q R) by (assert_diffs; auto).
          assert (H2 : Col Q R X2) by (assert_cols; Col).
          assert (H3 : Col P B X2) by (assert_cols; Col).
          assert (H := l9_19 Q R P B X2 H1 H2 H3); rewrite H.
          assert (HQX2 : Q X2) by (intro; treat_equalities; intuition).
          assert (¬ Col B P Q) by (intro; apply HQX2; apply l6_21 with Q R P B; assert_diffs; Col).
          split; Col.
          split; try (intro; treat_equalities; intuition).
          split; Between.
          }
        }

        {
         X2; split.

          {
          apply l9_8_2 with P.

            {
            assert (Q B) by (assert_diffs; auto).
            assert (HQX2 : Q X2) by (intro; treat_equalities; intuition).
            assert (¬ Col B P Q) by (intro; apply HQX2; apply l6_21 with Q R P B; assert_diffs; Col).
            split; Col.
            split; try (intro; assert_cols; apply HBQR; ColR).
             B; split; Col; eBetween.
            }

            {
            assert (H1 : Q B) by (assert_diffs; auto).
            assert (H2 : Col Q B U) by (assert_cols; Col).
            assert (H3 : Col P A U) by (assert_cols; Col).
            assert (H := l9_19 Q B P A U H1 H2 H3); rewrite H.
            assert (HQX2 : Q X2) by (intro; treat_equalities; intuition).
            assert (HBPQ : ¬ Col B P Q) by (intro; apply HQX2; apply l6_21 with Q R P B; assert_diffs; Col).
            split; Col.
            split; try (intro; treat_equalities; apply HBPQ; Col).
            split; try (intro; subst; apply HABQ; Col).
            Between.
            }
          }

          {
          assert (Q B) by (assert_diffs; auto).
          assert (HQX2 : Q X2) by (intro; treat_equalities; intuition).
          assert (¬ Col B P Q) by (intro; apply HQX2; apply l6_21 with Q R P B; assert_diffs; Col).
          split; Col.
          split; try (intro; assert_cols; apply HBQR; ColR).
           Q; split; Col; eBetween.
          }
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }

    {
    assert (H : TS B Q R A).
      {
      apply l9_8_2 with P.

        {
        assert (H1 : B Q) by (assert_diffs; auto).
        assert (HQX2 : Q X2) by (intro; treat_equalities; intuition).
        assert (HBPQ : ¬ Col B P Q) by (intro; apply HQX2; apply l6_21 with Q R P B; assert_diffs; Col).
        split; Col.
        split; Col.
         U; split; Col; Between.
        }

        {
         X2; split.

          {
          assert (B Q) by (assert_diffs; auto).
          assert (HQX2 : Q X2) by (intro; treat_equalities; intuition).
          assert (¬ Col B P Q) by (intro; apply HQX2; apply l6_21 with Q R P B; assert_diffs; Col).
          split; Col.
          split; try (intro; assert_cols; apply HBQR; ColR).
           B; split; Col; eBetween.
          }

          {
          assert (B Q) by (assert_diffs; auto).
          assert (HQX2 : Q X2) by (intro; treat_equalities; intuition).
          assert (¬ Col B P Q) by (intro; apply HQX2; apply l6_21 with Q R P B; assert_diffs; Col).
          split; Col.
          split; try (intro; assert_cols; apply HBQR; ColR).
           Q; split; Col; eBetween.
          }
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }

  {
  apply between_symmetry in HRX1X2.
  assert (H := inner_pasch P R X2 B X1 HCol3 HRX1X2); destruct H as [U [HBUR HPUX1]].
  apply between_symmetry in HPUX1.
  assert (H := l5_3 P A U X1 HCol1 HPUX1).
  elim H; clear H; intro HAPU.

    {
    assert (H : TS R A Q B).
      {
      apply l9_31.

        {
        apply one_side_transitivity with P.

          {
          assert (H1 : R Q) by (assert_diffs; auto).
          assert (H2 : Col R Q X1) by (assert_cols; Col).
          assert (H3 : Col A P X1) by (assert_cols; Col).
          assert (H := l9_19 R Q A P X1 H1 H2 H3); rewrite H.
          split; Col.
          split; try assumption.
          split; try (intro; treat_equalities; intuition).
          Between.
          }

          {
          assert (H1 : R Q) by (assert_diffs; auto).
          assert (H2 : Col R Q X2) by (assert_cols; Col).
          assert (H3 : Col P B X2) by (assert_cols; Col).
          assert (H := l9_19 R Q P B X2 H1 H2 H3); rewrite H.
          assert (HQX2 : Q X2) by (intro; treat_equalities; intuition).
          assert (¬ Col B P Q) by (intro; apply HQX2; apply l6_21 with Q R P B; assert_diffs; Col).
          split; Col.
          split; try (intro; treat_equalities; intuition).
          split; Between.
          }
        }

        {
         X2; split.

          {
          apply l9_8_2 with P.

            {
            assert (R B) by (assert_diffs; auto).
            assert (HRX2 : R X2) by (intro; treat_equalities; intuition).
            assert (¬ Col B P R) by (intro; apply HRX2; apply l6_21 with Q R P B; assert_diffs; Col).
            split; Col.
            split; try (intro; assert_cols; apply HBQR; ColR).
             B; split; Col; eBetween.
            }

            {
            assert (H1 : R B) by (assert_diffs; auto).
            assert (H2 : Col R B U) by (assert_cols; Col).
            assert (H3 : Col P A U) by (assert_cols; Col).
            assert (H := l9_19 R B P A U H1 H2 H3); rewrite H.
            assert (HRX2 : R X2) by (intro; treat_equalities; intuition).
            assert (HBPR : ¬ Col B P R) by (intro; apply HRX2; apply l6_21 with Q R P B; assert_diffs; Col).
            split; Col.
            split; try (intro; treat_equalities; apply HABP; Col).
            split; try (intro; treat_equalities; apply HABR; Col).
            Between.
            }
          }

          {
          assert (R B) by (assert_diffs; auto).
          assert (HRX2 : R X2) by (intro; treat_equalities; intuition).
          assert (¬ Col B P R) by (intro; apply HRX2; apply l6_21 with Q R P B; assert_diffs; Col).
          split; Col.
          split; try (intro; assert_cols; apply HBQR; ColR).
           R; split; Col; eBetween.
          }
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }

    {
    assert (H : TS B R Q A).
      {
      apply l9_8_2 with P.

        {
        assert (H1 : B R) by (assert_diffs; auto).
        assert (HRX2 : R X2) by (intro; treat_equalities; intuition).
        assert (HBPR : ¬ Col B P R) by (intro; apply HRX2; apply l6_21 with Q R P B; assert_diffs; Col).
        split; Col.
        split; Col.
         U; split; Col; Between.
        }

        {
         X2; split.

          {
          assert (B R) by (assert_diffs; auto).
          assert (HRX2 : R X2) by (intro; treat_equalities; intuition).
          assert (¬ Col B P R) by (intro; apply HRX2; apply l6_21 with Q R P B; assert_diffs; Col).
          split; Col.
          split; try (intro; assert_cols; apply HBQR; ColR).
           B; split; Col; eBetween.
          }

          {
          assert (B R) by (assert_diffs; auto).
          assert (HRX2 : R X2) by (intro; treat_equalities; intuition).
          assert (¬ Col B P R) by (intro; apply HRX2; apply l6_21 with Q R P B; assert_diffs; Col).
          split; Col.
          split; try (intro; assert_cols; apply HBQR; ColR).
           R; split; Col; eBetween.
          }
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_2_1_1_1_2 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet P A X1
  Bet P B X2
  Bet Q X1 X2
  Bet X1 X2 R
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
assert (H := outer_pasch X1 P X2 R B HRX1X2 HCol3); destruct H as [U [HPUX1 HRBU]].
apply between_symmetry in HPUX1.
assert (H := l5_3 P A U X1 HCol1 HPUX1).
elim H; clear H; intro HAPU.

  {
  assert (H : TS B R Q A).
    {
    apply l9_8_2 with X1.

      {
      assert (H1 : B R) by (assert_diffs; auto).
      assert (HRX1 : R X1) by (intro; treat_equalities; intuition).
      split; try (intro; apply HBQR; ColR).
      split; Col.
       U; split; Col; eBetween.
      }

      {
      assert (H1 : B R) by (assert_diffs; auto).
      assert (H2 : Col B R R) by Col.
      assert (H3 : Col X1 Q R) by (assert_cols; Col).
      assert (H := l9_19 B R X1 Q R H1 H2 H3); rewrite H.
      assert (HRX2 : R X1) by (intro; treat_equalities; intuition).
      split; try (intro; apply HBQR; ColR).
      split; try auto.
      split; assert_diffs; eBetween.
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }

  {
  assert (H : TS R A Q B).
    {
    apply l9_31.

      {
      apply one_side_transitivity with P.

        {
        assert (H1 : R Q) by (assert_diffs; auto).
        assert (H2 : Col R Q X1) by (assert_cols; Col).
        assert (H3 : Col A P X1) by (assert_cols; Col).
        assert (H := l9_19 R Q A P X1 H1 H2 H3); rewrite H.
        split; Col.
        split; try assumption.
        split; try (intro; treat_equalities; intuition).
        Between.
        }

        {
        assert (H1 : R Q) by (assert_diffs; auto).
        assert (H2 : Col R Q X2) by (assert_cols; Col).
        assert (H3 : Col P B X2) by (assert_cols; Col).
        assert (H := l9_19 R Q P B X2 H1 H2 H3); rewrite H.
        assert (HQX2 : Q X2) by (intro; treat_equalities; intuition).
        assert (¬ Col B P Q) by (intro; apply HQX2; apply l6_21 with Q R P B; assert_diffs; Col).
        split; Col.
        split; try (intro; treat_equalities; intuition).
        split; Between.
        }
      }

      {
      apply one_side_transitivity with X1.

        {
        assert (H1 : R B) by (assert_diffs; auto).
        assert (H2 : Col R B U) by (assert_cols; Col).
        assert (HBet : Bet U A X1) by eBetween.
        assert (H3 : Col A X1 U) by (assert_cols; Col).
        assert (H := l9_19 R B A X1 U H1 H2 H3); rewrite H.
        split; Col.
        split; try (intro; treat_equalities; intuition).
        split; try (intro; treat_equalities; intuition).
        Between.
        }

        {
        assert (H1 : R B) by (assert_diffs; auto).
        assert (H2 : Col R B R) by Col.
        assert (H3 : Col X1 Q R) by (assert_cols; Col).
        assert (H := l9_19 R B X1 Q R H1 H2 H3); rewrite H.
        assert (HRX1 : R X1) by (intro; treat_equalities; intuition).
        split; try (intro; apply HBQR; ColR).
        split; try auto.
        split; assert_diffs; eBetween.
        }
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }
Qed.

Lemma coplanar_trans_1_aux_2_1_1_1_3 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet P A X1
  Bet P B X2
  Bet Q X1 X2
  Bet X2 R X1
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
elim (eq_dec_points R X1); intro HRX1; elim (eq_dec_points R X2); intro HRX2; treat_equalities.

  {
  subst; intuition.
  }

  {
  assert (H := inner_pasch P Q X2 B R HCol3 HQX1X2); destruct H as [U [HBUQ HPUR]].
   U; right; right.
  assert (P R) by (intro; treat_equalities; intuition).
  split; assert_cols; ColR.
  }

  {
  apply between_symmetry in HQX1X2.
  assert (H := outer_pasch R P X1 Q A HQX1X2 HCol1); destruct H as [U [HPUR HQAU]].
   U; right; left.
  assert (P R) by (intro; treat_equalities; intuition).
  split; assert_cols; ColR.
  }

  {
  assert (H : TS R A Q B).

    {
    apply l9_31.

      {
      apply one_side_transitivity with P.

        {
        assert (H1 : R Q) by (assert_diffs; auto).
        assert (H2 : Col R Q X1) by (assert_cols; Col).
        assert (H3 : Col A P X1) by (assert_cols; Col).
        assert (H := l9_19 R Q A P X1 H1 H2 H3); rewrite H.
        split; Col.
        split; try assumption.
        split; try (intro; treat_equalities; intuition).
        Between.
        }

        {
        assert (H1 : R Q) by (assert_diffs; auto).
        assert (H2 : Col R Q X2) by (assert_cols; Col).
        assert (H3 : Col P B X2) by (assert_cols; Col).
        assert (H := l9_19 R Q P B X2 H1 H2 H3); rewrite H.
        assert (HQX2 : Q X2) by (intro; treat_equalities; intuition).
        assert (¬ Col B P Q) by (intro; apply HQX2; apply l6_21 with Q R P B; assert_diffs; Col).
        split; Col.
        split; try (intro; treat_equalities; intuition).
        split; Between.
        }
      }

      {
      apply one_side_transitivity with X1.

        {
        apply one_side_symmetry; apply l9_17 with P; Between.
         X2; split.

          {
          assert (H1 : R B) by (assert_diffs; auto).
          split; try (intro; apply HBQR; ColR).
          split; try (intro; apply HBQR; ColR).
           R; split; Col; Between.
          }

          {
          assert (H1 : R B) by (assert_diffs; auto).
          split; try (intro; apply HRX2; apply l6_21 with Q R P B; assert_diffs; Col).
          split; try (intro; apply HBQR; ColR).
           B; split; Col; Between.
          }
        }

        {
         X2; split.

          {
          assert (H1 : R B) by (assert_diffs; auto).
          split; try (intro; apply HBQR; ColR).
          split; try (intro; apply HBQR; ColR).
           R; split; Col; Between.
          }

          {
          assert (H1 : R B) by (assert_diffs; auto).
          split; try (intro; apply HBQR; ColR).
          split; try (intro; apply HBQR; ColR).
           R; split; Col; eBetween.
          }
        }
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }
Qed.

Unset Regular Subst Tactic.

Lemma coplanar_trans_1_aux_2_1_1_2_2 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet P A X1
  Bet P B X2
  Bet X2 Q X1
  Bet X2 R X1
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
assert (H := l5_3 X2 Q R X1 HQX1X2 HRX1X2).
apply between_symmetry in HQX1X2.
apply between_symmetry in HRX1X2.
assert (H' := l5_3 X1 Q R X2 HQX1X2 HRX1X2).
elim H; clear H; intro HQRX2; elim H'; clear H'; intro HQRX1.

  {
  assert (H : Bet X1 R Q) by eBetween.
  apply between_symmetry in HQRX1.
  apply between_symmetry in H.
  assert (H' := between_equality R Q X1 HQRX1 H); treat_equalities; exfalso; apply HNC; Col.
  }

  {
  elim (eq_dec_points R X1); intro HRX1; elim (eq_dec_points R X2); intro HRX2; treat_equalities.

    {
    subst; intuition.
    }

    {
    apply between_symmetry in HCol1.
    apply between_symmetry in HCol3.
    assert (H := inner_pasch R X2 P A B HCol1 HCol3); destruct H as [U [HAUX2 HBUR]].
    assert (T: Bet R Q X2) by Between.
    assert (H := inner_pasch A R X2 U Q HAUX2 T); destruct H as [V [RVU HAVQ]].
     V; right; left.
    assert (R U) by (intro; treat_equalities; assert_cols; apply HAQR; ColR).
    assert_cols; split; ColR.
    }

    {
    exfalso; apply HNC; Col.
    }

    {
    assert (H : TS R B Q A).

      {
      apply l9_31.

        {
        apply one_side_transitivity with P.

          {
          assert (H1 : R Q) by (assert_diffs; auto).
          assert (H2 : Col R Q X2) by (assert_cols; Col).
          assert (H3 : Col B P X2) by (assert_cols; Col).
          assert (H := l9_19 R Q B P X2 H1 H2 H3); rewrite H.
          split; Col.
          split; try (intro; treat_equalities; intuition).
          split; Between.
          intro; treat_equalities; intuition.
          }

          {
          assert (H1 : R Q) by (assert_diffs; auto).
          assert (H2 : Col R Q X1) by (assert_cols; Col).
          assert (H3 : Col P A X1) by (assert_cols; Col).
          assert (H := l9_19 R Q P A X1 H1 H2 H3); rewrite H.
          split; Col.
          split; try (intro; treat_equalities; intuition).
          split; Between.
          }
        }

        {
         X1; split.

          {
          apply l9_8_2 with P.

            {
            assert (H1 : R A) by (assert_diffs; auto).
            split; try (intro; apply HRX1; apply l6_21 with Q R P A; assert_diffs; Col).
            split; try (intro; apply HAQR; ColR).
             A; split; Col; Between.
            }

            {
            apply l9_17 with X2; Between.
             X1; split.

              {
              assert (H1 : R A) by (assert_diffs; auto).
              split; try (intro; apply HRX1; apply l6_21 with Q R P A; assert_diffs; Col).
              split; try (intro; apply HAQR; ColR).
               A; split; Col; Between.
              }

              {
              assert (H1 : R A) by (assert_diffs; auto).
              split; try (intro; apply HAQR; ColR).
              split; try (intro; apply HAQR; ColR).
               R; split; Col; Between.
              }
            }
          }

          {
          assert (H1 : R A) by (assert_diffs; auto).
          split; try (intro; apply HAQR; ColR).
          split; try (intro; apply HAQR; ColR).
           R; split; Col; eBetween.
          }
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }

  {
  elim (eq_dec_points Q X1); intro HQX1; elim (eq_dec_points Q X2); intro HQX2; treat_equalities.

    {
    subst; intuition.
    }

    {
    apply between_symmetry in HCol1.
    apply between_symmetry in HCol3.
    assert (H := inner_pasch X2 Q P B A HCol3 HCol1); destruct H as [U [HBUQ HAUX2]].
    assert (T:Bet Q R X2) by auto using between_symmetry.
    assert (H := inner_pasch A Q X2 U R HAUX2 T); destruct H as [V [QVU HAVR]].
     V; right; right.
    assert (Q U) by (intro; treat_equalities; assert_cols; apply HAQR; ColR).
    assert_cols; split; ColR.
    }

    {
    exfalso; apply HNC; Col.
    }

    {
    assert (H : TS Q B R A).

      {
      apply l9_31.

        {
        apply one_side_transitivity with P.

          {
          assert (H1 : Q R) by (assert_diffs; auto).
          assert (H2 : Col Q R X2) by (assert_cols; Col).
          assert (H3 : Col B P X2) by (assert_cols; Col).
          assert (H := l9_19 Q R B P X2 H1 H2 H3); rewrite H.
          split; Col.
          split; try (intro; treat_equalities; intuition).
          split; Between.
          intro; treat_equalities; intuition.
          }

          {
          assert (H1 : Q R) by (assert_diffs; auto).
          assert (H2 : Col Q R X1) by (assert_cols; Col).
          assert (H3 : Col P A X1) by (assert_cols; Col).
          assert (H := l9_19 Q R P A X1 H1 H2 H3); rewrite H.
          split; Col.
          split; try (intro; treat_equalities; intuition).
          split; Between.
          }
        }

        {
         X1; split.

          {
          apply l9_8_2 with P.

            {
            assert (H1 : Q A) by (assert_diffs; auto).
            split; try (intro; apply HQX1; apply l6_21 with Q R P A; assert_diffs; Col).
            split; try (intro; apply HAQR; ColR).
             A; split; Col; Between.
            }

            {
            apply l9_17 with X2; Between.
             X1; split.

              {
              assert (H1 : Q A) by (assert_diffs; auto).
              split; try (intro; apply HQX1; apply l6_21 with Q R P A; assert_diffs; Col).
              split; try (intro; apply HAQR; ColR).
               A; split; Col; Between.
              }

              {
              assert (H1 : Q A) by (assert_diffs; auto).
              split; try (intro; apply HAQR; ColR).
              split; try (intro; apply HAQR; ColR).
               Q; split; Col; Between.
              }
            }
          }

          {
          assert (H1 : Q A) by (assert_diffs; auto).
          split; try (intro; apply HAQR; ColR).
          split; try (intro; apply HAQR; ColR).
           Q; split; Col; Between.
          }
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }

  {
  assert (H : Bet X1 Q R) by eBetween.
  apply between_symmetry in HQRX1.
  apply between_symmetry in H.
  assert (H' := between_equality R Q X1 H HQRX1); treat_equalities; exfalso; apply HNC; Col.
  }
Qed.

Lemma coplanar_trans_1_aux_2_1_1 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet P A X1
  Bet P B X2
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2 HCol2 HCol4 HCol1 HCol3.
assert (HQX1X2 : Col Q X1 X2) by (assert_diffs; ColR).
assert (HRX1X2 : Col R X1 X2) by (assert_diffs; ColR).
elim HQX1X2; clear HQX1X2; intro HQX1X2; elim HRX1X2; clear HRX1X2; intro HRX1X2.

  {
  apply coplanar_trans_1_aux_2_1_1_1_1 with P X1 X2; assumption.
  }

  {
  elim HRX1X2; clear HRX1X2; intro HRX1X2.

    {
    apply coplanar_trans_1_aux_2_1_1_1_2 with P X1 X2; assumption.
    }

    {
    apply coplanar_trans_1_aux_2_1_1_1_3 with P X1 X2; assumption.
    }
  }

  {
  elim HQX1X2; clear HQX1X2; intro HQX1X2.

    {
    assert (Coplanar Q R B A) by (apply coplanar_trans_1_aux_2_1_1_1_2 with P X2 X1; Col; Between); Cop.
    }

    {
    assert (Coplanar R Q A B) by (apply coplanar_trans_1_aux_2_1_1_1_3 with P X1 X2; Col; Between); Cop.
    }
  }

  {
  elim HQX1X2; clear HQX1X2; intro HQX1X2; elim HRX1X2; clear HRX1X2; intro HRX1X2.

    {
    assert (Coplanar Q R B A) by (apply coplanar_trans_1_aux_2_1_1_1_1 with P X2 X1; Col; Between); Cop.
    }

    {
    assert (Coplanar Q R B A) by (apply coplanar_trans_1_aux_2_1_1_1_3 with P X2 X1; Col; Between); Cop.
    }

    {
    assert (Coplanar R Q B A) by (apply coplanar_trans_1_aux_2_1_1_1_3 with P X2 X1; Col; Between); Cop.
    }

    {
    apply coplanar_trans_1_aux_2_1_1_2_2 with P X1 X2; assumption.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_2_1_2 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet P A X1
  Bet B X2 P
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2 HCol2 HCol4 HCol1 HCol3.
assert (H : TS Q R A B).
  {
  apply l9_8_2 with P.

    {
    assert (H1 : Q R) by (assert_diffs; auto).
    split; Col.
    split; Col.
     X2; split; Col; Between.
    }

    {
    assert (H1 : Q R) by (assert_diffs; auto).
    assert (H2 : Col Q R X1) by (assert_cols; Col).
    assert (H3 : Col P A X1) by (assert_cols; Col).
    assert (H := l9_19 Q R P A X1 H1 H2 H3); rewrite H.
    split; Col.
    split; try (intro; treat_equalities; intuition).
    split; Between.
    }
  }
destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
I; assert_cols; Col5.
Qed.

Lemma coplanar_trans_1_aux_2_1_3_1_1 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet P A X1
  Bet X2 P B
  Bet Q X1 X2
  Bet R X1 X2
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
assert (HOS : OS Q R A B).
  {
  apply one_side_transitivity with P.

    {
    assert (H1 : Q R) by (assert_diffs; auto).
    assert (H2 : Col Q R X1) by (assert_cols; Col).
    assert (H3 : Col A P X1) by (assert_cols; Col).
    assert (H := l9_19 Q R A P X1 H1 H2 H3); rewrite H.
    split; Col.
    split; try (intro; treat_equalities; intuition).
    split; try (intro; treat_equalities; apply HAX1; reflexivity).
    Between.
    }

    {
    assert (H1 : Q R) by (assert_diffs; auto).
    assert (H2 : Col Q R X2) by (assert_cols; Col).
    assert (H3 : Col P B X2) by (assert_cols; Col).
    assert (H := l9_19 Q R P B X2 H1 H2 H3); rewrite H.
    split; Col.
    split; try (intro; treat_equalities; intuition).
    split; Between.
    }
  }
apply between_symmetry in HQX1X2.
apply between_symmetry in HRX1X2.
assert (H : X2 X1) by auto; assert (HQRX1 := l5_2 X2 X1 Q R H HQX1X2 HRX1X2); clear H.
elim HQRX1; clear HQRX1; intro HQRX1.

  {
  assert (H : TS Q B R A).
    {
    apply l9_31; apply one_side_symmetry; try assumption.
     X2; split.

      {
      assert (H1 : Q A) by (assert_diffs; auto).
      split; Col.
      assert (Q X2) by (intro; treat_equalities; apply HX1X2; reflexivity).
      split; try (intro; apply HAQR; ColR).
       Q; split; Col; eBetween.
      }

      {
      assert (H := outer_pasch X2 P X1 Q A HQX1X2 HCol1); destruct H as [U [HPUX2 HQAU]].
      assert (H1 : Q A) by (assert_diffs; auto).
      split; Col.
      assert (Q X2) by (intro; treat_equalities; apply HX1X2; reflexivity).
      split; try (intro; apply HAQR; ColR).
       U; split; Col; eBetween.
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }

  {
  assert (H : TS R B Q A).
    {
    apply l9_31; apply one_side_symmetry; apply invert_one_side; try assumption.
     X2; split.

      {
      assert (H1 : A R) by (assert_diffs; auto).
      split; Col.
      assert (R X2) by (intro; treat_equalities; apply HX1X2; reflexivity).
      split; try (intro; apply HAQR; ColR).
       R; split; Col; eBetween.
      }

      {
      assert (H := outer_pasch X2 P X1 R A HRX1X2 HCol1); destruct H as [U [HPUX2 HRAU]].
      assert (H1 : A R) by (assert_diffs; auto).
      split; Col.
      assert (R X2) by (intro; treat_equalities; apply HX1X2; reflexivity).
      split; try (intro; apply HAQR; ColR).
       U; split; Col; eBetween.
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }
Qed.

Lemma coplanar_trans_1_aux_2_1_3_1_2 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet P A X1
  Bet X2 P B
  Bet Q X1 X2
  Bet X1 X2 R
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
assert (H : TS A Q R B).
  {
  apply l9_8_2 with X2.

    {
    apply between_symmetry in HQX1X2.
    assert (H := outer_pasch X2 P X1 Q A HQX1X2 HCol1); destruct H as [U [HPUX2 HQAU]].
    assert (H1 : A Q) by (assert_diffs; auto).
    assert (Q X2) by (intro; treat_equalities; apply HX1X2; reflexivity).
    split; try (intro; apply HAQR; ColR).
    split; Col.
     U; split; Col; eBetween.
    }

    {
    assert (H1 : A Q) by (assert_diffs; auto).
    assert (H2 : Col A Q Q) by (assert_cols; Col).
    assert (H3 : Col X2 R Q) by (assert_cols; Col).
    assert (H := l9_19 A Q X2 R Q H1 H2 H3); rewrite H.
    assert (Q X2) by (intro; treat_equalities; apply HX1X2; reflexivity).
    split; try (intro; apply HAQR; ColR).
    split; auto.
    split; try (intro; treat_equalities; intuition).
    eBetween.
    }
  }
destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
I; assert_cols; Col5.
Qed.

Lemma coplanar_trans_1_aux_2_1_3_1_3 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet P A X1
  Bet X2 P B
  Bet Q X1 X2
  Bet X2 R X1
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
assert (H : TS A Q R B).
  {
  apply l9_8_2 with X2.

    {
    apply between_symmetry in HQX1X2.
    assert (H := outer_pasch X2 P X1 Q A HQX1X2 HCol1); destruct H as [U [HPUX2 HQAU]].
    assert (H1 : A Q) by (assert_diffs; auto).
    assert (Q X2) by (intro; treat_equalities; apply HX1X2; reflexivity).
    split; try (intro; apply HAQR; ColR).
    split; Col.
     U; split; Col; eBetween.
    }

    {
    assert (H1 : A Q) by (assert_diffs; auto).
    assert (H2 : Col A Q Q) by (assert_cols; Col).
    assert (H3 : Col X2 R Q) by (assert_cols; Col).
    assert (H := l9_19 A Q X2 R Q H1 H2 H3); rewrite H.
    assert (Q X2) by (intro; treat_equalities; apply HX1X2; reflexivity).
    split; try (intro; apply HAQR; ColR).
    split; auto.
    split; try (intro; treat_equalities; intuition).
    eBetween.
    }
  }
destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
I; assert_cols; Col5.
Qed.

Lemma coplanar_trans_1_aux_2_1_3_2_2 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet P A X1
  Bet X2 P B
  Bet X1 X2 Q
  Bet X1 X2 R
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
assert (HQRX2 := l5_2 X1 X2 Q R HX1X2 HQX1X2 HRX1X2).
assert (HOS : OS Q R A B).
  {
  apply one_side_transitivity with P.

    {
    assert (H1 : Q R) by (assert_diffs; auto).
    assert (H2 : Col Q R X1) by (assert_cols; Col).
    assert (H3 : Col A P X1) by (assert_cols; Col).
    assert (H := l9_19 Q R A P X1 H1 H2 H3); rewrite H.
    split; Col.
    split; try (intro; treat_equalities; intuition).
    split; try (intro; treat_equalities; apply HAX1; reflexivity).
    Between.
    }

    {
    assert (H1 : Q R) by (assert_diffs; auto).
    assert (H2 : Col Q R X2) by (assert_cols; Col).
    assert (H3 : Col P B X2) by (assert_cols; Col).
    assert (H := l9_19 Q R P B X2 H1 H2 H3); rewrite H.
    split; Col.
    split; try (intro; treat_equalities; intuition).
    split; Between.
    }
  }
elim HQRX2; clear HQRX2; intro HQRX2.

  {
  elim (eq_dec_points Q X2); intro HQX2; treat_equalities.

    {
    apply between_symmetry in HRX1X2.
    assert (H := inner_pasch P R X1 A Q HCol1 HRX1X2); destruct H as [U [HAUR HPUQ]].
     U; right; right.
    assert (P Q) by (assert_diffs; auto).
    assert_cols; split; ColR.
    }

    {
    assert (H : TS Q B R A).
      {
      apply l9_31; apply one_side_symmetry; try assumption.
       X2; split.

        {
        assert (H1 : Q A) by (assert_diffs; auto).
        split; Col.
        split; try (intro; apply HAQR; ColR).
         Q; split; Col; eBetween.
        }

        {
        apply between_symmetry in HQX1X2.
        assert (H := inner_pasch P Q X1 A X2 HCol1 HQX1X2); destruct H as [U [HAUQ HPUX2]].
        assert (H1 : Q A) by (assert_diffs; auto).
        split; Col.
        split; try (intro; apply HAQR; ColR).
         U; split; Col; eBetween.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }

  {
  elim (eq_dec_points R X2); intro HRX2; treat_equalities.

    {
    apply between_symmetry in HQX1X2.
    assert (H := inner_pasch P Q X1 A R HCol1 HQX1X2); destruct H as [U [HAUQ HPUR]].
     U; right; left.
    assert (P R) by (assert_diffs; auto).
    assert_cols; split; ColR.
    }

    {
    assert (H : TS R B Q A).
      {
      apply l9_31; apply one_side_symmetry; apply invert_one_side; try assumption.
       X2; split.

        {
        assert (H1 : A R) by (assert_diffs; auto).
        split; Col.
        split; try (intro; apply HAQR; ColR).
         R; split; Col; eBetween.
        }

        {
        apply between_symmetry in HRX1X2.
        assert (H := inner_pasch P R X1 A X2 HCol1 HRX1X2); destruct H as [U [HAUR HPUX2]].
        assert (H1 : A R) by (assert_diffs; auto).
        split; Col.
        split; try (intro; apply HAQR; ColR).
         U; split; Col; eBetween.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_2_1_3_2_3 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet P A X1
  Bet X2 P B
  Bet X1 X2 Q
  Bet X2 R X1
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
assert (HOS : OS Q R A B).
  {
  apply one_side_transitivity with P.

    {
    assert (H1 : Q R) by (assert_diffs; auto).
    assert (H2 : Col Q R X1) by (assert_cols; Col).
    assert (H3 : Col A P X1) by (assert_cols; Col).
    assert (H := l9_19 Q R A P X1 H1 H2 H3); rewrite H.
    split; Col.
    split; try (intro; treat_equalities; intuition).
    split; try (intro; treat_equalities; apply HAX1; reflexivity).
    Between.
    }

    {
    assert (H1 : Q R) by (assert_diffs; auto).
    assert (H2 : Col Q R X2) by (assert_cols; Col).
    assert (H3 : Col P B X2) by (assert_cols; Col).
    assert (H := l9_19 Q R P B X2 H1 H2 H3); rewrite H.
    split; Col.
    split; try (intro; treat_equalities; intuition).
    split; Between.
    }
  }
elim (eq_dec_points Q X2); intro HQX2; treat_equalities.

  {
  assert (H := inner_pasch P Q X1 A R HCol1 HRX1X2); destruct H as [U [HAUQ HPUR]].
  apply between_symmetry in HCol3.
  assert (H := outer_pasch B R P Q U HCol3 HPUR); destruct H as [V [HBVR HQUV]].
   V; right; left.
  assert (Q U) by (intro; treat_equalities; assert_cols; apply HNC; Col).
  assert_cols; split; ColR.
  }

  {
  assert (H : TS Q A B R).
    {
    apply l9_31; try assumption.
    apply one_side_transitivity with P.

      {
      apply between_symmetry in HQX1X2.
      apply between_symmetry in HCol3.
      assert (H := outer_pasch Q B X2 X1 P HQX1X2 HCol3); destruct H as [U [HBUQ HUPX1]].
      assert (H1 : Q B) by (assert_diffs; auto).
      assert (H2 : Col Q B U) by (assert_cols; Col).
      assert (H' : P X1) by (intro; treat_equalities; apply HAX1; reflexivity).
      assert (H3 : Col A P U) by (assert_cols; ColR).
      assert (H := l9_19 Q B A P U H1 H2 H3); rewrite H.
      split; Col.
      split; try (intro; treat_equalities; apply HABQ; Col).
      split; try (intro; treat_equalities; apply HQX2; apply l6_21 with Q R P B; assert_diffs; Col).
      eBetween.
      }

      {
      apply one_side_transitivity with X2.

        {
        assert (H1 : Q B) by (assert_diffs; auto).
        assert (H2 : Col Q B B) by (assert_cols; Col).
        assert (H3 : Col P X2 B) by (assert_cols; Col).
        assert (H := l9_19 Q B P X2 B H1 H2 H3); rewrite H.
        split; try (intro; treat_equalities; apply HQX2; apply l6_21 with Q R P B; assert_diffs; Col).
        split; try (intro; treat_equalities; apply HABP; Col).
        split; Between.
        }

        {
        assert (H1 : Q B) by (assert_diffs; auto).
        assert (H2 : Col Q B Q) by (assert_cols; Col).
        assert (H3 : Col X2 R Q) by (assert_cols; Col).
        assert (H := l9_19 Q B X2 R Q H1 H2 H3); rewrite H.
        split; try (intro; apply HBQR; ColR).
        split; auto.
        split; try (intro; assert_diffs; intuition).
        eBetween.
        }
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }
Qed.

Lemma coplanar_trans_1_aux_2_1_3_3_3 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet P A X1
  Bet X2 P B
  Bet X2 Q X1
  Bet X2 R X1
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
assert (HOS : OS Q R A B).
  {
  apply one_side_transitivity with P.

    {
    assert (H1 : Q R) by (assert_diffs; auto).
    assert (H2 : Col Q R X1) by (assert_cols; Col).
    assert (H3 : Col A P X1) by (assert_cols; Col).
    assert (H := l9_19 Q R A P X1 H1 H2 H3); rewrite H.
    split; Col.
    split; try (intro; treat_equalities; intuition).
    split; try (intro; treat_equalities; apply HAX1; reflexivity).
    Between.
    }

    {
    assert (H1 : Q R) by (assert_diffs; auto).
    assert (H2 : Col Q R X2) by (assert_cols; Col).
    assert (H3 : Col P B X2) by (assert_cols; Col).
    assert (H := l9_19 Q R P B X2 H1 H2 H3); rewrite H.
    split; Col.
    split; try (intro; treat_equalities; intuition).
    split; Between.
    }
  }
assert (H := l5_3 X2 Q R X1 HQX1X2 HRX1X2).
apply between_symmetry in HQX1X2.
apply between_symmetry in HRX1X2.
assert (H' := l5_3 X1 Q R X2 HQX1X2 HRX1X2).
elim H'; clear H'; intro HQRX1; elim H; clear H; intro HQRX2.

  {
  assert (H : Bet X1 R Q) by eBetween.
  apply between_symmetry in HQRX1.
  apply between_symmetry in H.
  assert (H' := between_equality R Q X1 HQRX1 H); treat_equalities; exfalso; apply HNC; Col.
  }

  {
  apply between_symmetry in HCol3.
  assert (H := inner_pasch B X1 X2 P Q HCol3 HQX1X2); destruct H as [U [HPUX1 HBUQ]].
  assert (H := l5_3 P A U X1 HCol1 HPUX1).
  elim H; clear H; intro HAPU.

    {
    elim (eq_dec_points Q X2); intro HQX2; treat_equalities.

      {
      exfalso; apply HNC; Col.
      }

      {
      assert (H : TS Q A B R).
        {
        apply l9_31; try assumption.
        apply one_side_transitivity with P.

          {
          assert (H1 : Q B) by (assert_diffs; auto).
          assert (H2 : Col Q B U) by (assert_cols; Col).
          assert (H3 : Col A P U) by (assert_cols; Col).
          assert (H := l9_19 Q B A P U H1 H2 H3); rewrite H.
          split; Col.
          split; try (intro; treat_equalities; apply HABQ; ColR).
          split; try (intro; treat_equalities; apply HABP; Col).
          Between.
          }

          {
          apply one_side_transitivity with X2.

            {
            assert (H1 : Q B) by (assert_diffs; auto).
            assert (H2 : Col Q B B) by (assert_cols; Col).
            assert (H3 : Col P X2 B) by (assert_cols; Col).
            assert (H := l9_19 Q B P X2 B H1 H2 H3); rewrite H.
            split; try (intro; treat_equalities; apply HQX2; apply l6_21 with Q R P B; assert_diffs; Col).
            split; try (intro; treat_equalities; apply HABP; Col).
            split; Between.
            }

            {
            assert (H1 : Q B) by (assert_diffs; auto).
            assert (H2 : Col Q B Q) by (assert_cols; Col).
            assert (H3 : Col X2 R Q) by (assert_cols; Col).
            assert (H := l9_19 Q B X2 R Q H1 H2 H3); rewrite H.
            split; try (intro; apply HBQR; ColR).
            split; try auto.
            split; try (intro; treat_equalities; intuition).
            Between.
            }
          }
        }
      destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
       I; assert_cols; Col5.
      }
    }

    {
    elim (eq_dec_points Q X1); intro HQX1; treat_equalities.

      {
        
      assert (T: Bet Q R X2) by auto using between_symmetry.
      assert (H := inner_pasch B Q X2 P R HCol3 T); destruct H as [V [HPVQ HBVR]].
       V; right; left.
      assert_diffs; assert_cols; split; ColR.
      }

      {
      assert (H : TS Q B A R).
        {
        apply l9_8_2 with X1.

          {
          assert (H1 : Q B) by (assert_diffs; auto).
          split; try (intro; apply HBQR; ColR).
          split; Col.
           Q; split; Col; Between.
          }

          {
          assert (H1 : Q B) by (assert_diffs; auto).
          assert (H2 : Col Q B U) by (assert_cols; Col).
          assert (H' : P X1) by (intro; treat_equalities; apply HAX1; reflexivity).
          assert (H3 : Col X1 A U) by (assert_cols; ColR).
          assert (H := l9_19 Q B X1 A U H1 H2 H3); rewrite H.
          split; try (intro; apply HBQR; ColR).
          split; try (intro; treat_equalities; apply HBQR; ColR).
          split; try (intro; treat_equalities; apply HABQ; Col).
          eBetween.
          }
        }
      destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
       I; assert_cols; Col5.
      }
    }
  }

  {
  apply between_symmetry in HCol3.
  assert (H := inner_pasch B X1 X2 P R HCol3 HRX1X2); destruct H as [U [HPUX1 HBUR]].
  assert (H := l5_3 P A U X1 HCol1 HPUX1).
  elim H; clear H; intro HAPU.

    {
    elim (eq_dec_points R X2); intro HRX2; treat_equalities; Cop.
    assert (H : TS R A B Q).
      {
      apply l9_31; apply invert_one_side; try assumption.
      apply one_side_transitivity with P.

        {
        assert (H1 : B R) by (assert_diffs; auto).
        assert (H2 : Col B R U) by (assert_cols; Col).
        assert (H3 : Col A P U) by (assert_cols; Col).
        assert (H := l9_19 B R A P U H1 H2 H3); rewrite H.
        split; Col.
        split; try (intro; treat_equalities; apply HABR; Col).
        split; try (intro; treat_equalities; apply HABP; Col).
        Between.
        }

        {
        apply one_side_transitivity with X2.

          {
          assert (H1 : B R) by (assert_diffs; auto).
          assert (H2 : Col B R B) by (assert_cols; Col).
          assert (H3 : Col P X2 B) by (assert_cols; Col).
          assert (H := l9_19 B R P X2 B H1 H2 H3); rewrite H.
          split; try (intro; treat_equalities; apply HRX2; apply l6_21 with Q R P B; assert_diffs; Col).
          split; try (intro; treat_equalities; intuition).
          split; Between.
          }

          {
          assert (H1 : B R) by (assert_diffs; auto).
          assert (H2 : Col B R R) by (assert_cols; Col).
          assert (H3 : Col X2 Q R) by (assert_cols; Col).
          assert (H := l9_19 B R X2 Q R H1 H2 H3); rewrite H.
          split; try (intro; apply HBQR; ColR).
          split; try auto.
          split; try (intro; treat_equalities; intuition).
          Between.
          }
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }

    {
    elim (eq_dec_points R X1); intro HRX1; treat_equalities.

      {
      apply between_symmetry in HCol1.
      apply between_symmetry in HCol3.
      assert (H := outer_pasch X2 R P B A HCol3 HCol1); destruct H as [V [HRVX2 HBAV]].
       V; left.
      assert_cols; split; ColR.
      }

      {
      assert (H : TS R B A Q).
        {
        apply l9_8_2 with X1.

          {
          assert (H1 : R B) by (assert_diffs; auto).
          split; try (intro; apply HBQR; ColR).
          split; Col.
           R; split; Col; Between.
          }

          {
          assert (H1 : R B) by (assert_diffs; auto).
          assert (H2 : Col R B U) by (assert_cols; Col).
          assert (H' : P X1) by (intro; treat_equalities; apply HAX1; reflexivity).
          assert (H3 : Col X1 A U) by (assert_cols; ColR).
          assert (H := l9_19 R B X1 A U H1 H2 H3); rewrite H.
          split; try (intro; apply HBQR; ColR).
          split; try (intro; treat_equalities; apply HBQR; ColR).
          split; try (intro; treat_equalities; apply HABR; Col).
          eBetween.
          }
        }
      destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
       I; assert_cols; Col5.
      }
    }
  }

  {
  assert (H : Bet X1 Q R) by eBetween.
  apply between_symmetry in HQRX1.
  apply between_symmetry in H.
  assert (H' := between_equality R Q X1 H HQRX1); treat_equalities; exfalso; apply HNC; Col.
  }
Qed.

Lemma coplanar_trans_1_aux_2_1_3 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet P A X1
  Bet X2 P B
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2 HCol2 HCol4 HCol1 HCol3.
assert (HQX1X2 : Col Q X1 X2) by (assert_diffs; ColR).
assert (HRX1X2 : Col R X1 X2) by (assert_diffs; ColR).
elim HQX1X2; clear HQX1X2; intro HQX1X2; elim HRX1X2; clear HRX1X2; intro HRX1X2.

  {
  apply coplanar_trans_1_aux_2_1_3_1_1 with P X1 X2; assumption.
  }

  {
  elim HRX1X2; clear HRX1X2; intro HRX1X2.

    {
    apply coplanar_trans_1_aux_2_1_3_1_2 with P X1 X2; assumption.
    }

    {
    apply coplanar_trans_1_aux_2_1_3_1_3 with P X1 X2; assumption.
    }
  }

  {
  elim HQX1X2; clear HQX1X2; intro HQX1X2.

    {
    assert (Coplanar R Q A B) by (apply coplanar_trans_1_aux_2_1_3_1_2 with P X1 X2; Col; Between); Cop.
    }

    {
    assert (Coplanar R Q A B) by (apply coplanar_trans_1_aux_2_1_3_1_3 with P X1 X2; Col; Between); Cop.
    }
  }

  {
  elim HQX1X2; clear HQX1X2; intro HQX1X2; elim HRX1X2; clear HRX1X2; intro HRX1X2.

    {
    apply coplanar_trans_1_aux_2_1_3_2_2 with P X1 X2; assumption.
    }

    {
    apply coplanar_trans_1_aux_2_1_3_2_3 with P X1 X2; assumption.
    }

    {
    assert (Coplanar R Q A B) by (apply coplanar_trans_1_aux_2_1_3_2_3 with P X1 X2; Col; Between); Cop.
    }

    {
    apply coplanar_trans_1_aux_2_1_3_3_3 with P X1 X2; assumption.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_2_2_2_1_1 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet A X1 P
  Bet B X2 P
  Bet Q X1 X2
  Bet R X1 X2
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
apply between_symmetry in HQX1X2.
apply between_symmetry in HRX1X2.
assert (H : X2 X1) by auto; assert (HQRX1 := l5_2 X2 X1 Q R H HQX1X2 HRX1X2); clear H.
elim HQRX1; clear HQRX1; intro HQRX1.

  {
  apply between_symmetry in HQX1X2.
  assert (H := outer_pasch B Q X2 P X1 HCol3 HQX1X2); destruct H as [U [HBUQ HPX1U]].
  apply between_symmetry in HCol1.
  assert (HPX1 : P X1) by (intro; treat_equalities; assert_cols; apply HNC; Col).
  assert (H := l5_2 P X1 A U HPX1 HCol1 HPX1U).
  elim H; clear H; intro HAX1U.

    {
    elim (eq_dec_points Q X1); intro HQX1; treat_equalities.

      {
      apply between_symmetry in HRX1X2.
      assert (H := outer_pasch B R X2 P Q HCol3 HRX1X2); destruct H as [V [HBVR HPQV]].
       V; right; left.
      assert_cols; split; ColR.
      }

      {
      assert (H : TS Q B A R).
        {
        apply l9_8_2 with X1.

          {
          assert (H1 : Q B) by (assert_diffs; auto).
          split; try (intro; assert_cols; apply HABQ; ColR).
          split; Col.
           Q; split; Col; Between.
          }

          {
          assert (H1 : Q B) by (assert_diffs; auto).
          assert (H2 : Col Q B U) by (assert_cols; Col).
          assert (H3 : Col X1 A U) by (assert_cols; Col).
          assert (H := l9_19 Q B X1 A U H1 H2 H3); rewrite H.
          split; try (intro; assert_cols; apply HABQ; ColR).
          split; try (intro; treat_equalities; intuition).
          split; try (intro; subst; apply HABQ; Col).
          Between.
          }
        }
      destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
       I; assert_cols; Col5.
      }
    }

    {
    elim (eq_dec_points Q X1); intro HQX1; treat_equalities.

      {
      apply between_symmetry in HRX1X2.
      assert (H := outer_pasch B R X2 P Q HCol3 HRX1X2); destruct H as [V [HBVR HPQV]].
       V; right; left.
      assert_cols; split; ColR.
      }

      {
      assert (H : TS Q A R B).
        {
        apply l9_31.

          {
           P; split.

            {
            assert (H1 : Q R) by (assert_diffs; auto).
            split; Col.
            split; Col.
             X1; split; Col; Between.
            }

            {
            assert (H1 : Q R) by (assert_diffs; auto).
            split; Col.
            split; Col.
             X2; split; Col; Between.
            }
          }

          {
           X1; split.

            {
            assert (H1 : Q B) by (assert_diffs; auto).
            split; Col.
            split; try (intro; assert_cols; apply HABQ; ColR).
             U; split; Col; Between.
            }

            {
            assert (H1 : Q B) by (assert_diffs; auto).
            split; Col.
            split; try (intro; assert_cols; apply HABQ; ColR).
             Q; split; Col; Between.
            }
          }
        }
      destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
       I; assert_cols; Col5.
      }
    }
  }

  {
  apply between_symmetry in HRX1X2.
  assert (H := outer_pasch B R X2 P X1 HCol3 HRX1X2); destruct H as [U [HBUR HPX1U]].
  apply between_symmetry in HCol1.
  assert (HPX1 : P X1) by (intro; treat_equalities; assert_cols; apply HNC; Col).
  assert (H := l5_2 P X1 A U HPX1 HCol1 HPX1U).
  elim H; clear H; intro HAX1U.

    {
    elim (eq_dec_points R X1); intro HRX1; treat_equalities.

      {
      apply between_symmetry in HQX1X2.
      assert (H := outer_pasch B Q X2 P R HCol3 HQX1X2); destruct H as [V [HBVQ HPRV]].
       V; right; right.
      assert_cols; split; ColR.
      }

      {
      assert (H : TS R B A Q).
        {
        apply l9_8_2 with X1.

          {
          assert (H1 : R B) by (assert_diffs; auto).
          split; try (intro; assert_cols; apply HABR; ColR).
          split; Col.
           R; split; Col; Between.
          }

          {
          assert (H1 : R B) by (assert_diffs; auto).
          assert (H2 : Col R B U) by (assert_cols; Col).
          assert (H3 : Col X1 A U) by (assert_cols; Col).
          assert (H := l9_19 R B X1 A U H1 H2 H3); rewrite H.
          split; try (intro; assert_cols; apply HABR; ColR).
          split; try (intro; treat_equalities; intuition).
          split; try (intro; subst; apply HABR; Col).
          Between.
          }
        }
      destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
       I; assert_cols; Col5.
      }
    }

    {
    elim (eq_dec_points R X1); intro HRX1; treat_equalities.

      {
      apply between_symmetry in HQX1X2.
      assert (H := outer_pasch B Q X2 P R HCol3 HQX1X2); destruct H as [V [HBVQ HPRV]].
       V; right; right.
      assert_cols; split; ColR.
      }

      {
      assert (H : TS R A Q B).
        {
        apply l9_31.

          {
           P; split.

            {
            assert (H1 : R Q) by (assert_diffs; auto).
            split; Col.
            split; Col.
             X1; split; Col; Between.
            }

            {
            assert (H1 : R Q) by (assert_diffs; auto).
            split; Col.
            split; Col.
             X2; split; Col; Between.
            }
          }

          {
           X1; split.

            {
            assert (H1 : R B) by (assert_diffs; auto).
            split; Col.
            split; try (intro; assert_cols; apply HABR; ColR).
             U; split; Col; Between.
            }

            {
            assert (H1 : R B) by (assert_diffs; auto).
            split; Col.
            split; try (intro; assert_cols; apply HABR; ColR).
             R; split; Col; Between.
            }
          }
        }
      destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
       I; assert_cols; Col5.
      }
    }
  }
Qed.

Lemma coplanar_trans_1_aux_2_2_2_1_2 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet A X1 P
  Bet B X2 P
  Bet Q X1 X2
  Bet X1 X2 R
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
elim (eq_dec_points Q X1); intro HQX1; treat_equalities.

  {
  assert (H : TS B Q R A).
    {
    apply l9_8_2 with P.

      {
      assert (B Q) by (assert_diffs; auto).
      split; try (intro; assert_diffs; assert_cols; apply HABQ; ColR).
      split; Col.
       Q; split; Col; Between.
      }

      {
      apply one_side_transitivity with X2.

        {
        assert (H1 : B Q) by (assert_diffs; auto).
        assert (H2 : Col B Q B) by (assert_cols; Col).
        assert (H3 : Col P X2 B) by (assert_cols; Col).
        assert (H := l9_19 B Q P X2 B H1 H2 H3); rewrite H.
        split; try (intro; assert_diffs; assert_cols; apply HABQ; ColR).
        split; try (intro; treat_equalities; intuition).
        split; Between.
        }

        {
        assert (H1 : B Q) by (assert_diffs; auto).
        assert (H2 : Col B Q Q) by (assert_cols; Col).
        assert (H3 : Col X2 R Q) by (assert_cols; Col).
        assert (H := l9_19 B Q X2 R Q H1 H2 H3); rewrite H.
        assert (Q X2) by (intro; treat_equalities; intuition).
        split; try (intro; assert_diffs; assert_cols; apply HABQ; ColR).
        split; try auto.
        split; try (intro; treat_equalities; intuition).
        Between.
        }
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }
    
  {
  assert (H := outer_pasch B Q X2 P X1 HCol3 HQX1X2); destruct H as [U [HBUQ HPX1U]].
  apply between_symmetry in HCol1.
  assert (HPX1 : P X1) by (intro; treat_equalities; assert_cols; apply HNC; Col).
  assert (H := l5_2 P X1 A U HPX1 HCol1 HPX1U).
  elim H; clear H; intro HAX1U.

    {
    assert (H : TS Q A R B).
      {
      apply l9_31.

        {
         P; split.

          {
          assert (H1 : Q R) by (assert_diffs; auto).
          split; Col.
          split; Col.
           X1; split; Col; Between.
          }

          {
          assert (H1 : Q R) by (assert_diffs; auto).
          split; Col.
          split; Col.
           X2; split; Col; Between.
          }
        }

        {
        apply one_side_transitivity with X1.

          {
          assert (H1 : Q B) by (assert_diffs; auto).
          assert (H2 : Col Q B U) by (assert_cols; Col).
          assert (H3 : Col A X1 U) by (assert_cols; Col).
          assert (H := l9_19 Q B A X1 U H1 H2 H3); rewrite H.
          split; try (intro; assert_cols; apply HABQ; ColR).
          split; try (intro; treat_equalities; intuition).
          split; try (intro; treat_equalities; intuition).
          Between.
          }

          {
          assert (H1 : Q B) by (assert_diffs; auto).
          assert (H2 : Col Q B Q) by (assert_cols; Col).
          assert (H3 : Col X1 R Q) by (assert_cols; Col).
          assert (H := l9_19 Q B X1 R Q H1 H2 H3); rewrite H.
          split; try (intro; assert_cols; apply HABQ; ColR).
          split; try (intro; treat_equalities; intuition).
          split; try (intro; treat_equalities; intuition).
          eBetween.
          }
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }

    {
    assert (H : TS B Q R A).
      {
      apply l9_8_2 with X1.

        {
        assert (B Q) by (assert_diffs; auto).
        split; try (intro; assert_cols; apply HABQ; ColR).
        split; Col.
         U; split; Col; Between.
        }

        {
        assert (H1 : B Q) by (assert_diffs; auto).
        assert (H2 : Col B Q Q) by (assert_cols; Col).
        assert (H3 : Col X1 R Q) by (assert_cols; Col).
        assert (H := l9_19 B Q X1 R Q H1 H2 H3); rewrite H.
        split; try (intro; assert_cols; apply HABQ; ColR).
        split; try (intro; treat_equalities; intuition).
        split; try (intro; treat_equalities; apply HNC; Col).
        eBetween.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_2_2_2_1_3 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet A X1 P
  Bet B X2 P
  Bet Q X1 X2
  Bet X2 R X1
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
elim (eq_dec_points Q X1); intro HQX1; treat_equalities.

  {
  assert (H : TS B Q R A).
    {
    apply l9_8_2 with P.

      {
      assert (B Q) by (assert_diffs; auto).
      split; try (intro; assert_diffs; assert_cols; apply HABQ; ColR).
      split; Col.
       Q; split; Col; Between.
      }

      {
      apply one_side_transitivity with X2.

        {
        assert (H1 : B Q) by (assert_diffs; auto).
        assert (H2 : Col B Q B) by (assert_cols; Col).
        assert (H3 : Col P X2 B) by (assert_cols; Col).
        assert (H := l9_19 B Q P X2 B H1 H2 H3); rewrite H.
        split; try (intro; assert_diffs; assert_cols; apply HABQ; ColR).
        split; try (intro; treat_equalities; intuition).
        split; Between.
        }

        {
        assert (H1 : B Q) by (assert_diffs; auto).
        assert (H2 : Col B Q Q) by (assert_cols; Col).
        assert (H3 : Col X2 R Q) by (assert_cols; Col).
        assert (H := l9_19 B Q X2 R Q H1 H2 H3); rewrite H.
        assert (Q X2) by (intro; treat_equalities; intuition).
        split; try (intro; assert_diffs; assert_cols; apply HABQ; ColR).
        split; try auto.
        split; try (intro; treat_equalities; intuition).
        Between.
        }
      }
    }
  destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
   I; assert_cols; Col5.
  }
    
  {
  assert (H := outer_pasch B Q X2 P X1 HCol3 HQX1X2); destruct H as [U [HBUQ HPX1U]].
  apply between_symmetry in HCol1.
  assert (HPX1 : P X1) by (intro; treat_equalities; assert_cols; apply HNC; Col).
  assert (H := l5_2 P X1 A U HPX1 HCol1 HPX1U).
  elim H; clear H; intro HAX1U.

    {
    assert (H : TS Q A R B).
      {
      apply l9_31.

        {
         P; split.

          {
          assert (H1 : Q R) by (assert_diffs; auto).
          split; Col.
          split; Col.
           X1; split; Col; Between.
          }

          {
          assert (H1 : Q R) by (assert_diffs; auto).
          split; Col.
          split; Col.
           X2; split; Col; Between.
          }
        }

        {
        apply one_side_transitivity with X1.

          {
          assert (H1 : Q B) by (assert_diffs; auto).
          assert (H2 : Col Q B U) by (assert_cols; Col).
          assert (H3 : Col A X1 U) by (assert_cols; Col).
          assert (H := l9_19 Q B A X1 U H1 H2 H3); rewrite H.
          split; try (intro; assert_cols; apply HABQ; ColR).
          split; try (intro; treat_equalities; intuition).
          split; try (intro; treat_equalities; intuition).
          Between.
          }

          {
          assert (H1 : Q B) by (assert_diffs; auto).
          assert (H2 : Col Q B Q) by (assert_cols; Col).
          assert (H3 : Col X1 R Q) by (assert_cols; Col).
          assert (H := l9_19 Q B X1 R Q H1 H2 H3); rewrite H.
          split; try (intro; assert_cols; apply HABQ; ColR).
          split; try (intro; treat_equalities; intuition).
          split; try (intro; treat_equalities; intuition).
          eBetween.
          }
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }

    {
    assert (H : TS B Q R A).
      {
      apply l9_8_2 with X1.

        {
        assert (B Q) by (assert_diffs; auto).
        split; try (intro; assert_cols; apply HABQ; ColR).
        split; Col.
         U; split; Col; Between.
        }

        {
        assert (H1 : B Q) by (assert_diffs; auto).
        assert (H2 : Col B Q Q) by (assert_cols; Col).
        assert (H3 : Col X1 R Q) by (assert_cols; Col).
        assert (H := l9_19 B Q X1 R Q H1 H2 H3); rewrite H.
        split; try (intro; assert_cols; apply HABQ; ColR).
        split; try (intro; treat_equalities; intuition).
        split; try (intro; treat_equalities; apply HNC; Col).
        eBetween.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_2_2_2_2_2 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet A X1 P
  Bet B X2 P
  Bet X2 Q X1
  Bet X2 R X1
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
assert (HQRX2 := l5_3 X2 Q R X1 HQX1X2 HRX1X2).
elim HQRX2; clear HQRX2; intro HQRX2.

  {
  elim (eq_dec_points Q X2); intro HQX2; treat_equalities.

    {
    apply between_symmetry in HCol1.
    assert (H := outer_pasch P Q X1 A R HCol1 HRX1X2); destruct H as [U [HPUQ HARU]].
     U; right; right.
    assert_diffs; assert_cols; split; ColR.
    }

    {
    assert (H : TS A Q B R).
      {
      apply l9_8_2 with X2.

        {
        assert (A Q) by (assert_diffs; auto).
        split; try (intro; assert_cols; apply HAQR; ColR).
        split; Col.
         Q; split; Col; Between.
        }

        {
        apply between_symmetry in HCol1.
        assert (H := outer_pasch P X2 X1 A Q HCol1 HQX1X2); destruct H as [U [HPUX2 HAQU]].
        assert (H1 : A Q) by (assert_diffs; auto).
        assert (H2 : Col A Q U) by (assert_cols; Col).
        assert (HPX2 : P X2) by (intro; treat_equalities; apply HNC; Col).
        assert (H3 : Col X2 B U) by (assert_cols; ColR).
        assert (H := l9_19 A Q X2 B U H1 H2 H3); rewrite H.
        split; try (intro; assert_cols; apply HAQR; ColR).
        split; try (intro; treat_equalities; assert_cols; apply HAQR; ColR).
        split; try (intro; treat_equalities; apply HABQ; Col).
        eBetween.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }

  {
  elim (eq_dec_points R X2); intro HRX2; treat_equalities.

    {
    apply between_symmetry in HCol1.
    assert (H := outer_pasch P R X1 A Q HCol1 HQX1X2); destruct H as [U [HPUR HAQU]].
     U; right; left.
    assert_diffs; assert_cols; split; ColR.
    }

    {
    assert (H : TS A R B Q).
      {
      apply l9_8_2 with X2.

        {
        assert (A R) by (assert_diffs; auto).
        split; try (intro; assert_cols; apply HAQR; ColR).
        split; Col.
         R; split; Col; Between.
        }

        {
        apply between_symmetry in HCol1.
        assert (H := outer_pasch P X2 X1 A R HCol1 HRX1X2); destruct H as [U [HPUX2 HARU]].
        assert (H1 : A R) by (assert_diffs; auto).
        assert (H2 : Col A R U) by (assert_cols; Col).
        assert (HPX2 : P X2) by (intro; treat_equalities; apply HNC; Col).
        assert (H3 : Col X2 B U) by (assert_cols; ColR).
        assert (H := l9_19 A R X2 B U H1 H2 H3); rewrite H.
        split; try (intro; assert_cols; apply HAQR; ColR).
        split; try (intro; treat_equalities; assert_cols; apply HAQR; ColR).
        split; try (intro; treat_equalities; apply HABR; Col).
        eBetween.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_2_2_2 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet A X1 P
  Bet B X2 P
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2 HCol2 HCol4 HCol1 HCol3.
assert (HQX1X2 : Col Q X1 X2) by (assert_diffs; ColR).
assert (HRX1X2 : Col R X1 X2) by (assert_diffs; ColR).
elim HQX1X2; clear HQX1X2; intro HQX1X2; elim HRX1X2; clear HRX1X2; intro HRX1X2.

  {
  apply coplanar_trans_1_aux_2_2_2_1_1 with P X1 X2; assumption.
  }

  {
  elim HRX1X2; clear HRX1X2; intro HRX1X2.

    {
    apply coplanar_trans_1_aux_2_2_2_1_2 with P X1 X2; assumption.
    }

    {
    apply coplanar_trans_1_aux_2_2_2_1_3 with P X1 X2; assumption.
    }
  }

  {
  elim HQX1X2; clear HQX1X2; intro HQX1X2.

    {
    assert (Coplanar Q R B A) by (apply coplanar_trans_1_aux_2_2_2_1_2 with P X2 X1; Col; Between); Cop.
    }

    {
    assert (Coplanar R Q A B) by (apply coplanar_trans_1_aux_2_2_2_1_3 with P X1 X2; Col; Between); Cop.
    }
  }

  {
  elim HQX1X2; clear HQX1X2; intro HQX1X2; elim HRX1X2; clear HRX1X2; intro HRX1X2.

    {
    assert (Coplanar Q R B A) by (apply coplanar_trans_1_aux_2_2_2_1_1 with P X2 X1; Col; Between); Cop.
    }

    {
    assert (Coplanar Q R B A) by (apply coplanar_trans_1_aux_2_2_2_1_3 with P X2 X1; Col; Between); Cop.
    }

    {
    assert (Coplanar R Q B A) by (apply coplanar_trans_1_aux_2_2_2_1_3 with P X2 X1; Col; Between); Cop.
    }

    {
    apply coplanar_trans_1_aux_2_2_2_2_2 with P X1 X2; assumption.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_2_2_3 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet A X1 P
  Bet X2 P B
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2 HCol2 HCol4 HCol1 HCol3.
assert (H : TS Q R B A).
  {
  apply l9_8_2 with P.

    {
    assert (H1 : Q R) by (assert_diffs; auto).
    split; Col.
    split; Col.
     X1; split; Col; Between.
    }

    {
    assert (H1 : Q R) by (assert_diffs; auto).
    assert (H2 : Col Q R X2) by (assert_cols; Col).
    assert (H3 : Col P B X2) by (assert_cols; Col).
    assert (H := l9_19 Q R P B X2 H1 H2 H3); rewrite H.
    split; Col.
    split; try (intro; treat_equalities; intuition).
    split; Between.
    }
  }
destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
I; assert_cols; Col5.
Qed.

Lemma coplanar_trans_1_aux_2_3_3_1_1 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet X1 P A
  Bet X2 P B
  Bet Q X1 X2
  Bet R X1 X2
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
apply between_symmetry in HQX1X2.
apply between_symmetry in HRX1X2.
assert (H : X2 X1) by auto; assert (HQRX1 := l5_2 X2 X1 Q R H HQX1X2 HRX1X2); clear H.
elim HQRX1; clear HQRX1; intro HQRX1.

  {
  apply between_symmetry in HCol1.
  apply between_symmetry in HRX1X2.
  assert (H := outer_pasch R A X1 X2 P HRX1X2 HCol1); destruct H as [U [HAUR HX2PU]].
  assert (HPX2 : X2 P) by (intro; treat_equalities; apply HNC; Col).
  assert (H := l5_2 X2 P B U HPX2 HCol3 HX2PU).
  elim H; clear H; intro HBPU.

    {
    assert (H : TS R B Q A).
      {
      apply l9_31.

        {
        apply one_side_transitivity with P.

          {
          assert (H1 : R Q) by (assert_diffs; auto).
          assert (H2 : Col R Q X2) by (assert_cols; Col).
          assert (H3 : Col B P X2) by (assert_cols; Col).
          assert (H := l9_19 R Q B P X2 H1 H2 H3); rewrite H.
          split; Col.
          split; try assumption.
          split; try (intro; treat_equalities; intuition).
          Between.
          }

          {
          assert (H1 : R Q) by (assert_diffs; auto).
          assert (H2 : Col R Q X1) by (assert_cols; Col).
          assert (H3 : Col P A X1) by (assert_cols; Col).
          assert (H := l9_19 R Q P A X1 H1 H2 H3); rewrite H.
          split; Col.
          split; try (intro; treat_equalities; intuition).
          split; try assumption.
          Between.
          }
        }

        {
        apply one_side_transitivity with X2.

          {
          assert (H1 : R A) by (assert_diffs; auto).
          assert (H2 : Col R A U) by (assert_cols; Col).
          assert (H3 : Col B X2 U) by (assert_cols; ColR).
          assert (H := l9_19 R A B X2 U H1 H2 H3); rewrite H.
          split; Col.
          split; try (intro; treat_equalities; intuition).
          split; try (intro; treat_equalities; intuition).
          eBetween.
          }

          {
          assert (H1 : R A) by (assert_diffs; auto).
          assert (H2 : Col R A R) by (assert_cols; Col).
          assert (H3 : Col X2 Q R) by (assert_cols; Col).
          assert (H := l9_19 R A X2 Q R H1 H2 H3); rewrite H.
          assert (R X2) by (intro; treat_equalities; apply HNC; Col).
          split; try (intro; apply HAQR; ColR).
          split; try (intro; treat_equalities; intuition).
          split; try (intro; treat_equalities; intuition).
          eBetween.
          }
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }

    {
    assert (H : TS A R Q B).
      {
      apply l9_8_2 with X2.

        {
        assert (A R) by (assert_diffs; auto).
        assert (R X2) by (intro; treat_equalities; apply HNC; Col).
        split; try (intro; apply HAQR; ColR).
        split; Col.
         U; split; Col; eBetween.
        }

        {
        assert (H1 : A R) by (assert_diffs; auto).
        assert (H2 : Col A R R) by (assert_cols; Col).
        assert (H3 : Col X2 Q R) by (assert_cols; Col).
        assert (H := l9_19 A R X2 Q R H1 H2 H3); rewrite H.
        assert (R X2) by (intro; treat_equalities; apply HNC; Col).
        split; try (intro; apply HAQR; ColR).
        split; try (intro; treat_equalities; intuition).
        split; try (intro; treat_equalities; intuition).
        eBetween.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }

  {
  apply between_symmetry in HCol1.
  apply between_symmetry in HQX1X2.
  assert (H := outer_pasch Q A X1 X2 P HQX1X2 HCol1); destruct H as [U [HAUQ HX2PU]].
  assert (HPX2 : X2 P) by (intro; treat_equalities; apply HNC; Col).
  assert (H := l5_2 X2 P B U HPX2 HCol3 HX2PU).
  elim H; clear H; intro HBPU.

    {
    assert (H : TS Q B R A).
      {
      apply l9_31.

        {
        apply one_side_transitivity with P.

          {
          assert (H1 : Q R) by (assert_diffs; auto).
          assert (H2 : Col Q R X2) by (assert_cols; Col).
          assert (H3 : Col B P X2) by (assert_cols; Col).
          assert (H := l9_19 Q R B P X2 H1 H2 H3); rewrite H.
          split; Col.
          split; try assumption.
          split; try (intro; treat_equalities; intuition).
          Between.
          }

          {
          assert (H1 : Q R) by (assert_diffs; auto).
          assert (H2 : Col Q R X1) by (assert_cols; Col).
          assert (H3 : Col P A X1) by (assert_cols; Col).
          assert (H := l9_19 Q R P A X1 H1 H2 H3); rewrite H.
          split; Col.
          split; try (intro; treat_equalities; intuition).
          split; try assumption.
          Between.
          }
        }

        {
        apply one_side_transitivity with X2.

          {
          assert (H1 : Q A) by (assert_diffs; auto).
          assert (H2 : Col Q A U) by (assert_cols; Col).
          assert (H3 : Col B X2 U) by (assert_cols; ColR).
          assert (H := l9_19 Q A B X2 U H1 H2 H3); rewrite H.
          split; Col.
          split; try (intro; treat_equalities; intuition).
          split; try (intro; treat_equalities; intuition).
          eBetween.
          }

          {
          assert (H1 : Q A) by (assert_diffs; auto).
          assert (H2 : Col Q A Q) by (assert_cols; Col).
          assert (H3 : Col X2 R Q) by (assert_cols; Col).
          assert (H := l9_19 Q A X2 R Q H1 H2 H3); rewrite H.
          assert (Q X2) by (intro; treat_equalities; apply HNC; Col).
          split; try (intro; apply HAQR; ColR).
          split; try (intro; treat_equalities; intuition).
          split; try (intro; treat_equalities; intuition).
          eBetween.
          }
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }

    {
    assert (H : TS A Q R B).
      {
      apply l9_8_2 with X2.

        {
        assert (A Q) by (assert_diffs; auto).
        assert (Q X2) by (intro; treat_equalities; apply HNC; Col).
        split; try (intro; apply HAQR; ColR).
        split; Col.
         U; split; Col; eBetween.
        }

        {
        assert (H1 : A Q) by (assert_diffs; auto).
        assert (H2 : Col A Q Q) by (assert_cols; Col).
        assert (H3 : Col X2 R Q) by (assert_cols; Col).
        assert (H := l9_19 A Q X2 R Q H1 H2 H3); rewrite H.
        assert (Q X2) by (intro; treat_equalities; apply HNC; Col).
        split; try (intro; apply HAQR; ColR).
        split; try (intro; treat_equalities; intuition).
        split; try (intro; treat_equalities; intuition).
        eBetween.
        }
      }
    destruct H as [HCol5 [HCol6 [I [HCol7 HCol8]]]].
     I; assert_cols; Col5.
    }
  }
Qed.

Lemma coplanar_trans_1_aux_2_3_3_1_2 : P Q R A B X1 X2,
  ¬ Col P Q R
  ¬ Col A B P
  ¬ Col A B Q
  ¬ Col A B R
  ¬ Col A Q R
  ¬ Col B Q R
  A X1
  B X2
  X1 X2
  Col Q R X1
  Col Q R X2
  Bet X1 P A
  Bet X2 P B
  Bet Q X1 X2
  Bet X1 X2 R
  Coplanar Q R A B.
Proof.
intros P Q R A B X1 X2 HNC HABP HABQ HABR HAQR HBQR HAX1 HAX2 HX1X2;
intros HCol2 HCol4 HCol1 HCol3 HQX1X2 HRX1X2.
apply between_symmetry in HCol1.
assert (H := outer_pasch Q A X1 X2 P HQX1X2 HCol1); destruct H as [U [HAUQ HX2PU]].
assert (HPX2 : X2 P) by (intro; treat_equalities; apply HNC; Col).
assert (H := l5_2 X2 P B U HPX2 HCol3 HX2PU).
elim H; clear H; intro HBPU.

  {
  assert (H : TS Q B R A).
    {
    apply l9_31.

      {
      apply one_side_transitivity with P.

        {
        assert (H1 : Q R) by (assert_diffs; auto).
        assert (H2 : Col Q R X2) by (assert_cols; Col).
        assert (H3 : Col B P X2) by (assert_cols; Col).
        assert (H := l9_19 Q R B P X2 H1 H2 H3); rewrite H.
        split; Col.
        split; try assumption.
        split; try (intro; treat_equalities; intuition).
        Between.
        }

        {
        assert (H1 : Q R) by (assert_diffs; auto).
        assert (H2 : Col Q R X1) by (assert_cols; Col).
        assert (H3 : Col P A X1) by (assert_cols; Col).
        assert (H := l9_19 Q R P A X1 H1 H2 H3); rewrite H.
        split; Col.
        split; try (intro; treat_equalities; intuition).
        split; try assumption.
        Between.
        }
      }

      {
      apply one_side_transitivity with X2.

        {
        assert (H1 : Q A) by (assert_diffs; auto).
        assert (H2 : Col Q A U) by (assert_cols; Col).
        assert (H3 : Col B X2 U) by (assert_cols; ColR).
        assert (H := l9_19 Q A B X2 U H1 H2 H3); rewrite H.
        split; Col.
        split; try (intro; treat_equalities; intuition).
        split; try (intro; treat_equalities; intuition).
        eBetween.
        }

        {
        assert (H1 : Q A) by (assert_diffs; auto).
        assert (H2 : Col Q A Q) by (assert_cols; Col).
        assert (H3 : Col X2 R Q) by (assert_cols; Col).
        assert (H := l9_19 Q A X2 R Q H1 H2 H3); rewrite H.
        assert (Q X2) by (intro; treat_equalities; apply HX1X2; reflexivit