Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear5.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_NChelper : 
   forall 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.
(* Goal: forall (A B C P Q : @Point Ax0) (_ : @nCol Ax0 A B C) (_ : @Col Ax0 A B P) (_ : @Col Ax0 A B Q) (_ : @neq Ax0 P Q), @nCol Ax0 P Q C *)
intros.
(* Goal: @nCol Ax0 P Q C *)
assert (~ eq A B).
(* Goal: not (@Col Ax0 P Q C) *)
(* Goal: @nCol Ax0 P Q C *)
 {
(* Goal: not (@Col Ax0 P Q C) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @nCol Ax0 P Q C *)
assert (Col B P Q) by (conclude lemma_collinear4).
(* Goal: @nCol Ax0 P Q C *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
(* Goal: @nCol Ax0 P Q C *)
assert (Col B A P) by (forward_using lemma_collinearorder).
(* Goal: @nCol Ax0 P Q C *)
assert (Col B A Q) by (forward_using lemma_collinearorder).
(* Goal: @nCol Ax0 P Q C *)
assert (Col A P Q) by (conclude lemma_collinear4).
(* Goal: @nCol Ax0 P Q C *)
assert (Col P Q A) by (forward_using lemma_collinearorder).
(* Goal: @nCol Ax0 P Q C *)
assert (Col P Q B) by (forward_using lemma_collinearorder).
(* Goal: @nCol Ax0 P Q C *)
assert (~ Col P Q C).
(* Goal: not (@Col Ax0 P Q C) *)
(* Goal: @nCol Ax0 P Q C *)
 {
(* Goal: not (@Col Ax0 P Q C) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude lemma_collinear5).
(* Goal: False *)
 contradict.
 }
(* Goal: @nCol Ax0 P Q C *)
close.
Qed.

End Euclid.


