Require Export GeoCoq.Elements.OriginalProofs.lemma_squareparallelogram.

Section Euclid.

Context `{Ax1:euclidean_euclidean}.

Lemma lemma_squareunique : 
   forall A B C D E, 
   SQ A B C D -> SQ A B C E ->
   eq E D.
Proof.
(* Goal: forall (A B C D E : @Point Ax0) (_ : @SQ Ax0 A B C D) (_ : @SQ Ax0 A B C E), @eq Ax0 E D *)
intros.
(* Goal: @eq Ax0 E D *)
assert (PG A B C D) by (conclude lemma_squareparallelogram).
let Tf:=fresh in
assert (Tf:exists M, (Midpoint A M C /\ Midpoint B M D)) by (conclude lemma_diagonalsbisect);destruct Tf as [M];spliter.
(* Goal: @eq Ax0 E D *)
assert (BetS B M D) by (conclude_def Midpoint ).
(* Goal: @eq Ax0 E D *)
assert (BetS A M C) by (conclude_def Midpoint ).
(* Goal: @eq Ax0 E D *)
assert (Per D A B) by (conclude_def SQ ).
(* Goal: @eq Ax0 E D *)
assert (Per E A B) by (conclude_def SQ ).
(* Goal: @eq Ax0 E D *)
assert (nCol D A B) by (conclude lemma_rightangleNC).
(* Goal: @eq Ax0 E D *)
assert (nCol E A B) by (conclude lemma_rightangleNC).
(* Goal: @eq Ax0 E D *)
assert (Cong A B A B) by (conclude cn_congruencereflexive).
(* Goal: @eq Ax0 E D *)
assert (Cong A B D A) by (conclude_def SQ ).
(* Goal: @eq Ax0 E D *)
assert (Cong A B E A) by (conclude_def SQ ).
(* Goal: @eq Ax0 E D *)
assert (Cong E A A B) by (conclude lemma_congruencesymmetric).
(* Goal: @eq Ax0 E D *)
assert (Cong E A D A) by (conclude lemma_congruencetransitive).
(* Goal: @eq Ax0 E D *)
assert (Cong A E A D) by (forward_using lemma_congruenceflip).
(* Goal: @eq Ax0 E D *)
assert (CongA E A B D A B) by (conclude lemma_Euclid4).
(* Goal: @eq Ax0 E D *)
assert ((Cong E B D B /\ CongA A E B A D B /\ CongA A B E A B D)) by (conclude proposition_04).
(* Goal: @eq Ax0 E D *)
assert (CongA A B D A B E) by (conclude lemma_equalanglessymmetric).
(* Goal: @eq Ax0 E D *)
assert (neq B E) by (forward_using lemma_NCdistinct).
(* Goal: @eq Ax0 E D *)
assert (neq B M) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists N, (Out B E N /\ Cong B N B M)) by (conclude lemma_layoff);destruct Tf as [N];spliter.
(* Goal: @eq Ax0 E D *)
assert (Cong B M B N) by (conclude lemma_congruencesymmetric).
(* Goal: @eq Ax0 E D *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: @eq Ax0 E D *)
assert (neq B A) by (forward_using lemma_NCdistinct).
(* Goal: @eq Ax0 E D *)
assert (Out B A A) by (conclude lemma_ray4).
(* Goal: @eq Ax0 E D *)
assert (Out B M D) by (conclude lemma_ray4).
(* Goal: @eq Ax0 E D *)
assert (Out B D M) by (conclude lemma_ray5).
(* Goal: @eq Ax0 E D *)
assert (nCol A B D) by (forward_using lemma_NCorder).
(* Goal: @eq Ax0 E D *)
assert (CongA A B D A B D) by (conclude lemma_equalanglesreflexive).
(* Goal: @eq Ax0 E D *)
assert (CongA A B D A B M) by (conclude lemma_equalangleshelper).
(* Goal: @eq Ax0 E D *)
assert (CongA A B M A B D) by (conclude lemma_equalanglessymmetric).
(* Goal: @eq Ax0 E D *)
assert (CongA A B M A B E) by (conclude lemma_equalanglestransitive).
(* Goal: @eq Ax0 E D *)
assert (nCol A B E) by (forward_using lemma_NCorder).
(* Goal: @eq Ax0 E D *)
assert (CongA A B E A B E) by (conclude lemma_equalanglesreflexive).
(* Goal: @eq Ax0 E D *)
assert (CongA A B E A B N) by (conclude lemma_equalangleshelper).
(* Goal: @eq Ax0 E D *)
assert (CongA A B M A B N) by (conclude lemma_equalanglestransitive).
(* Goal: @eq Ax0 E D *)
assert (Cong B A B A) by (conclude cn_congruencereflexive).
(* Goal: @eq Ax0 E D *)
assert (Cong A M A N) by (conclude proposition_04).
(* Goal: @eq Ax0 E D *)
assert (Per B C D) by (conclude_def SQ ).
(* Goal: @eq Ax0 E D *)
assert (Per B C E) by (conclude_def SQ ).
(* Goal: @eq Ax0 E D *)
assert (CongA B C E B C D) by (conclude lemma_Euclid4).
(* Goal: @eq Ax0 E D *)
assert (Cong A B C D) by (conclude_def SQ ).
(* Goal: @eq Ax0 E D *)
assert (Cong A B C E) by (conclude_def SQ ).
(* Goal: @eq Ax0 E D *)
assert (Cong C E A B) by (conclude lemma_congruencesymmetric).
(* Goal: @eq Ax0 E D *)
assert (Cong C E C D) by (conclude lemma_congruencetransitive).
(* Goal: @eq Ax0 E D *)
assert (nCol B C E) by (conclude lemma_rightangleNC).
(* Goal: @eq Ax0 E D *)
assert (nCol B C D) by (conclude lemma_rightangleNC).
(* Goal: @eq Ax0 E D *)
assert (Cong C B C B) by (conclude cn_congruencereflexive).
(* Goal: @eq Ax0 E D *)
assert ((Cong B E B D /\ CongA C B E C B D /\ CongA C E B C D B)) by (conclude proposition_04).
(* Goal: @eq Ax0 E D *)
assert (neq B C) by (forward_using lemma_NCdistinct).
(* Goal: @eq Ax0 E D *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: @eq Ax0 E D *)
assert (Out B C C) by (conclude lemma_ray4).
(* Goal: @eq Ax0 E D *)
assert (nCol B C D) by (conclude lemma_rightangleNC).
(* Goal: @eq Ax0 E D *)
assert (nCol C B D) by (forward_using lemma_NCorder).
(* Goal: @eq Ax0 E D *)
assert (CongA C B D C B D) by (conclude lemma_equalanglesreflexive).
(* Goal: @eq Ax0 E D *)
assert (CongA C B D C B M) by (conclude lemma_equalangleshelper).
(* Goal: @eq Ax0 E D *)
assert (nCol C B E) by (forward_using lemma_NCorder).
(* Goal: @eq Ax0 E D *)
assert (CongA C B E C B E) by (conclude lemma_equalanglesreflexive).
(* Goal: @eq Ax0 E D *)
assert (CongA C B E C B N) by (conclude lemma_equalangleshelper).
(* Goal: @eq Ax0 E D *)
assert (CongA C B E C B D) by (conclude lemma_equalanglestransitive).
(* Goal: @eq Ax0 E D *)
assert (CongA C B D C B E) by (conclude lemma_equalanglessymmetric).
(* Goal: @eq Ax0 E D *)
assert (CongA C B M C B D) by (conclude lemma_equalanglessymmetric).
(* Goal: @eq Ax0 E D *)
assert (CongA C B M C B E) by (conclude lemma_equalanglestransitive).
(* Goal: @eq Ax0 E D *)
assert (CongA C B M C B N) by (conclude lemma_equalanglestransitive).
(* Goal: @eq Ax0 E D *)
assert (CongA M B C N B C) by (conclude lemma_equalanglesflip).
(* Goal: @eq Ax0 E D *)
assert (Cong B C B C) by (conclude cn_congruencereflexive).
(* Goal: @eq Ax0 E D *)
assert (Cong M C N C) by (conclude (proposition_04 B M C B N C)).
(* Goal: @eq Ax0 E D *)
assert (Cong A C A C) by (conclude cn_congruencereflexive).
(* Goal: @eq Ax0 E D *)
assert (BetS A N C) by (conclude lemma_betweennesspreserved).
(* Goal: @eq Ax0 E D *)
assert (neq A M) by (forward_using lemma_betweennotequal).
(* Goal: @eq Ax0 E D *)
assert (Out A M C) by (conclude lemma_ray4).
(* Goal: @eq Ax0 E D *)
assert (neq A N) by (forward_using lemma_betweennotequal).
(* Goal: @eq Ax0 E D *)
assert (Out A N C) by (conclude lemma_ray4).
(* Goal: @eq Ax0 E D *)
assert (Out A C N) by (conclude lemma_ray5).
(* Goal: @eq Ax0 E D *)
assert (Out A C M) by (conclude lemma_ray5).
(* Goal: @eq Ax0 E D *)
assert (eq M N) by (conclude lemma_layoffunique).
(* Goal: @eq Ax0 E D *)
assert (Out B N E) by (conclude lemma_ray5).
(* Goal: @eq Ax0 E D *)
assert (Out B M D) by (conclude lemma_ray5).
(* Goal: @eq Ax0 E D *)
assert (Out B M E) by (conclude cn_equalitysub).
(* Goal: @eq Ax0 E D *)
assert (eq E D) by (conclude lemma_layoffunique).
(* Goal: @eq Ax0 E D *)
close.
Qed.

End Euclid.


