Library GeoCoq.Elements.OriginalProofs.lemma_collinearbetween

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear4.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_collinearbetween :
    A B C D E F H,
   Col A E B Col C F D neq A B neq C D neq A E neq F D ¬ Meet A B C D BetS A H D Col E F H
   BetS E H F.
Proof.
intros.
assert (¬ Col A B C).
 {
 intro.
 assert (eq C C) by (conclude cn_equalityreflexive).
 assert (Col C D C) by (conclude_def Col ).
 assert (Meet A B C D) by (conclude_def Meet ).
 contradict.
 }
assert (¬ eq H E).
 {
 intro.
 assert (Col A H B) by (conclude cn_equalitysub).
 assert (Col H A B) by (forward_using lemma_collinearorder).
 assert (Col A H D) by (conclude_def Col ).
 assert (Col H A D) by (forward_using lemma_collinearorder).
 assert (neq A H) by (forward_using lemma_betweennotequal).
 assert (neq H A) by (conclude lemma_inequalitysymmetric).
 assert (Col A B D) by (conclude lemma_collinear4).
 assert (eq D D) by (conclude cn_equalityreflexive).
 assert (Col C D D) by (conclude_def Col ).
 assert (Meet A B C D) by (conclude_def Meet ).
 contradict.
 }
assert (¬ eq H F).
 {
 intro.
 assert (Col C D F) by (forward_using lemma_collinearorder).
 assert (Col A H D) by (conclude_def Col ).
 assert (Col A F D) by (conclude cn_equalitysub).
 assert (Col F D A) by (forward_using lemma_collinearorder).
 assert (Col F D C) by (forward_using lemma_collinearorder).
 assert (Col D A C) by (conclude lemma_collinear4).
 assert (Col C D A) by (forward_using lemma_collinearorder).
 assert (eq A A) by (conclude cn_equalityreflexive).
 assert (Col A B A) by (conclude_def Col ).
 assert (Meet A B C D) by (conclude_def Meet ).
 contradict.
 }
assert (¬ BetS E F H).
 {
 intro.
 assert (BetS H F E) by (conclude axiom_betweennesssymmetry).
 assert (BetS D H A) by (conclude axiom_betweennesssymmetry).
 assert (¬ Col D A E).
  {
  intro.
  assert (Col E A B) by (forward_using lemma_collinearorder).
  assert (Col E A D) by (forward_using lemma_collinearorder).
  assert (neq E A) by (conclude lemma_inequalitysymmetric).
  assert (Col A B D) by (conclude lemma_collinear4).
  assert (eq D D) by (conclude cn_equalityreflexive).
  assert (Col C D D) by (conclude_def Col ).
  assert (Meet A B C D) by (conclude_def Meet ).
  contradict.
  }
 let Tf:=fresh in
 assert (Tf: Q, (BetS E Q A BetS D F Q)) by (conclude postulate_Pasch_outer);destruct Tf as [Q];spliter.
 assert (Col E Q A) by (conclude_def Col ).
 assert (Col D F Q) by (conclude_def Col ).
 assert (Col E A Q) by (forward_using lemma_collinearorder).
 assert (Col E A B) by (forward_using lemma_collinearorder).
 assert (neq E A) by (conclude lemma_inequalitysymmetric).
 assert (Col A Q B) by (conclude lemma_collinear4).
 assert (Col A B Q) by (forward_using lemma_collinearorder).
 assert (Col F D Q) by (forward_using lemma_collinearorder).
 assert (Col F D C) by (forward_using lemma_collinearorder).
 assert (Col D Q C) by (conclude lemma_collinear4).
 assert (Col C D Q) by (forward_using lemma_collinearorder).
 assert (Meet A B C D) by (conclude_def Meet ).
 contradict.
 }
assert (¬ BetS F E H).
 {
 intro.
 assert (¬ Col A D F).
  {
  intro.
  assert (Col F D C) by (forward_using lemma_collinearorder).
  assert (Col F D A) by (forward_using lemma_collinearorder).
  assert (Col D C A) by (conclude lemma_collinear4).
  assert (Col C D A) by (forward_using lemma_collinearorder).
  assert (eq A A) by (conclude cn_equalityreflexive).
  assert (Col A B A) by (conclude_def Col ).
  assert (Meet A B C D) by (conclude_def Meet ).
  contradict.
  }
 let Tf:=fresh in
 assert (Tf: R, (BetS F R D BetS A E R)) by (conclude postulate_Pasch_outer);destruct Tf as [R];spliter.
 assert (Col F R D) by (conclude_def Col ).
 assert (Col A E R) by (conclude_def Col ).
 assert (Col F D R) by (forward_using lemma_collinearorder).
 assert (Col F D C) by (forward_using lemma_collinearorder).
 assert (Col D R C) by (conclude lemma_collinear4).
 assert (Col C D R) by (forward_using lemma_collinearorder).
 assert (Col E A R) by (forward_using lemma_collinearorder).
 assert (Col E A B) by (forward_using lemma_collinearorder).
 assert (neq A E) by (forward_using lemma_betweennotequal).
 assert (neq E A) by (conclude lemma_inequalitysymmetric).
 assert (Col A R B) by (conclude lemma_collinear4).
 assert (Col A B R) by (forward_using lemma_collinearorder).
 assert (Meet A B C D) by (conclude_def Meet ).
 contradict.
 }
assert (¬ eq E F).
 {
 intro.
 assert (Col C D F) by (forward_using lemma_collinearorder).
 assert (Col A B E) by (forward_using lemma_collinearorder).
 assert (Col A B F) by (conclude cn_equalitysub).
 assert (Meet A B C D) by (conclude_def Meet ).
 contradict.
 }
assert ((eq E F eq E H eq F H BetS F E H BetS E F H BetS E H F)) by (conclude_def Col ).
assert (BetS E H F).
by cases on (eq E F eq E H eq F H BetS F E H BetS E F H BetS E H F).
{
 assert (¬ ¬ BetS E H F).
  {
  intro.
  contradict.
  }
 close.
 }
{
 assert (¬ ¬ BetS E H F).
  {
  intro.
  assert (neq E H) by (conclude lemma_inequalitysymmetric).
  contradict.
  }
 close.
 }
{
 assert (¬ ¬ BetS E H F).
  {
  intro.
  assert (neq F H) by (conclude lemma_inequalitysymmetric).
  contradict.
  }
 close.
 }
{
 assert (¬ ¬ BetS E H F).
  {
  intro.
  contradict.
  }
 close.
 }
{
 assert (¬ ¬ BetS E H F).
  {
  intro.
  contradict.
  }
 close.
 }
{
 close.
 }

close.
Qed.

End Euclid.