Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelsymmetric.
Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelflip.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_PGsymmetric : 
   forall A B C D, 
   PG A B C D ->
   PG C D A B.
Proof.
(* Goal: forall (A B C D : @Point Ax1) (_ : @PG Ax1 A B C D), @PG Ax1 C D A B *)
intros.
(* Goal: @PG Ax1 C D A B *)
assert ((Par A B C D /\ Par A D B C)) by (conclude_def PG ).
(* Goal: @PG Ax1 C D A B *)
assert (Par C D A B) by (conclude lemma_parallelsymmetric).
(* Goal: @PG Ax1 C D A B *)
assert (Par B C A D) by (conclude lemma_parallelsymmetric).
(* Goal: @PG Ax1 C D A B *)
assert (Par C B D A) by (forward_using lemma_parallelflip).
(* Goal: @PG Ax1 C D A B *)
assert (PG C D A B) by (conclude_def PG ).
(* Goal: @PG Ax1 C D A B *)
close.
Qed.

End Euclid.


