Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear4.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_collinearparallel : 
   forall A B C c d, 
   Par A B c d -> Col c d C -> neq C d ->
   Par A B C d.
Proof.
(* Goal: forall (A B C c d : @Point Ax0) (_ : @Par Ax0 A B c d) (_ : @Col Ax0 c d C) (_ : @neq Ax0 C d), @Par Ax0 A B C d *)
intros.
let Tf:=fresh in
assert (Tf:exists R a b p q, (neq A B /\ neq c d /\ Col A B a /\ Col A B b /\ neq a b /\ Col c d p /\ Col c d q /\ neq p q /\ ~ Meet A B c d /\ BetS a R q /\ BetS p R b)) by (conclude_def Par );destruct Tf as [R[a[b[p[q]]]]];spliter.
(* Goal: @Par Ax0 A B C d *)
assert (neq d C) by (conclude lemma_inequalitysymmetric).
(* Goal: @Par Ax0 A B C d *)
assert (Col d C p) by (conclude lemma_collinear4).
(* Goal: @Par Ax0 A B C d *)
assert (Col C d p) by (forward_using lemma_collinearorder).
(* Goal: @Par Ax0 A B C d *)
assert (Col d C q) by (conclude lemma_collinear4).
(* Goal: @Par Ax0 A B C d *)
assert (Col C d q) by (forward_using lemma_collinearorder).
(* Goal: @Par Ax0 A B C d *)
assert (~ Meet A B C d).
(* Goal: not (@Meet Ax0 A B C d) *)
(* Goal: @Par Ax0 A B C d *)
 {
(* Goal: not (@Meet Ax0 A B C d) *)
 intro.
 let Tf:=fresh in
 assert (Tf:exists E, (neq A B /\ neq C d /\ Col A B E /\ Col C d E)) by (conclude_def Meet );destruct Tf as [E];spliter.
(* Goal: False *)
 assert (Col C d c) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col d E c) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col c d E) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Meet A B c d) by (conclude_def Meet ).
(* Goal: False *)
 contradict.
 }
(* Goal: @Par Ax0 A B C d *)
assert (Par A B C d) by (conclude_def Par ).
(* Goal: @Par Ax0 A B C d *)
close.
Qed.

End Euclid.


