Require Export GeoCoq.Elements.OriginalProofs.lemma_squarerectangle.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_48A : 
   forall A B C D a b c d, 
   SQ A B C D -> SQ a b c d -> EF A B C D a b c d ->
   Cong A B a b.
Proof.
(* Goal: forall (A B C D a b c d : @Point Ax0) (_ : @SQ Ax0 A B C D) (_ : @SQ Ax0 a b c d) (_ : @EF Ax0 Ax1 Ax2 Ax A B C D a b c d), @Cong Ax0 A B a b *)
intros.
(* Goal: @Cong Ax0 A B a b *)
assert (PG A B C D) by (conclude lemma_squareparallelogram).
(* Goal: @Cong Ax0 A B a b *)
assert (PG a b c d) by (conclude lemma_squareparallelogram).
(* Goal: @Cong Ax0 A B a b *)
assert (Cong_3 B A D D C B) by (conclude proposition_34).
(* Goal: @Cong Ax0 A B a b *)
assert (Cong_3 b a d d c b) by (conclude proposition_34).
(* Goal: @Cong Ax0 A B a b *)
assert (ET B A D D C B) by (conclude axiom_congruentequal).
(* Goal: @Cong Ax0 A B a b *)
assert (ET b a d d c b) by (conclude axiom_congruentequal).
(* Goal: @Cong Ax0 A B a b *)
assert (ET B A D B D C) by (forward_using axiom_ETpermutation).
(* Goal: @Cong Ax0 A B a b *)
assert (ET B D C B A D) by (conclude axiom_ETsymmetric).
(* Goal: @Cong Ax0 A B a b *)
assert (ET B D C A B D) by (forward_using axiom_ETpermutation).
(* Goal: @Cong Ax0 A B a b *)
assert (ET A B D B D C) by (conclude axiom_ETsymmetric).
(* Goal: @Cong Ax0 A B a b *)
assert (ET b a d b d c) by (forward_using axiom_ETpermutation).
(* Goal: @Cong Ax0 A B a b *)
assert (ET b d c b a d) by (conclude axiom_ETsymmetric).
(* Goal: @Cong Ax0 A B a b *)
assert (ET b d c a b d) by (forward_using axiom_ETpermutation).
(* Goal: @Cong Ax0 A B a b *)
assert (ET a b d b d c) by (conclude axiom_ETsymmetric).
(* Goal: @Cong Ax0 A B a b *)
assert (RE A B C D) by (conclude lemma_squarerectangle).
(* Goal: @Cong Ax0 A B a b *)
assert (RE a b c d) by (conclude lemma_squarerectangle).
(* Goal: @Cong Ax0 A B a b *)
assert (CR A C B D) by (conclude_def RE ).
(* Goal: @Cong Ax0 A B a b *)
assert (CR a c b d) by (conclude_def RE ).
(* Goal: @Cong Ax0 A B a b *)
assert (Par A B C D) by (conclude_def PG ).
(* Goal: @Cong Ax0 A B a b *)
assert (nCol A B D) by (forward_using lemma_parallelNC).
(* Goal: @Cong Ax0 A B a b *)
assert (Par a b c d) by (conclude_def PG ).
(* Goal: @Cong Ax0 A B a b *)
assert (nCol a b d) by (forward_using lemma_parallelNC).
(* Goal: @Cong Ax0 A B a b *)
assert (TS A B D C) by (forward_using lemma_crossimpliesopposite).
(* Goal: @Cong Ax0 A B a b *)
assert (TS a b d c) by (forward_using lemma_crossimpliesopposite).
(* Goal: @Cong Ax0 A B a b *)
assert (ET A B D a b d) by (conclude axiom_halvesofequals).
(* Goal: @Cong Ax0 A B a b *)
assert (Cong a b d a) by (conclude_def SQ ).
(* Goal: @Cong Ax0 A B a b *)
assert (Cong A B D A) by (conclude_def SQ ).
(* Goal: @Cong Ax0 A B a b *)
assert (Cong a b a d) by (forward_using lemma_congruenceflip).
(* Goal: @Cong Ax0 A B a b *)
assert (Cong A B A D) by (forward_using lemma_congruenceflip).
(* Goal: @Cong Ax0 A B a b *)
assert (~ Lt a b A B).
(* Goal: not (@Lt Ax0 A B a b) *)
(* Goal: @Cong Ax0 A B a b *)
 {
(* Goal: not (@Lt Ax0 A B a b) *)
 intro.
 let Tf:=fresh in
 assert (Tf:exists E, (BetS A E B /\ Cong A E a b)) by (conclude_def Lt );destruct Tf as [E];spliter.
(* Goal: False *)
 assert (Lt a d A B) by (conclude lemma_lessthancongruence2).
(* Goal: False *)
 assert (Lt a d A D) by (conclude lemma_lessthancongruence).
 let Tf:=fresh in
 assert (Tf:exists F, (BetS A F D /\ Cong A F a d)) by (conclude_def Lt );destruct Tf as [F];spliter.
(* Goal: False *)
 assert (Per D A B) by (conclude_def SQ ).
(* Goal: False *)
 assert (Per d a b) by (conclude_def SQ ).
(* Goal: False *)
 assert (neq A D) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq A B) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Out A D F) by (conclude lemma_ray4).
(* Goal: False *)
 assert (Out A B E) by (conclude lemma_ray4).
(* Goal: False *)
 assert (nCol D A B) by (forward_using lemma_NCorder).
(* Goal: False *)
 assert (CongA D A B D A B) by (conclude lemma_equalanglesreflexive).
(* Goal: False *)
 assert (CongA D A B F A E) by (conclude lemma_equalangleshelper).
(* Goal: False *)
 assert (CongA F A E D A B) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (Per F A E) by (conclude lemma_equaltorightisright).
(* Goal: False *)
 assert (CongA F A E d a b) by (conclude lemma_Euclid4).
(* Goal: False *)
 assert (Cong F E d b) by (conclude proposition_04).
(* Goal: False *)
 assert (Cong F A d a) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Cong_3 F A E d a b) by (conclude_def Cong_3 ).
(* Goal: False *)
 assert (ET F A E d a b) by (conclude axiom_congruentequal).
(* Goal: False *)
 assert (ET F A E a b d) by (forward_using axiom_ETpermutation).
(* Goal: False *)
 assert (ET a b d A B D) by (conclude axiom_ETsymmetric).
(* Goal: False *)
 assert (ET F A E A B D) by (conclude axiom_ETtransitive).
(* Goal: False *)
 assert (ET F A E D A B) by (forward_using axiom_ETpermutation).
(* Goal: False *)
 assert (ET D A B F A E) by (conclude axiom_ETsymmetric).
(* Goal: False *)
 assert (Triangle D A B) by (conclude_def Triangle ).
(* Goal: False *)
 assert (~ ET D A B F A E) by (conclude axiom_deZolt2).
(* Goal: False *)
 contradict.
 }
(* Goal: @Cong Ax0 A B a b *)
assert (~ Lt A B a b).
(* Goal: not (@Lt Ax0 A B a b) *)
(* Goal: @Cong Ax0 A B a b *)
 {
(* Goal: not (@Lt Ax0 A B a b) *)
 intro.
 let Tf:=fresh in
 assert (Tf:exists e, (BetS a e b /\ Cong a e A B)) by (conclude_def Lt );destruct Tf as [e];spliter.
(* Goal: False *)
 assert (Lt A D a b) by (conclude lemma_lessthancongruence2).
(* Goal: False *)
 assert (Lt A D a d) by (conclude lemma_lessthancongruence).
 let Tf:=fresh in
 assert (Tf:exists f, (BetS a f d /\ Cong a f A D)) by (conclude_def Lt );destruct Tf as [f];spliter.
(* Goal: False *)
 assert (Per d a b) by (conclude_def SQ ).
(* Goal: False *)
 assert (Per D A B) by (conclude_def SQ ).
(* Goal: False *)
 assert (neq a d) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq a b) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Out a d f) by (conclude lemma_ray4).
(* Goal: False *)
 assert (Out a b e) by (conclude lemma_ray4).
(* Goal: False *)
 assert (nCol d a b) by (forward_using lemma_NCorder).
(* Goal: False *)
 assert (CongA d a b d a b) by (conclude lemma_equalanglesreflexive).
(* Goal: False *)
 assert (CongA d a b f a e) by (conclude lemma_equalangleshelper).
(* Goal: False *)
 assert (CongA f a e d a b) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (Per f a e) by (conclude lemma_equaltorightisright).
(* Goal: False *)
 assert (CongA f a e D A B) by (conclude lemma_Euclid4).
(* Goal: False *)
 assert (Cong f e D B) by (conclude proposition_04).
(* Goal: False *)
 assert (Cong f a D A) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Cong_3 f a e D A B) by (conclude_def Cong_3 ).
(* Goal: False *)
 assert (ET f a e D A B) by (conclude axiom_congruentequal).
(* Goal: False *)
 assert (ET f a e A B D) by (forward_using axiom_ETpermutation).
(* Goal: False *)
 assert (ET A B D f a e) by (conclude axiom_ETsymmetric).
(* Goal: False *)
 assert (ET f a e a b d) by (conclude axiom_ETtransitive).
(* Goal: False *)
 assert (ET f a e d a b) by (forward_using axiom_ETpermutation).
(* Goal: False *)
 assert (ET d a b f a e) by (conclude axiom_ETsymmetric).
(* Goal: False *)
 assert (Triangle d a b) by (conclude_def Triangle ).
(* Goal: False *)
 assert (~ ET d a b f a e) by (conclude axiom_deZolt2).
(* Goal: False *)
 contradict.
 }
(* Goal: @Cong Ax0 A B a b *)
assert (neq A B) by (forward_using lemma_NCdistinct).
(* Goal: @Cong Ax0 A B a b *)
assert (neq a b) by (forward_using lemma_NCdistinct).
(* Goal: @Cong Ax0 A B a b *)
assert (Cong A B a b) by (conclude lemma_trichotomy1).
(* Goal: @Cong Ax0 A B a b *)
close.
Qed.

End Euclid.

