Library GeoCoq.Elements.OriginalProofs.lemma_twolines

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear4.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_twolines :
   ∀ A B C D E F,
   Cut A B C D E → Cut A B C D F → nCol B C D →
   eq E F.
Proof.
intros.
assert ((BetS A E B ∧ BetS C E D ∧ nCol A B C ∧ nCol A B D)) by (conclude_def Cut ).
assert ((BetS A F B ∧ BetS C F D ∧ nCol A B C ∧ nCol A B D)) by (conclude_def Cut ).
assert (Col A E B) by (conclude_def Col ).
assert (Col A B E) by (forward_using lemma_collinearorder).
assert (Col A F B) by (conclude_def Col ).
assert (Col A B F) by (forward_using lemma_collinearorder).
assert (neq A B) by (forward_using lemma_betweennotequal).
assert (Col B E F) by (conclude lemma_collinear4).
assert (Col E F B) by (forward_using lemma_collinearorder).
assert (Col C E D) by (conclude_def Col ).
assert (Col C F D) by (conclude_def Col ).
assert (Col C D F) by (forward_using lemma_collinearorder).
assert (Col C D E) by (forward_using lemma_collinearorder).
assert (neq C D) by (forward_using lemma_betweennotequal).
assert (Col D E F) by (conclude lemma_collinear4).
assert (Col E F D) by (forward_using lemma_collinearorder).
assert (Col D C E) by (conclude lemma_collinear1).
assert (Col D C F) by (conclude lemma_collinear1).
assert (BetS D E C) by (conclude axiom_betweennesssymmetry).
assert (neq D C) by (forward_using lemma_betweennotequal).
assert (Col C E F) by (conclude lemma_collinear4).
assert (Col E F C) by (forward_using lemma_collinearorder).
assert (¬ neq E F).
 {
 intro.
 assert (Col F B C) by (conclude lemma_collinear4).
 assert (Col F B D) by (conclude lemma_collinear4).
 assert (¬ eq F B).
  {
  intro.
  assert (Col F C D) by (conclude_def Col ).
  assert (Col B C D) by (conclude cn_equalitysub).
  contradict.
  }
 assert (Col B C D) by (conclude lemma_collinear4).
 contradict.
 }
close.
Qed.

End Euclid.