# Library GeoCoq.Elements.OriginalProofs.lemma_squaresequal

Require Export GeoCoq.Elements.OriginalProofs.lemma_squarerectangle.

Section Euclid.

Context `{Ax1:area}.

Lemma lemma_squaresequal :

∀ A B C D a b c d,

Cong A B a b → SQ A B C D → SQ a b c d →

EF A B C D a b c d.

Proof.

intros.

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

assert (Per d a b) by (conclude_def SQ ).

assert (CongA D A B d a b) by (conclude lemma_Euclid4).

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

assert (Cong a b d a) by (conclude_def SQ ).

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

assert (Cong D A a b) by (conclude lemma_congruencetransitive).

assert (Cong D A d a) by (conclude lemma_congruencetransitive).

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

assert (PG a b c d) by (conclude lemma_squareparallelogram).

assert (Par A B C D) by (conclude_def PG ).

assert (Par a b c d) by (conclude_def PG ).

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

assert (nCol a b d) by (forward_using lemma_parallelNC).

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

assert (nCol d a b) by (forward_using lemma_NCorder).

assert (Triangle D A B) by (conclude_def Triangle ).

assert (Triangle d a b) by (conclude_def Triangle ).

assert (Cong A D a d) by (forward_using lemma_congruenceflip).

assert (Cong D B d b) by (conclude proposition_04).

assert (Cong B D b d) by (forward_using lemma_congruenceflip).

assert (Cong_3 A B D a b d) by (conclude_def Cong_3 ).

assert (ET A B D a b d) by (conclude axiom_congruentequal).

assert (ET A B D b d a) by (forward_using axiom_ETpermutation).

assert (ET b d a A B D) by (conclude axiom_ETsymmetric).

assert (ET b d a B D A) by (forward_using axiom_ETpermutation).

assert (ET B D A b d a) by (conclude axiom_ETsymmetric).

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

assert (Cong a b b c) by (conclude_def SQ ).

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

assert (Cong a b c d) by (conclude_def SQ ).

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

assert (Cong B C a b) by (conclude lemma_congruencetransitive).

assert (Cong B C b c) by (conclude lemma_congruencetransitive).

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

assert (Cong C D a b) by (conclude lemma_congruencetransitive).

assert (Cong C D c d) by (conclude lemma_congruencetransitive).

assert (Cong_3 B C D b c d) by (conclude_def Cong_3 ).

assert (ET B C D b c d) by (conclude axiom_congruentequal).

assert (ET B C D b d c) by (forward_using axiom_ETpermutation).

assert (ET b d c B C D) by (conclude axiom_ETsymmetric).

assert (ET b d c B D C) by (forward_using axiom_ETpermutation).

assert (ET B D C b d c) by (conclude axiom_ETsymmetric).

assert (RE A B C D) by (conclude lemma_squarerectangle).

assert (CR A C B D) by (conclude_def RE ).

assert (nCol A C D) by (forward_using lemma_parallelNC).

assert (TS A B D C) by (forward_using lemma_crossimpliesopposite).

assert (RE a b c d) by (conclude lemma_squarerectangle).

assert (CR a c b d) by (conclude_def RE ).

assert (nCol a c d) by (forward_using lemma_parallelNC).

assert (TS a b d c) by (forward_using lemma_crossimpliesopposite).

assert (EF B A D C b a d c) by (conclude axiom_paste3).

assert (EF B A D C a b c d) by (forward_using axiom_EFpermutation).

assert (EF a b c d B A D C) by (conclude axiom_EFsymmetric).

assert (EF a b c d A B C D) by (forward_using axiom_EFpermutation).

assert (EF A B C D a b c d) by (conclude axiom_EFsymmetric).

close.

Qed.

End Euclid.

Section Euclid.

Context `{Ax1:area}.

Lemma lemma_squaresequal :

∀ A B C D a b c d,

Cong A B a b → SQ A B C D → SQ a b c d →

EF A B C D a b c d.

Proof.

intros.

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

assert (Per d a b) by (conclude_def SQ ).

assert (CongA D A B d a b) by (conclude lemma_Euclid4).

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

assert (Cong a b d a) by (conclude_def SQ ).

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

assert (Cong D A a b) by (conclude lemma_congruencetransitive).

assert (Cong D A d a) by (conclude lemma_congruencetransitive).

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

assert (PG a b c d) by (conclude lemma_squareparallelogram).

assert (Par A B C D) by (conclude_def PG ).

assert (Par a b c d) by (conclude_def PG ).

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

assert (nCol a b d) by (forward_using lemma_parallelNC).

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

assert (nCol d a b) by (forward_using lemma_NCorder).

assert (Triangle D A B) by (conclude_def Triangle ).

assert (Triangle d a b) by (conclude_def Triangle ).

assert (Cong A D a d) by (forward_using lemma_congruenceflip).

assert (Cong D B d b) by (conclude proposition_04).

assert (Cong B D b d) by (forward_using lemma_congruenceflip).

assert (Cong_3 A B D a b d) by (conclude_def Cong_3 ).

assert (ET A B D a b d) by (conclude axiom_congruentequal).

assert (ET A B D b d a) by (forward_using axiom_ETpermutation).

assert (ET b d a A B D) by (conclude axiom_ETsymmetric).

assert (ET b d a B D A) by (forward_using axiom_ETpermutation).

assert (ET B D A b d a) by (conclude axiom_ETsymmetric).

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

assert (Cong a b b c) by (conclude_def SQ ).

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

assert (Cong a b c d) by (conclude_def SQ ).

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

assert (Cong B C a b) by (conclude lemma_congruencetransitive).

assert (Cong B C b c) by (conclude lemma_congruencetransitive).

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

assert (Cong C D a b) by (conclude lemma_congruencetransitive).

assert (Cong C D c d) by (conclude lemma_congruencetransitive).

assert (Cong_3 B C D b c d) by (conclude_def Cong_3 ).

assert (ET B C D b c d) by (conclude axiom_congruentequal).

assert (ET B C D b d c) by (forward_using axiom_ETpermutation).

assert (ET b d c B C D) by (conclude axiom_ETsymmetric).

assert (ET b d c B D C) by (forward_using axiom_ETpermutation).

assert (ET B D C b d c) by (conclude axiom_ETsymmetric).

assert (RE A B C D) by (conclude lemma_squarerectangle).

assert (CR A C B D) by (conclude_def RE ).

assert (nCol A C D) by (forward_using lemma_parallelNC).

assert (TS A B D C) by (forward_using lemma_crossimpliesopposite).

assert (RE a b c d) by (conclude lemma_squarerectangle).

assert (CR a c b d) by (conclude_def RE ).

assert (nCol a c d) by (forward_using lemma_parallelNC).

assert (TS a b d c) by (forward_using lemma_crossimpliesopposite).

assert (EF B A D C b a d c) by (conclude axiom_paste3).

assert (EF B A D C a b c d) by (forward_using axiom_EFpermutation).

assert (EF a b c d B A D C) by (conclude axiom_EFsymmetric).

assert (EF a b c d A B C D) by (forward_using axiom_EFpermutation).

assert (EF A B C D a b c d) by (conclude axiom_EFsymmetric).

close.

Qed.

End Euclid.