Require Export GeoCoq.Elements.OriginalProofs.lemma_squareparallelogram.
Require Export GeoCoq.Elements.OriginalProofs.lemma_PGrectangle.

Section Euclid.

Context `{Ax1:euclidean_euclidean}.

Lemma lemma_squarerectangle : 
   forall A B C D, 
   SQ A B C D ->
   RE A B C D.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @SQ Ax0 A B C D), @RE Ax0 A B C D *)
intros.
(* Goal: @RE Ax0 A B C D *)
assert (PG A B C D) by (conclude lemma_squareparallelogram).
(* Goal: @RE Ax0 A B C D *)
assert (Per D A B) by (conclude_def SQ ).
(* Goal: @RE Ax0 A B C D *)
assert (RE A B C D) by (conclude lemma_PGrectangle).
(* Goal: @RE Ax0 A B C D *)
close.
Qed.

End Euclid.


