Library GeoCoq.Elements.OriginalProofs.proposition_48A
Require Export GeoCoq.Elements.OriginalProofs.lemma_squarerectangle.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_48A :
∀ 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.
intros.
assert (PG A B C D) by (conclude lemma_squareparallelogram).
assert (PG a b c d) by (conclude lemma_squareparallelogram).
assert (Cong_3 B A D D C B) by (conclude proposition_34).
assert (Cong_3 b a d d c b) by (conclude proposition_34).
assert (ET B A D D C B) by (conclude axiom_congruentequal).
assert (ET b a d d c b) by (conclude axiom_congruentequal).
assert (ET B A D B D C) by (forward_using axiom_ETpermutation).
assert (ET B D C B A D) by (conclude axiom_ETsymmetric).
assert (ET B D C A B D) by (forward_using axiom_ETpermutation).
assert (ET A B D B D C) by (conclude axiom_ETsymmetric).
assert (ET b a d b d c) by (forward_using axiom_ETpermutation).
assert (ET b d c b a d) by (conclude axiom_ETsymmetric).
assert (ET b d c a b d) by (forward_using axiom_ETpermutation).
assert (ET a b d b d c) by (conclude axiom_ETsymmetric).
assert (RE A B C D) by (conclude lemma_squarerectangle).
assert (RE a b c d) by (conclude lemma_squarerectangle).
assert (CR A C B D) by (conclude_def RE ).
assert (CR a c b d) by (conclude_def RE ).
assert (Par A B C D) by (conclude_def PG ).
assert (nCol A B D) by (forward_using lemma_parallelNC).
assert (Par a b c d) by (conclude_def PG ).
assert (nCol a b d) by (forward_using lemma_parallelNC).
assert (nCol d a b) by (forward_using lemma_NCorder).
assert (Triangle d a b) by (conclude_def Triangle ).
assert (nCol D A B) by (forward_using lemma_NCorder).
assert (Triangle D A B) by (conclude_def Triangle ).
assert (nCol A C D) by (forward_using lemma_parallelNC).
assert (nCol A D C) by (forward_using lemma_NCorder).
assert (TS A B D C) by (forward_using lemma_crossimpliesopposite).
assert (nCol a c d) by (forward_using lemma_parallelNC).
assert (nCol a d c) by (forward_using lemma_NCorder).
assert (TS a b d c) by (forward_using lemma_crossimpliesopposite).
assert (ET A B D a b d) by (conclude axiom_halvesofequals).
assert (Cong a b d a) by (conclude_def SQ ).
assert (Cong A B D A) by (conclude_def SQ ).
assert (Cong a b a d) by (forward_using lemma_congruenceflip).
assert (Cong A B A D) by (forward_using lemma_congruenceflip).
assert (¬ Lt a b A B).
{
intro.
let Tf:=fresh in
assert (Tf:∃ E, (BetS A E B ∧ Cong A E a b)) by (conclude_def Lt );destruct Tf as [E];spliter.
assert (Lt a d A B) by (conclude lemma_lessthancongruence2).
assert (Lt a d A D) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ F, (BetS A F D ∧ Cong A F a d)) by (conclude_def Lt );destruct Tf as [F];spliter.
assert (Per D A B) by (conclude_def SQ ).
assert (Per d a b) by (conclude_def SQ ).
assert (neq A D) by (forward_using lemma_betweennotequal).
assert (neq A B) by (forward_using lemma_betweennotequal).
assert (Out A D F) by (conclude lemma_ray4).
assert (Out A B E) by (conclude lemma_ray4).
assert (nCol D A B) by (forward_using lemma_NCorder).
assert (CongA D A B D A B) by (conclude lemma_equalanglesreflexive).
assert (CongA D A B F A E) by (conclude lemma_equalangleshelper).
assert (CongA F A E D A B) by (conclude lemma_equalanglessymmetric).
assert (Per F A E) by (conclude lemma_equaltorightisright).
assert (CongA F A E d a b) by (conclude lemma_Euclid4).
assert (Col A F D) by (conclude_def Col ).
assert (Col A E B) by (conclude_def Col ).
assert (Col A B E) by (forward_using lemma_collinearorder).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (nCol A B D) by (forward_using lemma_NCorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A B A) by (conclude_def Col ).
assert (nCol A E D) by (conclude lemma_NChelper).
assert (nCol A D E) by (forward_using lemma_NCorder).
assert (Col A D F) by (forward_using lemma_collinearorder).
assert (neq A F) by (forward_using lemma_betweennotequal).
assert (Col A D A) by (conclude_def Col ).
assert (nCol A F E) by (conclude lemma_NChelper).
assert (nCol F A E) by (forward_using lemma_NCorder).
assert (Triangle F A E) by (conclude_def Triangle ).
assert (Cong F E d b) by (conclude proposition_04).
assert (Cong F A d a) by (forward_using lemma_congruenceflip).
assert (Cong_3 F A E d a b) by (conclude_def Cong_3 ).
assert (ET F A E d a b) by (conclude axiom_congruentequal).
assert (ET F A E a b d) by (forward_using axiom_ETpermutation).
assert (ET a b d A B D) by (conclude axiom_ETsymmetric).
assert (ET F A E A B D) by (conclude axiom_ETtransitive).
assert (ET F A E D A B) by (forward_using axiom_ETpermutation).
assert (ET D A B F A E) by (conclude axiom_ETsymmetric).
assert (Triangle D A B) by (conclude_def Triangle ).
assert (¬ ET D A B F A E) by (conclude axiom_deZolt2).
contradict.
}
assert (¬ Lt A B a b).
{
intro.
let Tf:=fresh in
assert (Tf:∃ e, (BetS a e b ∧ Cong a e A B)) by (conclude_def Lt );destruct Tf as [e];spliter.
assert (Lt A D a b) by (conclude lemma_lessthancongruence2).
assert (Lt A D a d) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ f, (BetS a f d ∧ Cong a f A D)) by (conclude_def Lt );destruct Tf as [f];spliter.
assert (Per d a b) by (conclude_def SQ ).
assert (Per D A B) by (conclude_def SQ ).
assert (neq a d) by (forward_using lemma_betweennotequal).
assert (neq a b) by (forward_using lemma_betweennotequal).
assert (Out a d f) by (conclude lemma_ray4).
assert (Out a b e) by (conclude lemma_ray4).
assert (nCol d a b) by (forward_using lemma_NCorder).
assert (CongA d a b d a b) by (conclude lemma_equalanglesreflexive).
assert (CongA d a b f a e) by (conclude lemma_equalangleshelper).
assert (CongA f a e d a b) by (conclude lemma_equalanglessymmetric).
assert (Per f a e) by (conclude lemma_equaltorightisright).
assert (CongA f a e D A B) by (conclude lemma_Euclid4).
assert (Col a f d) by (conclude_def Col ).
assert (Col a e b) by (conclude_def Col ).
assert (Col a b e) by (forward_using lemma_collinearorder).
assert (neq a e) by (forward_using lemma_betweennotequal).
assert (nCol a b d) by (forward_using lemma_NCorder).
assert (eq a a) by (conclude cn_equalityreflexive).
assert (Col a b a) by (conclude_def Col ).
assert (nCol a e d) by (conclude lemma_NChelper).
assert (nCol a d e) by (forward_using lemma_NCorder).
assert (Col a d f) by (forward_using lemma_collinearorder).
assert (neq a f) by (forward_using lemma_betweennotequal).
assert (Col a d a) by (conclude_def Col ).
assert (nCol a f e) by (conclude lemma_NChelper).
assert (nCol f a e) by (forward_using lemma_NCorder).
assert (Triangle f a e) by (conclude_def Triangle ).
assert (Cong f e D B) by (conclude proposition_04).
assert (Cong f a D A) by (forward_using lemma_congruenceflip).
assert (Cong_3 f a e D A B) by (conclude_def Cong_3 ).
assert (ET f a e D A B) by (conclude axiom_congruentequal).
assert (ET f a e A B D) by (forward_using axiom_ETpermutation).
assert (ET A B D f a e) by (conclude axiom_ETsymmetric).
assert (ET f a e a b d) by (conclude axiom_ETtransitive).
assert (ET f a e d a b) by (forward_using axiom_ETpermutation).
assert (ET d a b f a e) by (conclude axiom_ETsymmetric).
assert (Triangle d a b) by (conclude_def Triangle ).
assert (¬ ET d a b f a e) by (conclude axiom_deZolt2).
contradict.
}
assert (neq A B) by (forward_using lemma_NCdistinct).
assert (neq a b) by (forward_using lemma_NCdistinct).
assert (Cong A B a b) by (conclude lemma_trichotomy1).
close.
Qed.
End Euclid.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_48A :
∀ 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.
intros.
assert (PG A B C D) by (conclude lemma_squareparallelogram).
assert (PG a b c d) by (conclude lemma_squareparallelogram).
assert (Cong_3 B A D D C B) by (conclude proposition_34).
assert (Cong_3 b a d d c b) by (conclude proposition_34).
assert (ET B A D D C B) by (conclude axiom_congruentequal).
assert (ET b a d d c b) by (conclude axiom_congruentequal).
assert (ET B A D B D C) by (forward_using axiom_ETpermutation).
assert (ET B D C B A D) by (conclude axiom_ETsymmetric).
assert (ET B D C A B D) by (forward_using axiom_ETpermutation).
assert (ET A B D B D C) by (conclude axiom_ETsymmetric).
assert (ET b a d b d c) by (forward_using axiom_ETpermutation).
assert (ET b d c b a d) by (conclude axiom_ETsymmetric).
assert (ET b d c a b d) by (forward_using axiom_ETpermutation).
assert (ET a b d b d c) by (conclude axiom_ETsymmetric).
assert (RE A B C D) by (conclude lemma_squarerectangle).
assert (RE a b c d) by (conclude lemma_squarerectangle).
assert (CR A C B D) by (conclude_def RE ).
assert (CR a c b d) by (conclude_def RE ).
assert (Par A B C D) by (conclude_def PG ).
assert (nCol A B D) by (forward_using lemma_parallelNC).
assert (Par a b c d) by (conclude_def PG ).
assert (nCol a b d) by (forward_using lemma_parallelNC).
assert (nCol d a b) by (forward_using lemma_NCorder).
assert (Triangle d a b) by (conclude_def Triangle ).
assert (nCol D A B) by (forward_using lemma_NCorder).
assert (Triangle D A B) by (conclude_def Triangle ).
assert (nCol A C D) by (forward_using lemma_parallelNC).
assert (nCol A D C) by (forward_using lemma_NCorder).
assert (TS A B D C) by (forward_using lemma_crossimpliesopposite).
assert (nCol a c d) by (forward_using lemma_parallelNC).
assert (nCol a d c) by (forward_using lemma_NCorder).
assert (TS a b d c) by (forward_using lemma_crossimpliesopposite).
assert (ET A B D a b d) by (conclude axiom_halvesofequals).
assert (Cong a b d a) by (conclude_def SQ ).
assert (Cong A B D A) by (conclude_def SQ ).
assert (Cong a b a d) by (forward_using lemma_congruenceflip).
assert (Cong A B A D) by (forward_using lemma_congruenceflip).
assert (¬ Lt a b A B).
{
intro.
let Tf:=fresh in
assert (Tf:∃ E, (BetS A E B ∧ Cong A E a b)) by (conclude_def Lt );destruct Tf as [E];spliter.
assert (Lt a d A B) by (conclude lemma_lessthancongruence2).
assert (Lt a d A D) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ F, (BetS A F D ∧ Cong A F a d)) by (conclude_def Lt );destruct Tf as [F];spliter.
assert (Per D A B) by (conclude_def SQ ).
assert (Per d a b) by (conclude_def SQ ).
assert (neq A D) by (forward_using lemma_betweennotequal).
assert (neq A B) by (forward_using lemma_betweennotequal).
assert (Out A D F) by (conclude lemma_ray4).
assert (Out A B E) by (conclude lemma_ray4).
assert (nCol D A B) by (forward_using lemma_NCorder).
assert (CongA D A B D A B) by (conclude lemma_equalanglesreflexive).
assert (CongA D A B F A E) by (conclude lemma_equalangleshelper).
assert (CongA F A E D A B) by (conclude lemma_equalanglessymmetric).
assert (Per F A E) by (conclude lemma_equaltorightisright).
assert (CongA F A E d a b) by (conclude lemma_Euclid4).
assert (Col A F D) by (conclude_def Col ).
assert (Col A E B) by (conclude_def Col ).
assert (Col A B E) by (forward_using lemma_collinearorder).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (nCol A B D) by (forward_using lemma_NCorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A B A) by (conclude_def Col ).
assert (nCol A E D) by (conclude lemma_NChelper).
assert (nCol A D E) by (forward_using lemma_NCorder).
assert (Col A D F) by (forward_using lemma_collinearorder).
assert (neq A F) by (forward_using lemma_betweennotequal).
assert (Col A D A) by (conclude_def Col ).
assert (nCol A F E) by (conclude lemma_NChelper).
assert (nCol F A E) by (forward_using lemma_NCorder).
assert (Triangle F A E) by (conclude_def Triangle ).
assert (Cong F E d b) by (conclude proposition_04).
assert (Cong F A d a) by (forward_using lemma_congruenceflip).
assert (Cong_3 F A E d a b) by (conclude_def Cong_3 ).
assert (ET F A E d a b) by (conclude axiom_congruentequal).
assert (ET F A E a b d) by (forward_using axiom_ETpermutation).
assert (ET a b d A B D) by (conclude axiom_ETsymmetric).
assert (ET F A E A B D) by (conclude axiom_ETtransitive).
assert (ET F A E D A B) by (forward_using axiom_ETpermutation).
assert (ET D A B F A E) by (conclude axiom_ETsymmetric).
assert (Triangle D A B) by (conclude_def Triangle ).
assert (¬ ET D A B F A E) by (conclude axiom_deZolt2).
contradict.
}
assert (¬ Lt A B a b).
{
intro.
let Tf:=fresh in
assert (Tf:∃ e, (BetS a e b ∧ Cong a e A B)) by (conclude_def Lt );destruct Tf as [e];spliter.
assert (Lt A D a b) by (conclude lemma_lessthancongruence2).
assert (Lt A D a d) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ f, (BetS a f d ∧ Cong a f A D)) by (conclude_def Lt );destruct Tf as [f];spliter.
assert (Per d a b) by (conclude_def SQ ).
assert (Per D A B) by (conclude_def SQ ).
assert (neq a d) by (forward_using lemma_betweennotequal).
assert (neq a b) by (forward_using lemma_betweennotequal).
assert (Out a d f) by (conclude lemma_ray4).
assert (Out a b e) by (conclude lemma_ray4).
assert (nCol d a b) by (forward_using lemma_NCorder).
assert (CongA d a b d a b) by (conclude lemma_equalanglesreflexive).
assert (CongA d a b f a e) by (conclude lemma_equalangleshelper).
assert (CongA f a e d a b) by (conclude lemma_equalanglessymmetric).
assert (Per f a e) by (conclude lemma_equaltorightisright).
assert (CongA f a e D A B) by (conclude lemma_Euclid4).
assert (Col a f d) by (conclude_def Col ).
assert (Col a e b) by (conclude_def Col ).
assert (Col a b e) by (forward_using lemma_collinearorder).
assert (neq a e) by (forward_using lemma_betweennotequal).
assert (nCol a b d) by (forward_using lemma_NCorder).
assert (eq a a) by (conclude cn_equalityreflexive).
assert (Col a b a) by (conclude_def Col ).
assert (nCol a e d) by (conclude lemma_NChelper).
assert (nCol a d e) by (forward_using lemma_NCorder).
assert (Col a d f) by (forward_using lemma_collinearorder).
assert (neq a f) by (forward_using lemma_betweennotequal).
assert (Col a d a) by (conclude_def Col ).
assert (nCol a f e) by (conclude lemma_NChelper).
assert (nCol f a e) by (forward_using lemma_NCorder).
assert (Triangle f a e) by (conclude_def Triangle ).
assert (Cong f e D B) by (conclude proposition_04).
assert (Cong f a D A) by (forward_using lemma_congruenceflip).
assert (Cong_3 f a e D A B) by (conclude_def Cong_3 ).
assert (ET f a e D A B) by (conclude axiom_congruentequal).
assert (ET f a e A B D) by (forward_using axiom_ETpermutation).
assert (ET A B D f a e) by (conclude axiom_ETsymmetric).
assert (ET f a e a b d) by (conclude axiom_ETtransitive).
assert (ET f a e d a b) by (forward_using axiom_ETpermutation).
assert (ET d a b f a e) by (conclude axiom_ETsymmetric).
assert (Triangle d a b) by (conclude_def Triangle ).
assert (¬ ET d a b f a e) by (conclude axiom_deZolt2).
contradict.
}
assert (neq A B) by (forward_using lemma_NCdistinct).
assert (neq a b) by (forward_using lemma_NCdistinct).
assert (Cong A B a b) by (conclude lemma_trichotomy1).
close.
Qed.
End Euclid.