# Library GeoCoq.Elements.OriginalProofs.lemma_twolines2

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear4.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_twolines2 :

∀ 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.

intros.

assert (neq B A) by (conclude lemma_inequalitysymmetric).

assert (neq D C) by (conclude lemma_inequalitysymmetric).

assert (¬ neq P Q).

{

intro.

assert (Col D C P) by (forward_using lemma_collinearorder).

assert (Col D C Q) by (forward_using lemma_collinearorder).

assert (Col C P Q) by (conclude lemma_collinear4).

assert (Col A B P) by (forward_using lemma_collinearorder).

assert (Col A B Q) by (forward_using lemma_collinearorder).

assert (Col B P Q) by (conclude lemma_collinear4).

assert (Col P Q B) by (forward_using lemma_collinearorder).

assert (Col P Q C) by (forward_using lemma_collinearorder).

assert (Col Q C B) by (conclude lemma_collinear4).

assert (Col Q C D) by (forward_using lemma_collinearorder).

assert (¬ eq Q C).

{

intro.

assert (Col C P D) by (forward_using lemma_collinearorder).

assert (Col Q P B) by (forward_using lemma_collinearorder).

assert (Col B A Q) by (forward_using lemma_collinearorder).

assert (Col B A P) by (forward_using lemma_collinearorder).

assert (Col A Q P) by (conclude lemma_collinear4).

assert (Col Q P A) by (forward_using lemma_collinearorder).

assert (Col C P B) by (conclude cn_equalitysub).

assert (Col C P A) by (conclude cn_equalitysub).

assert (Col P C A) by (forward_using lemma_collinearorder).

assert (Col P C B) by (forward_using lemma_collinearorder).

assert (Col P C D) by (forward_using lemma_collinearorder).

assert (¬ eq P C).

{

intro.

assert (eq P Q) by (conclude cn_equalitysub).

contradict.

}

assert (Col C D A) by (conclude lemma_collinear4).

assert (Col C D B) by (conclude lemma_collinear4).

assert (Col A C D) by (forward_using lemma_collinearorder).

assert (Col B C D) by (forward_using lemma_collinearorder).

contradict.

}

assert (Col C B D) by (conclude lemma_collinear4).

assert (Col B C D) by (forward_using lemma_collinearorder).

assert (¬ eq B A).

{

intro.

assert (eq A B) by (conclude lemma_equalitysymmetric).

contradict.

}

assert (Col B A P) by (forward_using lemma_collinearorder).

assert (Col B A Q) by (forward_using lemma_collinearorder).

assert (Col A P Q) by (conclude lemma_collinear4).

assert (Col P Q A) by (forward_using lemma_collinearorder).

assert (Col P Q C) by (forward_using lemma_collinearorder).

assert (Col Q C A) by (conclude lemma_collinear4).

assert (Col Q C D) by (forward_using lemma_collinearorder).

assert (Col C A D) by (conclude lemma_collinear4).

assert (Col A C D) by (forward_using lemma_collinearorder).

contradict.

}

close.

Qed.

End Euclid.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_twolines2 :

∀ 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.

intros.

assert (neq B A) by (conclude lemma_inequalitysymmetric).

assert (neq D C) by (conclude lemma_inequalitysymmetric).

assert (¬ neq P Q).

{

intro.

assert (Col D C P) by (forward_using lemma_collinearorder).

assert (Col D C Q) by (forward_using lemma_collinearorder).

assert (Col C P Q) by (conclude lemma_collinear4).

assert (Col A B P) by (forward_using lemma_collinearorder).

assert (Col A B Q) by (forward_using lemma_collinearorder).

assert (Col B P Q) by (conclude lemma_collinear4).

assert (Col P Q B) by (forward_using lemma_collinearorder).

assert (Col P Q C) by (forward_using lemma_collinearorder).

assert (Col Q C B) by (conclude lemma_collinear4).

assert (Col Q C D) by (forward_using lemma_collinearorder).

assert (¬ eq Q C).

{

intro.

assert (Col C P D) by (forward_using lemma_collinearorder).

assert (Col Q P B) by (forward_using lemma_collinearorder).

assert (Col B A Q) by (forward_using lemma_collinearorder).

assert (Col B A P) by (forward_using lemma_collinearorder).

assert (Col A Q P) by (conclude lemma_collinear4).

assert (Col Q P A) by (forward_using lemma_collinearorder).

assert (Col C P B) by (conclude cn_equalitysub).

assert (Col C P A) by (conclude cn_equalitysub).

assert (Col P C A) by (forward_using lemma_collinearorder).

assert (Col P C B) by (forward_using lemma_collinearorder).

assert (Col P C D) by (forward_using lemma_collinearorder).

assert (¬ eq P C).

{

intro.

assert (eq P Q) by (conclude cn_equalitysub).

contradict.

}

assert (Col C D A) by (conclude lemma_collinear4).

assert (Col C D B) by (conclude lemma_collinear4).

assert (Col A C D) by (forward_using lemma_collinearorder).

assert (Col B C D) by (forward_using lemma_collinearorder).

contradict.

}

assert (Col C B D) by (conclude lemma_collinear4).

assert (Col B C D) by (forward_using lemma_collinearorder).

assert (¬ eq B A).

{

intro.

assert (eq A B) by (conclude lemma_equalitysymmetric).

contradict.

}

assert (Col B A P) by (forward_using lemma_collinearorder).

assert (Col B A Q) by (forward_using lemma_collinearorder).

assert (Col A P Q) by (conclude lemma_collinear4).

assert (Col P Q A) by (forward_using lemma_collinearorder).

assert (Col P Q C) by (forward_using lemma_collinearorder).

assert (Col Q C A) by (conclude lemma_collinear4).

assert (Col Q C D) by (forward_using lemma_collinearorder).

assert (Col C A D) by (conclude lemma_collinear4).

assert (Col A C D) by (forward_using lemma_collinearorder).

contradict.

}

close.

Qed.

End Euclid.