Require Export GeoCoq.Elements.OriginalProofs.lemma_squarerectangle.

Section Euclid.

Context `{Ax1:area}.


Lemma lemma_squaresequal : 
   forall 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.
(* Goal: forall (A B C D a b c d : @Point Ax0) (_ : @Cong Ax0 A B a b) (_ : @SQ Ax0 A B C D) (_ : @SQ Ax0 a b c d), @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
intros.
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Per D A B) by (conclude_def SQ ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Per d a b) by (conclude_def SQ ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (CongA D A B d a b) by (conclude lemma_Euclid4).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong A B D A) by (conclude_def SQ ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong a b d a) by (conclude_def SQ ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong D A A B) by (conclude lemma_congruencesymmetric).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong D A a b) by (conclude lemma_congruencetransitive).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong D A d a) by (conclude lemma_congruencetransitive).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (PG A B C D) by (conclude lemma_squareparallelogram).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (PG a b c d) by (conclude lemma_squareparallelogram).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Par A B C D) by (conclude_def PG ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Par a b c d) by (conclude_def PG ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (nCol A B D) by (forward_using lemma_parallelNC).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (nCol a b d) by (forward_using lemma_parallelNC).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong A D a d) by (forward_using lemma_congruenceflip).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong D B d b) by (conclude proposition_04).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong B D b d) by (forward_using lemma_congruenceflip).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Triangle A B D) by (conclude_def Triangle ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong_3 A B D a b d) by (conclude_def Cong_3 ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (ET A B D a b d) by (conclude axiom_congruentequal).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (ET A B D b d a) by (forward_using axiom_ETpermutation).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (ET b d a A B D) by (conclude axiom_ETsymmetric).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (ET b d a B D A) by (forward_using axiom_ETpermutation).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (ET B D A b d a) by (conclude axiom_ETsymmetric).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong A B B C) by (conclude_def SQ ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong a b b c) by (conclude_def SQ ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong A B C D) by (conclude_def SQ ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong a b c d) by (conclude_def SQ ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong B C A B) by (conclude lemma_congruencesymmetric).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong B C a b) by (conclude lemma_congruencetransitive).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong B C b c) by (conclude lemma_congruencetransitive).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong C D A B) by (conclude lemma_congruencesymmetric).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong C D a b) by (conclude lemma_congruencetransitive).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong C D c d) by (conclude lemma_congruencetransitive).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (nCol B C D) by (forward_using lemma_parallelNC).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Triangle B C D) by (conclude_def Triangle ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (Cong_3 B C D b c d) by (conclude_def Cong_3 ).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (ET B C D b c d) by (conclude axiom_congruentequal).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (ET B C D b d c) by (forward_using axiom_ETpermutation).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (ET b d c B C D) by (conclude axiom_ETsymmetric).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (ET b d c B D C) by (forward_using axiom_ETpermutation).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (ET B D C b d c) by (conclude axiom_ETsymmetric).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (RE A B C D) by (conclude lemma_squarerectangle).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (CR A C B D) by (conclude_def RE ).
let Tf:=fresh in
assert (Tf:exists M, (BetS A M C /\ BetS B M D)) by (conclude_def CR );destruct Tf as [M];spliter.
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (RE a b c d) by (conclude lemma_squarerectangle).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (CR a c b d) by (conclude_def RE ).
let Tf:=fresh in
assert (Tf:exists m, (BetS a m c /\ BetS b m d)) by (conclude_def CR );destruct Tf as [m];spliter.
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (EF B A D C b a d c) by (conclude axiom_paste3).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (EF B A D C a b c d) by (forward_using axiom_EFpermutation).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (EF a b c d B A D C) by (conclude axiom_EFsymmetric).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (EF a b c d A B C D) by (forward_using axiom_EFpermutation).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
assert (EF A B C D a b c d) by (conclude axiom_EFsymmetric).
(* Goal: @EF Ax0 Ax2 Ax Ax1 A B C D a b c d *)
close.
Qed.

End Euclid.


