# Library GeoCoq.Elements.OriginalProofs.lemma_NChelper

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear5.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_NChelper :

∀ A B C P Q,

nCol A B C → Col A B P → Col A B Q → neq P Q →

nCol P Q C.

Proof.

intros.

assert (¬ eq A B).

{

intro.

assert (Col A B C) by (conclude_def Col ).

contradict.

}

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

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

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 B) by (forward_using lemma_collinearorder).

assert (¬ Col P Q C).

{

intro.

assert (Col A B C) by (conclude lemma_collinear5).

contradict.

}

close.

Qed.

End Euclid.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_NChelper :

∀ A B C P Q,

nCol A B C → Col A B P → Col A B Q → neq P Q →

nCol P Q C.

Proof.

intros.

assert (¬ eq A B).

{

intro.

assert (Col A B C) by (conclude_def Col ).

contradict.

}

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

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

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 B) by (forward_using lemma_collinearorder).

assert (¬ Col P Q C).

{

intro.

assert (Col A B C) by (conclude lemma_collinear5).

contradict.

}

close.

Qed.

End Euclid.