Library GeoCoq.Elements.OriginalProofs.lemma_collinear4

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearorder.
Require Export GeoCoq.Elements.OriginalProofs.lemma_outerconnectivity.
Require Export GeoCoq.Elements.OriginalProofs.lemma_3_7b.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_collinear4 :
    A B C D,
   Col A B C Col A B D neq A B
   Col B C D.
Proof.
intros.
assert (Col B C D).
by cases on (eq B C eq B D eq C D eq A C eq A D (neq B C neq B D neq C D neq A C neq A D)).
{
 assert (Col B C D) by (conclude_def Col ).
 close.
 }
{
 assert (Col B C D) by (conclude_def Col ).
 close.
 }
{
 assert (Col B C D) by (conclude_def Col ).
 close.
 }
{
 assert (Col C B D) by (conclude cn_equalitysub).
 assert (Col B C D) by (forward_using lemma_collinearorder).
 close.
 }
{
 assert (Col D B C) by (conclude cn_equalitysub).
 assert (Col B C D) by (forward_using lemma_collinearorder).
 close.
 }
{
 assert ((eq A B eq A C eq B C BetS B A C BetS A B C BetS A C B)) by (conclude_def Col ).
 assert (Col B C D).
 by cases on (BetS B A C BetS A B C BetS A C B).
 {
  assert ((eq A B eq A D eq B D BetS B A D BetS A B D BetS A D B)) by (conclude_def Col ).
  assert (Col B C D).
  by cases on (BetS B A D BetS A B D BetS A D B).
  {
   assert (¬ nCol B C D).
    {
    intro.
    assert (¬ BetS B C D).
     {
     intro.
     assert (Col B C D) by (conclude_def Col ).
     contradict.
     }
    assert (¬ BetS A C D).
     {
     intro.
     assert (BetS B C D) by (conclude lemma_3_5b).
     contradict.
     }
    assert (¬ nCol B D C).
     {
     intro.
     assert (¬ BetS C D C) by (conclude axiom_betweennessidentity).
     assert (¬ BetS A D C).
      {
      intro.
      assert (BetS B D C) by (conclude lemma_3_5b).
      assert (Col B D C) by (conclude_def Col ).
      contradict.
      }
     assert (eq C D) by (conclude lemma_outerconnectivity).
     assert (Col B C D) by (conclude_def Col ).
     assert (Col B D C) by (forward_using lemma_collinearorder).
     contradict.
     }
    assert (Col B C D) by (forward_using lemma_collinearorder).
    contradict.
    }
   close.
   }
  {
   assert (BetS D B A) by (conclude axiom_betweennesssymmetry).
   assert (BetS D B C) by (conclude lemma_3_7b).
   assert (Col D B C) by (conclude_def Col ).
   assert (Col B C D) by (forward_using lemma_collinearorder).
   close.
   }
  {
   assert (BetS B D A) by (conclude axiom_betweennesssymmetry).
   assert (BetS B D C) by (conclude lemma_3_6b).
   assert (Col B D C) by (conclude_def Col ).
   assert (Col B C D) by (forward_using lemma_collinearorder).
   close.
   }

  close.
  }
 {
  assert ((eq A B eq A D eq B D BetS B A D BetS A B D BetS A D B)) by (conclude_def Col ).
  assert (Col B C D).
  by cases on (BetS B A D BetS A B D BetS A D B).
  {
   assert (BetS D A B) by (conclude axiom_betweennesssymmetry).
   assert (BetS D B C) by (conclude lemma_3_7a).
   assert (Col D B C) by (conclude_def Col ).
   assert (Col B C D) by (forward_using lemma_collinearorder).
   close.
   }
  {
   assert (¬ nCol B C D).
    {
    intro.
    assert (¬ BetS B C D).
     {
     intro.
     assert (Col B C D) by (conclude_def Col ).
     contradict.
     }
    assert (¬ BetS B D C).
     {
     intro.
     assert (Col B D C) by (conclude_def Col ).
     assert (Col B C D) by (forward_using lemma_collinearorder).
     contradict.
     }
    assert (eq C D) by (conclude lemma_outerconnectivity).
    assert (Col B C D) by (conclude_def Col ).
    contradict.
    }
   close.
   }
  {
   assert (BetS D B C) by (conclude lemma_3_6a).
   assert (Col D B C) by (conclude_def Col ).
   assert (Col B C D) by (forward_using lemma_collinearorder).
   close.
   }

  close.
  }
 {
  assert ((eq A B eq A D eq B D BetS B A D BetS A B D BetS A D B)) by (conclude_def Col ).
  assert (Col B C D).
  by cases on (BetS B A D BetS A B D BetS A D B).
  {
   assert (BetS D A B) by (conclude axiom_betweennesssymmetry).
   assert (BetS D C B) by (conclude lemma_3_5b).
   assert (BetS B C D) by (conclude axiom_betweennesssymmetry).
   assert (Col B C D) by (conclude_def Col ).
   close.
   }
  {
   assert (BetS C B D) by (conclude lemma_3_6a).
   assert (Col B C D) by (conclude_def Col ).
   close.
   }
  {
   assert (¬ nCol B C D).
    {
    intro.
    assert (¬ ¬ BetS B D C).
     {
     intro.
     assert (¬ ¬ BetS B C D).
      {
      intro.
      assert (BetS B C A) by (conclude axiom_betweennesssymmetry).
      assert (BetS B D A) by (conclude axiom_betweennesssymmetry).
      assert (eq C D) by (conclude axiom_connectivity).
      contradict.
      }
     assert (Col B C D) by (conclude_def Col ).
     contradict.
     }
    assert (Col B D C) by (conclude_def Col ).
    assert (Col B C D) by (forward_using lemma_collinearorder).
    contradict.
    }
   close.
   }

  close.
  }

 close.
 }

close.
Qed.

End Euclid.