Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear4.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_twolines : 
   forall 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.
(* Goal: forall (A B C D E F : @Point Ax) (_ : @Cut Ax A B C D E) (_ : @Cut Ax A B C D F) (_ : @nCol Ax B C D), @eq Ax E F *)
intros.
(* Goal: @eq Ax E F *)
assert ((BetS A E B /\ BetS C E D /\ nCol A B C /\ nCol A B D)) by (conclude_def Cut ).
(* Goal: @eq Ax E F *)
assert ((BetS A F B /\ BetS C F D /\ nCol A B C /\ nCol A B D)) by (conclude_def Cut ).
(* Goal: @eq Ax E F *)
assert (Col A E B) by (conclude_def Col ).
(* Goal: @eq Ax E F *)
assert (Col A B E) by (forward_using lemma_collinearorder).
(* Goal: @eq Ax E F *)
assert (Col A F B) by (conclude_def Col ).
(* Goal: @eq Ax E F *)
assert (Col A B F) by (forward_using lemma_collinearorder).
(* Goal: @eq Ax E F *)
assert (neq A B) by (forward_using lemma_betweennotequal).
(* Goal: @eq Ax E F *)
assert (Col B E F) by (conclude lemma_collinear4).
(* Goal: @eq Ax E F *)
assert (Col E F B) by (forward_using lemma_collinearorder).
(* Goal: @eq Ax E F *)
assert (Col C E D) by (conclude_def Col ).
(* Goal: @eq Ax E F *)
assert (Col C F D) by (conclude_def Col ).
(* Goal: @eq Ax E F *)
assert (Col C D F) by (forward_using lemma_collinearorder).
(* Goal: @eq Ax E F *)
assert (Col C D E) by (forward_using lemma_collinearorder).
(* Goal: @eq Ax E F *)
assert (neq C D) by (forward_using lemma_betweennotequal).
(* Goal: @eq Ax E F *)
assert (Col D E F) by (conclude lemma_collinear4).
(* Goal: @eq Ax E F *)
assert (Col E F D) by (forward_using lemma_collinearorder).
(* Goal: @eq Ax E F *)
assert (Col D C E) by (conclude lemma_collinear1).
(* Goal: @eq Ax E F *)
assert (Col D C F) by (conclude lemma_collinear1).
(* Goal: @eq Ax E F *)
assert (BetS D E C) by (conclude axiom_betweennesssymmetry).
(* Goal: @eq Ax E F *)
assert (neq D C) by (forward_using lemma_betweennotequal).
(* Goal: @eq Ax E F *)
assert (Col C E F) by (conclude lemma_collinear4).
(* Goal: @eq Ax E F *)
assert (Col E F C) by (forward_using lemma_collinearorder).
(* Goal: @eq Ax E F *)
assert (~ neq E F).
(* Goal: not (@eq Ax F B) *)
(* Goal: False *)
 {
(* Goal: not (@eq Ax F B) *)
 intro.
(* Goal: False *)
 assert (Col F B C) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col F B D) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (~ eq F B).
(* Goal: not (@eq Ax F B) *)
(* Goal: False *)
  {
(* Goal: not (@eq Ax F B) *)
  intro.
(* Goal: False *)
  assert (Col F C D) by (conclude_def Col ).
(* Goal: False *)
  assert (Col B C D) by (conclude cn_equalitysub).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (Col B C D) by (conclude lemma_collinear4).
(* Goal: False *)
 contradict.
 }
(* Goal: @eq Ax E F *)
close.
Qed.

End Euclid.


