# Library GeoCoq.Elements.OriginalProofs.lemma_squareunique

Require Export GeoCoq.Elements.OriginalProofs.lemma_squareparallelogram.

Section Euclid.

Context `{Ax1:euclidean_euclidean}.

Lemma lemma_squareunique :

∀ A B C D E,

SQ A B C D → SQ A B C E →

eq E D.

Proof.

intros.

assert (PG A B C D) by (conclude lemma_squareparallelogram).

let Tf:=fresh in

assert (Tf:∃ M, (Midpoint A M C ∧ Midpoint B M D)) by (conclude lemma_diagonalsbisect);destruct Tf as [M];spliter.

assert (BetS B M D) by (conclude_def Midpoint ).

assert (BetS A M C) by (conclude_def Midpoint ).

assert (Per D A B) by (conclude_def SQ ).

assert (Per E A B) by (conclude_def SQ ).

assert (nCol D A B) by (conclude lemma_rightangleNC).

assert (nCol E A B) by (conclude lemma_rightangleNC).

assert (Cong A B A B) by (conclude cn_congruencereflexive).

assert (Cong A B D A) by (conclude_def SQ ).

assert (Cong A B E A) by (conclude_def SQ ).

assert (Cong E A A B) by (conclude lemma_congruencesymmetric).

assert (Cong E A D A) by (conclude lemma_congruencetransitive).

assert (Cong A E A D) by (forward_using lemma_congruenceflip).

assert (CongA E A B D A B) by (conclude lemma_Euclid4).

assert ((Cong E B D B ∧ CongA A E B A D B ∧ CongA A B E A B D)) by (conclude proposition_04).

assert (CongA A B D A B E) by (conclude lemma_equalanglessymmetric).

assert (neq B E) by (forward_using lemma_NCdistinct).

assert (neq B M) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

assert (Tf:∃ N, (Out B E N ∧ Cong B N B M)) by (conclude lemma_layoff);destruct Tf as [N];spliter.

assert (Cong B M B N) by (conclude lemma_congruencesymmetric).

assert (eq A A) by (conclude cn_equalityreflexive).

assert (neq B A) by (forward_using lemma_NCdistinct).

assert (Out B A A) by (conclude lemma_ray4).

assert (Out B M D) by (conclude lemma_ray4).

assert (Out B D M) by (conclude lemma_ray5).

assert (nCol A B D) by (forward_using lemma_NCorder).

assert (CongA A B D A B D) by (conclude lemma_equalanglesreflexive).

assert (CongA A B D A B M) by (conclude lemma_equalangleshelper).

assert (CongA A B M A B D) by (conclude lemma_equalanglessymmetric).

assert (CongA A B M A B E) by (conclude lemma_equalanglestransitive).

assert (nCol A B E) by (forward_using lemma_NCorder).

assert (CongA A B E A B E) by (conclude lemma_equalanglesreflexive).

assert (CongA A B E A B N) by (conclude lemma_equalangleshelper).

assert (CongA A B M A B N) by (conclude lemma_equalanglestransitive).

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (Cong A M A N) by (conclude proposition_04).

assert (Per B C D) by (conclude_def SQ ).

assert (Per B C E) by (conclude_def SQ ).

assert (CongA B C E B C D) by (conclude lemma_Euclid4).

assert (Cong A B C D) by (conclude_def SQ ).

assert (Cong A B C E) by (conclude_def SQ ).

assert (Cong C E A B) by (conclude lemma_congruencesymmetric).

assert (Cong C E C D) by (conclude lemma_congruencetransitive).

assert (nCol B C E) by (conclude lemma_rightangleNC).

assert (nCol B C D) by (conclude lemma_rightangleNC).

assert (Cong C B C B) by (conclude cn_congruencereflexive).

assert ((Cong B E B D ∧ CongA C B E C B D ∧ CongA C E B C D B)) by (conclude proposition_04).

assert (neq B C) by (forward_using lemma_NCdistinct).

assert (eq C C) by (conclude cn_equalityreflexive).

assert (Out B C C) by (conclude lemma_ray4).

assert (nCol B C D) by (conclude lemma_rightangleNC).

assert (nCol C B D) by (forward_using lemma_NCorder).

assert (CongA C B D C B D) by (conclude lemma_equalanglesreflexive).

assert (CongA C B D C B M) by (conclude lemma_equalangleshelper).

assert (nCol C B E) by (forward_using lemma_NCorder).

assert (CongA C B E C B E) by (conclude lemma_equalanglesreflexive).

assert (CongA C B E C B N) by (conclude lemma_equalangleshelper).

assert (CongA C B E C B D) by (conclude lemma_equalanglestransitive).

assert (CongA C B D C B E) by (conclude lemma_equalanglessymmetric).

assert (CongA C B M C B D) by (conclude lemma_equalanglessymmetric).

assert (CongA C B M C B E) by (conclude lemma_equalanglestransitive).

assert (CongA C B M C B N) by (conclude lemma_equalanglestransitive).

assert (CongA M B C N B C) by (conclude lemma_equalanglesflip).

assert (Cong B C B C) by (conclude cn_congruencereflexive).

assert (Cong M C N C) by (conclude (proposition_04 B M C B N C)).

assert (Cong A C A C) by (conclude cn_congruencereflexive).

assert (BetS A N C) by (conclude lemma_betweennesspreserved).

assert (neq A M) by (forward_using lemma_betweennotequal).

assert (Out A M C) by (conclude lemma_ray4).

assert (neq A N) by (forward_using lemma_betweennotequal).

assert (Out A N C) by (conclude lemma_ray4).

assert (Out A C N) by (conclude lemma_ray5).

assert (Out A C M) by (conclude lemma_ray5).

assert (eq M N) by (conclude lemma_layoffunique).

assert (Out B N E) by (conclude lemma_ray5).

assert (Out B M D) by (conclude lemma_ray5).

assert (Out B M E) by (conclude cn_equalitysub).

assert (eq E D) by (conclude lemma_layoffunique).

close.

Qed.

End Euclid.

Section Euclid.

Context `{Ax1:euclidean_euclidean}.

Lemma lemma_squareunique :

∀ A B C D E,

SQ A B C D → SQ A B C E →

eq E D.

Proof.

intros.

assert (PG A B C D) by (conclude lemma_squareparallelogram).

let Tf:=fresh in

assert (Tf:∃ M, (Midpoint A M C ∧ Midpoint B M D)) by (conclude lemma_diagonalsbisect);destruct Tf as [M];spliter.

assert (BetS B M D) by (conclude_def Midpoint ).

assert (BetS A M C) by (conclude_def Midpoint ).

assert (Per D A B) by (conclude_def SQ ).

assert (Per E A B) by (conclude_def SQ ).

assert (nCol D A B) by (conclude lemma_rightangleNC).

assert (nCol E A B) by (conclude lemma_rightangleNC).

assert (Cong A B A B) by (conclude cn_congruencereflexive).

assert (Cong A B D A) by (conclude_def SQ ).

assert (Cong A B E A) by (conclude_def SQ ).

assert (Cong E A A B) by (conclude lemma_congruencesymmetric).

assert (Cong E A D A) by (conclude lemma_congruencetransitive).

assert (Cong A E A D) by (forward_using lemma_congruenceflip).

assert (CongA E A B D A B) by (conclude lemma_Euclid4).

assert ((Cong E B D B ∧ CongA A E B A D B ∧ CongA A B E A B D)) by (conclude proposition_04).

assert (CongA A B D A B E) by (conclude lemma_equalanglessymmetric).

assert (neq B E) by (forward_using lemma_NCdistinct).

assert (neq B M) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

assert (Tf:∃ N, (Out B E N ∧ Cong B N B M)) by (conclude lemma_layoff);destruct Tf as [N];spliter.

assert (Cong B M B N) by (conclude lemma_congruencesymmetric).

assert (eq A A) by (conclude cn_equalityreflexive).

assert (neq B A) by (forward_using lemma_NCdistinct).

assert (Out B A A) by (conclude lemma_ray4).

assert (Out B M D) by (conclude lemma_ray4).

assert (Out B D M) by (conclude lemma_ray5).

assert (nCol A B D) by (forward_using lemma_NCorder).

assert (CongA A B D A B D) by (conclude lemma_equalanglesreflexive).

assert (CongA A B D A B M) by (conclude lemma_equalangleshelper).

assert (CongA A B M A B D) by (conclude lemma_equalanglessymmetric).

assert (CongA A B M A B E) by (conclude lemma_equalanglestransitive).

assert (nCol A B E) by (forward_using lemma_NCorder).

assert (CongA A B E A B E) by (conclude lemma_equalanglesreflexive).

assert (CongA A B E A B N) by (conclude lemma_equalangleshelper).

assert (CongA A B M A B N) by (conclude lemma_equalanglestransitive).

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (Cong A M A N) by (conclude proposition_04).

assert (Per B C D) by (conclude_def SQ ).

assert (Per B C E) by (conclude_def SQ ).

assert (CongA B C E B C D) by (conclude lemma_Euclid4).

assert (Cong A B C D) by (conclude_def SQ ).

assert (Cong A B C E) by (conclude_def SQ ).

assert (Cong C E A B) by (conclude lemma_congruencesymmetric).

assert (Cong C E C D) by (conclude lemma_congruencetransitive).

assert (nCol B C E) by (conclude lemma_rightangleNC).

assert (nCol B C D) by (conclude lemma_rightangleNC).

assert (Cong C B C B) by (conclude cn_congruencereflexive).

assert ((Cong B E B D ∧ CongA C B E C B D ∧ CongA C E B C D B)) by (conclude proposition_04).

assert (neq B C) by (forward_using lemma_NCdistinct).

assert (eq C C) by (conclude cn_equalityreflexive).

assert (Out B C C) by (conclude lemma_ray4).

assert (nCol B C D) by (conclude lemma_rightangleNC).

assert (nCol C B D) by (forward_using lemma_NCorder).

assert (CongA C B D C B D) by (conclude lemma_equalanglesreflexive).

assert (CongA C B D C B M) by (conclude lemma_equalangleshelper).

assert (nCol C B E) by (forward_using lemma_NCorder).

assert (CongA C B E C B E) by (conclude lemma_equalanglesreflexive).

assert (CongA C B E C B N) by (conclude lemma_equalangleshelper).

assert (CongA C B E C B D) by (conclude lemma_equalanglestransitive).

assert (CongA C B D C B E) by (conclude lemma_equalanglessymmetric).

assert (CongA C B M C B D) by (conclude lemma_equalanglessymmetric).

assert (CongA C B M C B E) by (conclude lemma_equalanglestransitive).

assert (CongA C B M C B N) by (conclude lemma_equalanglestransitive).

assert (CongA M B C N B C) by (conclude lemma_equalanglesflip).

assert (Cong B C B C) by (conclude cn_congruencereflexive).

assert (Cong M C N C) by (conclude (proposition_04 B M C B N C)).

assert (Cong A C A C) by (conclude cn_congruencereflexive).

assert (BetS A N C) by (conclude lemma_betweennesspreserved).

assert (neq A M) by (forward_using lemma_betweennotequal).

assert (Out A M C) by (conclude lemma_ray4).

assert (neq A N) by (forward_using lemma_betweennotequal).

assert (Out A N C) by (conclude lemma_ray4).

assert (Out A C N) by (conclude lemma_ray5).

assert (Out A C M) by (conclude lemma_ray5).

assert (eq M N) by (conclude lemma_layoffunique).

assert (Out B N E) by (conclude lemma_ray5).

assert (Out B M D) by (conclude lemma_ray5).

assert (Out B M E) by (conclude cn_equalitysub).

assert (eq E D) by (conclude lemma_layoffunique).

close.

Qed.

End Euclid.