Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear4.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_twolines2 : 
   forall A B C D P Q, 
   neq A B -> neq C D -> Col P A B -> Col P C D -> Col Q A B -> Col Q C D -> ~ (Col A C D /\ Col B C D) ->
   eq P Q.
Proof.
(* Goal: forall (A B C D P Q : @Point Ax) (_ : @neq Ax A B) (_ : @neq Ax C D) (_ : @Col Ax P A B) (_ : @Col Ax P C D) (_ : @Col Ax Q A B) (_ : @Col Ax Q C D) (_ : not (and (@Col Ax A C D) (@Col Ax B C D))), @eq Ax P Q *)
intros.
(* Goal: @eq Ax P Q *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
(* Goal: @eq Ax P Q *)
assert (neq D C) by (conclude lemma_inequalitysymmetric).
(* Goal: @eq Ax P Q *)
assert (~ neq P Q).
(* Goal: not (@eq Ax B A) *)
(* Goal: False *)
 {
(* Goal: not (@eq Ax B A) *)
 intro.
(* Goal: False *)
 assert (Col D C P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col D C Q) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col C P Q) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A B P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col A B Q) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col B P Q) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col P Q B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col P Q C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col Q C B) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col Q C D) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (~ eq Q C).
(* Goal: not (@eq Ax B A) *)
(* Goal: False *)
  {
(* Goal: not (@eq Ax B A) *)
  intro.
(* Goal: False *)
  assert (Col C P D) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (Col Q P B) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (Col B A Q) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (Col B A P) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (Col A Q P) by (conclude lemma_collinear4).
(* Goal: False *)
  assert (Col Q P A) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (Col C P B) by (conclude cn_equalitysub).
(* Goal: False *)
  assert (Col C P A) by (conclude cn_equalitysub).
(* Goal: False *)
  assert (Col P C A) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (Col P C B) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (Col P C D) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (~ eq P C).
(* Goal: not (@eq Ax B A) *)
(* Goal: False *)
   {
(* Goal: not (@eq Ax B A) *)
   intro.
(* Goal: False *)
   assert (eq P Q) by (conclude cn_equalitysub).
(* Goal: False *)
   contradict.
   }
(* Goal: False *)
  assert (Col C D A) by (conclude lemma_collinear4).
(* Goal: False *)
  assert (Col C D B) by (conclude lemma_collinear4).
(* Goal: False *)
  assert (Col A C D) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (Col B C D) by (forward_using lemma_collinearorder).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (Col C B D) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col B C D) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (~ eq B A).
(* Goal: not (@eq Ax B A) *)
(* Goal: False *)
  {
(* Goal: not (@eq Ax B A) *)
  intro.
(* Goal: False *)
  assert (eq A B) by (conclude lemma_equalitysymmetric).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (Col B A P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col B A Q) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col A P Q) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col P Q A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col P Q C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col Q C A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col Q C D) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col C A D) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A C D) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @eq Ax P Q *)
close.
Qed.

End Euclid.


