Require Export GeoCoq.Elements.OriginalProofs.lemma_Euclid4.
Require Export GeoCoq.Elements.OriginalProofs.proposition_28C.
Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelflip.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_twoperpsparallel : 
   forall A B C D, 
   Per A B C -> Per B C D -> OS A D B C ->
   Par A B C D.
Proof.
(* Goal: forall (A B C D : @Point Ax) (_ : @Per Ax A B C) (_ : @Per Ax B C D) (_ : @OS Ax A D B C), @Par Ax A B C D *)
intros.
(* Goal: @Par Ax A B C D *)
assert (nCol A B C) by (conclude lemma_rightangleNC).
(* Goal: @Par Ax A B C D *)
assert (neq B C) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:exists E, (BetS B C E /\ Cong C E B C)) by (conclude lemma_extension);destruct Tf as [E];spliter.
(* Goal: @Par Ax A B C D *)
assert (Col B C E) by (conclude_def Col ).
(* Goal: @Par Ax A B C D *)
assert (neq C E) by (forward_using lemma_betweennotequal).
(* Goal: @Par Ax A B C D *)
assert (neq E C) by (conclude lemma_inequalitysymmetric).
(* Goal: @Par Ax A B C D *)
assert (Per E C D) by (conclude lemma_collinearright).
(* Goal: @Par Ax A B C D *)
assert (Per D C E) by (conclude lemma_8_2).
(* Goal: @Par Ax A B C D *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: @Par Ax A B C D *)
assert (nCol B C D) by (conclude lemma_rightangleNC).
(* Goal: @Par Ax A B C D *)
assert (neq C D) by (forward_using lemma_NCdistinct).
(* Goal: @Par Ax A B C D *)
assert (Out C D D) by (conclude lemma_ray4).
(* Goal: @Par Ax A B C D *)
assert (Supp B C D D E) by (conclude_def Supp ).
(* Goal: @Par Ax A B C D *)
assert (CongA A B C B C D) by (conclude lemma_Euclid4).
(* Goal: @Par Ax A B C D *)
assert (CongA B C D D C E) by (conclude lemma_Euclid4).
(* Goal: @Par Ax A B C D *)
assert (RT A B C B C D) by (conclude_def RT ).
(* Goal: @Par Ax A B C D *)
assert (Par B A C D) by (conclude proposition_28C).
(* Goal: @Par Ax A B C D *)
assert (Par C D B A) by (conclude lemma_parallelsymmetric).
(* Goal: @Par Ax A B C D *)
assert (Par C D A B) by (forward_using lemma_parallelflip).
(* Goal: @Par Ax A B C D *)
assert (Par A B C D) by (conclude lemma_parallelsymmetric).
(* Goal: @Par Ax A B C D *)
close.
Qed.

End Euclid.


