Library GeoCoq.Elements.OriginalProofs.proposition_47B
Require Export GeoCoq.Elements.OriginalProofs.proposition_47A.
Require Export GeoCoq.Elements.OriginalProofs.lemma_angleaddition.
Require Export GeoCoq.Elements.OriginalProofs.proposition_41.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_47B :
∀ A B C D E F G H K,
Triangle A B C → Per B A C → SQ A B F G → TS G B A C → SQ A C K H → TS H C A B → SQ B C E D → TS D C B A →
∃ X Y, PG B X Y D ∧ BetS B X C ∧ PG X C E Y ∧ BetS D Y E ∧ BetS Y X A ∧ Per D Y A ∧ EF A B F G B X Y D.
Proof.
intros.
let Tf:=fresh in
assert (Tf:∃ M L, (PG B M L D ∧ BetS B M C ∧ PG M C E L ∧ BetS D L E ∧ BetS L M A ∧ Per D L A)) by (conclude proposition_47A);destruct Tf as [M[L]];spliter.
assert (PG B C E D) by (conclude lemma_squareparallelogram).
let Tf:=fresh in
assert (Tf:∃ N, (BetS D N A ∧ Col C B N ∧ nCol C B D)) by (conclude_def TS );destruct Tf as [N];spliter.
assert (Per G A B) by (conclude_def SQ ).
assert (BetS G A C) by (conclude lemma_righttogether).
assert (BetS C A G) by (conclude axiom_betweennesssymmetry).
assert (Per H A C) by (conclude_def SQ ).
assert (Per C A B) by (conclude lemma_8_2).
assert (BetS H A B) by (conclude lemma_righttogether).
assert (BetS B A H) by (conclude axiom_betweennesssymmetry).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (neq A B) by (forward_using lemma_betweennotequal).
assert (Out A B B) by (conclude lemma_ray4).
assert (nCol A B C) by (conclude_def Triangle ).
assert (neq B C) by (forward_using lemma_NCdistinct).
assert (Cong B C E D) by (conclude_def SQ ).
assert (neq E D) by (conclude lemma_nullsegment3).
assert (neq D E) by (conclude lemma_inequalitysymmetric).
assert (Per A B F) by (conclude_def SQ ).
assert (Per F B A) by (conclude lemma_8_2).
assert (Per D B C) by (conclude_def SQ ).
assert (CongA D B C F B A) by (conclude lemma_Euclid4).
assert (nCol A B C) by (conclude_def Triangle ).
assert (CongA A B C C B A) by (conclude lemma_ABCequalsCBA).
assert (PG A B F G) by (conclude lemma_squareparallelogram).
assert (Par A B F G) by (conclude_def PG ).
assert (Par A B G F) by (forward_using lemma_parallelflip).
assert (TP A B G F) by (conclude lemma_paralleldef2B).
assert (OS G F A B) by (conclude_def TP ).
assert (OS F G A B) by (forward_using lemma_samesidesymmetric).
assert (TS G A B C) by (conclude lemma_oppositesideflip).
assert (TS F A B C) by (conclude lemma_planeseparation).
let Tf:=fresh in
assert (Tf:∃ a, (BetS F a C ∧ Col A B a ∧ nCol A B F)) by (conclude_def TS );destruct Tf as [a];spliter.
assert (Col B A a) by (forward_using lemma_collinearorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (Par A G B F) by (conclude_def PG ).
assert (Col A G A) by (conclude_def Col ).
assert (Col B F F) by (conclude_def Col ).
assert (Par A G F B) by (forward_using lemma_parallelflip).
assert (Col G A C) by (conclude_def Col ).
assert (Col A G C) by (forward_using lemma_collinearorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A G A) by (conclude_def Col ).
assert (neq G C) by (forward_using lemma_betweennotequal).
assert (neq C G) by (conclude lemma_inequalitysymmetric).
assert (Par F B A G) by (conclude lemma_parallelsymmetric).
assert (Par F B C G) by (conclude lemma_collinearparallel).
assert (Par F B G C) by (forward_using lemma_parallelflip).
assert (¬ Meet F B G C) by (conclude_def Par ).
assert (neq A C) by (forward_using lemma_NCdistinct).
assert (nCol A B F) by (forward_using lemma_parallelNC).
assert (neq F A) by (forward_using lemma_NCdistinct).
assert (neq F B) by (forward_using lemma_NCdistinct).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col F B B) by (conclude_def Col ).
assert (BetS B a A) by (conclude lemma_collinearbetween).
assert (neq B a) by (forward_using lemma_betweennotequal).
assert (Out B a A) by (conclude lemma_ray4).
assert (neq B F) by (conclude lemma_inequalitysymmetric).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (Out B F F) by (conclude lemma_ray4).
assert (nCol A B F) by (forward_using lemma_parallelNC).
assert (nCol F B A) by (forward_using lemma_NCorder).
assert (CongA F B A F B A) by (conclude lemma_equalanglesreflexive).
assert (Out B A a) by (conclude lemma_ray5).
assert (CongA F B A F B a) by (conclude lemma_equalangleshelper).
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 (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).
assert (CongA A B C a B C) by (conclude lemma_equalangleshelper).
assert (SumA F B A A B C F B C) by (conclude_def SumA ).
let Tf:=fresh in
assert (Tf:∃ c, (BetS D c A ∧ Col C B c ∧ nCol C B D)) by (conclude_def TS );destruct Tf as [c];spliter.
assert (Col B C c) by (forward_using lemma_collinearorder).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (PG B C E D) by (conclude lemma_squareparallelogram).
assert (Par B D C E) by (conclude_def PG ).
assert (Par C E B D) by (conclude lemma_parallelsymmetric).
assert (Col C D C) by (conclude_def Col ).
assert (Par C E D B) by (forward_using lemma_parallelflip).
assert (Col B C c) by (forward_using lemma_collinearorder).
assert (Col B M C) by (conclude_def Col ).
assert (Col C B M) by (forward_using lemma_collinearorder).
assert (Col C B c) by (forward_using lemma_collinearorder).
assert (neq C B) by (forward_using lemma_NCdistinct).
assert (Col B M c) by (conclude lemma_collinear4).
assert (Par B D M L) by (conclude_def PG ).
assert (Col L M A) by (conclude_def Col ).
assert (Col M L A) by (forward_using lemma_collinearorder).
assert (neq L A) by (forward_using lemma_betweennotequal).
assert (neq A L) by (conclude lemma_inequalitysymmetric).
assert (Par B D A L) by (conclude lemma_collinearparallel).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Par D B L A) by (forward_using lemma_parallelflip).
assert (¬ Meet D B L A) by (conclude_def Par ).
assert (nCol D M L) by (forward_using lemma_parallelNC).
assert (neq M D) by (forward_using lemma_NCdistinct).
assert (nCol B D L) by (forward_using lemma_parallelNC).
assert (neq D B) by (forward_using lemma_NCdistinct).
assert (neq M A) by (forward_using lemma_betweennotequal).
assert (neq L M) by (forward_using lemma_betweennotequal).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (Col D B B) by (conclude_def Col ).
assert (BetS B c M) by (conclude lemma_collinearbetween).
assert (BetS B c C) by (conclude lemma_3_6b).
assert (nCol D B A) by (forward_using lemma_parallelNC).
assert (¬ eq B c).
{
intro.
assert (Col D B c) by (conclude_def Col ).
assert (Col D c A) by (conclude_def Col ).
assert (Col c D B) by (forward_using lemma_collinearorder).
assert (Col c D A) by (forward_using lemma_collinearorder).
assert (neq D c) by (forward_using lemma_betweennotequal).
assert (neq c D) by (conclude lemma_inequalitysymmetric).
assert (Col D B A) by (conclude lemma_collinear4).
contradict.
}
assert (Out B c C) by (conclude lemma_ray4).
assert (Out B C c) by (conclude lemma_ray5).
assert (nCol C B A) by (forward_using lemma_NCorder).
assert (CongA C B A C B A) by (conclude lemma_equalanglesreflexive).
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 (CongA C B A c B A) by (conclude lemma_equalangleshelper).
assert (nCol C D B) by (forward_using lemma_parallelNC).
assert (nCol D B C) by (forward_using lemma_NCorder).
assert (CongA D B C D B C) by (conclude lemma_equalanglesreflexive).
assert (neq B D) by (conclude lemma_inequalitysymmetric).
assert (Out B D D) by (conclude lemma_ray4).
assert (CongA D B C D B c) by (conclude lemma_equalangleshelper).
assert (SumA D B C C B A D B A) by (conclude_def SumA ).
assert (CongA F B A D B C) by (conclude lemma_Euclid4).
assert (CongA A B C C B A) by (conclude lemma_ABCequalsCBA).
assert (CongA F B C D B A) by (conclude lemma_angleaddition).
assert (CongA D B A F B C) by (conclude lemma_equalanglessymmetric).
assert (¬ Col C B F).
{
intro.
assert (Col F B C) by (forward_using lemma_collinearorder).
assert (Per C B A) by (conclude lemma_collinearright).
assert (¬ Per C B A) by (conclude lemma_8_7).
contradict.
}
assert (nCol F B C) by (assert (nCol C B F) by auto;forward_using lemma_NCorder).
assert (CongA F B C C B F) by (conclude lemma_ABCequalsCBA).
assert (CongA D B A C B F) by (conclude lemma_equalanglestransitive).
assert (Cong A B B F) by (conclude_def SQ ).
assert (Cong A B F B) by (forward_using lemma_congruenceflip).
assert (Cong F B A B) by (conclude lemma_congruencesymmetric).
assert (Cong B F B A) by (forward_using lemma_congruenceflip).
assert (Cong B A B F) by (conclude lemma_congruencesymmetric).
assert (Cong B C D B) by (conclude_def SQ ).
assert (Cong D B B C) by (conclude lemma_congruencesymmetric).
assert (Cong B D B C) by (forward_using lemma_congruenceflip).
assert (Triangle D B A) by (conclude_def Triangle ).
assert (Triangle C B F) by (conclude_def Triangle ).
assert ((Cong D A C F ∧ CongA B D A B C F ∧ CongA B A D B F C)) by (conclude proposition_04).
assert (Cong A D F C) by (forward_using lemma_congruenceflip).
assert (Cong_3 A B D F B C) by (conclude_def Cong_3 ).
assert (ET A B D F B C) by (conclude axiom_congruentequal).
assert (Par B M L D) by (conclude_def PG ).
assert (Par B D M L) by (conclude_def PG ).
assert (Par M L B D) by (conclude lemma_parallelsymmetric).
assert (Par M B D L) by (forward_using lemma_parallelflip).
assert (PG M B D L) by (conclude_def PG ).
assert (Col M L A) by (forward_using lemma_collinearorder).
assert (ET M B D A B D) by (conclude proposition_41).
assert (PG A B F G) by (conclude lemma_squareparallelogram).
assert (PG B A G F) by (conclude lemma_PGflip).
assert (Col G A C) by (conclude_def Col ).
assert (Col A G C) by (forward_using lemma_collinearorder).
assert (ET A B F C B F) by (conclude proposition_41).
assert (ET A B F F B C) by (forward_using axiom_ETpermutation).
assert (ET F B C A B D) by (conclude axiom_ETsymmetric).
assert (ET A B F A B D) by (conclude axiom_ETtransitive).
assert (ET A B D M B D) by (conclude axiom_ETsymmetric).
assert (ET A B F M B D) by (conclude axiom_ETtransitive).
assert (Cong_3 A B F F G A) by (conclude proposition_34).
assert (ET A B F F G A) by (conclude axiom_congruentequal).
assert (PG B M L D) by (conclude lemma_PGflip).
assert (Cong_3 M B D D L M) by (conclude proposition_34).
assert (ET M B D D L M) by (conclude axiom_congruentequal).
assert (ET F G A A B F) by (conclude axiom_ETsymmetric).
assert (ET F G A A B D) by (conclude axiom_ETtransitive).
assert (ET F G A M B D) by (conclude axiom_ETtransitive).
assert (ET F G A D L M) by (conclude axiom_ETtransitive).
assert (ET F G A D M L) by (forward_using axiom_ETpermutation).
assert (ET D M L F G A) by (conclude axiom_ETsymmetric).
assert (ET D M L F A G) by (forward_using axiom_ETpermutation).
assert (ET F A G D M L) by (conclude axiom_ETsymmetric).
assert (ET A B F D M B) by (forward_using axiom_ETpermutation).
assert (ET D M B A B F) by (conclude axiom_ETsymmetric).
assert (ET D M B F A B) by (forward_using axiom_ETpermutation).
assert (ET F A B D M B) by (conclude axiom_ETsymmetric).
let Tf:=fresh in
assert (Tf:∃ m, (Midpoint A m F ∧ Midpoint B m G)) by (conclude lemma_diagonalsbisect);destruct Tf as [m];spliter.
assert (BetS A m F) by (conclude_def Midpoint ).
assert (BetS B m G) by (conclude_def Midpoint ).
assert (Col A m F) by (conclude_def Col ).
assert (Col F A m) by (forward_using lemma_collinearorder).
assert (nCol A B F) by (forward_using lemma_parallelNC).
assert (nCol F A B) by (forward_using lemma_NCorder).
assert (TS B F A G) by (conclude_def TS ).
let Tf:=fresh in
assert (Tf:∃ n, (Midpoint B n L ∧ Midpoint M n D)) by (conclude lemma_diagonalsbisect);destruct Tf as [n];spliter.
assert (BetS B n L) by (conclude_def Midpoint ).
assert (BetS M n D) by (conclude_def Midpoint ).
assert (Col M n D) by (conclude_def Col ).
assert (Col D M n) by (forward_using lemma_collinearorder).
assert (nCol B M D) by (forward_using lemma_parallelNC).
assert (nCol D M B) by (forward_using lemma_NCorder).
assert (TS B D M L) by (conclude_def TS ).
assert (EF F B A G D B M L) by (conclude axiom_paste3).
assert (EF F B A G B M L D) by (forward_using axiom_EFpermutation).
assert (EF B M L D F B A G) by (conclude axiom_EFsymmetric).
assert (EF B M L D A B F G) by (forward_using axiom_EFpermutation).
assert (EF A B F G B M L D) by (conclude axiom_EFsymmetric).
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.lemma_angleaddition.
Require Export GeoCoq.Elements.OriginalProofs.proposition_41.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_47B :
∀ A B C D E F G H K,
Triangle A B C → Per B A C → SQ A B F G → TS G B A C → SQ A C K H → TS H C A B → SQ B C E D → TS D C B A →
∃ X Y, PG B X Y D ∧ BetS B X C ∧ PG X C E Y ∧ BetS D Y E ∧ BetS Y X A ∧ Per D Y A ∧ EF A B F G B X Y D.
Proof.
intros.
let Tf:=fresh in
assert (Tf:∃ M L, (PG B M L D ∧ BetS B M C ∧ PG M C E L ∧ BetS D L E ∧ BetS L M A ∧ Per D L A)) by (conclude proposition_47A);destruct Tf as [M[L]];spliter.
assert (PG B C E D) by (conclude lemma_squareparallelogram).
let Tf:=fresh in
assert (Tf:∃ N, (BetS D N A ∧ Col C B N ∧ nCol C B D)) by (conclude_def TS );destruct Tf as [N];spliter.
assert (Per G A B) by (conclude_def SQ ).
assert (BetS G A C) by (conclude lemma_righttogether).
assert (BetS C A G) by (conclude axiom_betweennesssymmetry).
assert (Per H A C) by (conclude_def SQ ).
assert (Per C A B) by (conclude lemma_8_2).
assert (BetS H A B) by (conclude lemma_righttogether).
assert (BetS B A H) by (conclude axiom_betweennesssymmetry).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (neq A B) by (forward_using lemma_betweennotequal).
assert (Out A B B) by (conclude lemma_ray4).
assert (nCol A B C) by (conclude_def Triangle ).
assert (neq B C) by (forward_using lemma_NCdistinct).
assert (Cong B C E D) by (conclude_def SQ ).
assert (neq E D) by (conclude lemma_nullsegment3).
assert (neq D E) by (conclude lemma_inequalitysymmetric).
assert (Per A B F) by (conclude_def SQ ).
assert (Per F B A) by (conclude lemma_8_2).
assert (Per D B C) by (conclude_def SQ ).
assert (CongA D B C F B A) by (conclude lemma_Euclid4).
assert (nCol A B C) by (conclude_def Triangle ).
assert (CongA A B C C B A) by (conclude lemma_ABCequalsCBA).
assert (PG A B F G) by (conclude lemma_squareparallelogram).
assert (Par A B F G) by (conclude_def PG ).
assert (Par A B G F) by (forward_using lemma_parallelflip).
assert (TP A B G F) by (conclude lemma_paralleldef2B).
assert (OS G F A B) by (conclude_def TP ).
assert (OS F G A B) by (forward_using lemma_samesidesymmetric).
assert (TS G A B C) by (conclude lemma_oppositesideflip).
assert (TS F A B C) by (conclude lemma_planeseparation).
let Tf:=fresh in
assert (Tf:∃ a, (BetS F a C ∧ Col A B a ∧ nCol A B F)) by (conclude_def TS );destruct Tf as [a];spliter.
assert (Col B A a) by (forward_using lemma_collinearorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (Par A G B F) by (conclude_def PG ).
assert (Col A G A) by (conclude_def Col ).
assert (Col B F F) by (conclude_def Col ).
assert (Par A G F B) by (forward_using lemma_parallelflip).
assert (Col G A C) by (conclude_def Col ).
assert (Col A G C) by (forward_using lemma_collinearorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A G A) by (conclude_def Col ).
assert (neq G C) by (forward_using lemma_betweennotequal).
assert (neq C G) by (conclude lemma_inequalitysymmetric).
assert (Par F B A G) by (conclude lemma_parallelsymmetric).
assert (Par F B C G) by (conclude lemma_collinearparallel).
assert (Par F B G C) by (forward_using lemma_parallelflip).
assert (¬ Meet F B G C) by (conclude_def Par ).
assert (neq A C) by (forward_using lemma_NCdistinct).
assert (nCol A B F) by (forward_using lemma_parallelNC).
assert (neq F A) by (forward_using lemma_NCdistinct).
assert (neq F B) by (forward_using lemma_NCdistinct).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col F B B) by (conclude_def Col ).
assert (BetS B a A) by (conclude lemma_collinearbetween).
assert (neq B a) by (forward_using lemma_betweennotequal).
assert (Out B a A) by (conclude lemma_ray4).
assert (neq B F) by (conclude lemma_inequalitysymmetric).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (Out B F F) by (conclude lemma_ray4).
assert (nCol A B F) by (forward_using lemma_parallelNC).
assert (nCol F B A) by (forward_using lemma_NCorder).
assert (CongA F B A F B A) by (conclude lemma_equalanglesreflexive).
assert (Out B A a) by (conclude lemma_ray5).
assert (CongA F B A F B a) by (conclude lemma_equalangleshelper).
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 (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).
assert (CongA A B C a B C) by (conclude lemma_equalangleshelper).
assert (SumA F B A A B C F B C) by (conclude_def SumA ).
let Tf:=fresh in
assert (Tf:∃ c, (BetS D c A ∧ Col C B c ∧ nCol C B D)) by (conclude_def TS );destruct Tf as [c];spliter.
assert (Col B C c) by (forward_using lemma_collinearorder).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (PG B C E D) by (conclude lemma_squareparallelogram).
assert (Par B D C E) by (conclude_def PG ).
assert (Par C E B D) by (conclude lemma_parallelsymmetric).
assert (Col C D C) by (conclude_def Col ).
assert (Par C E D B) by (forward_using lemma_parallelflip).
assert (Col B C c) by (forward_using lemma_collinearorder).
assert (Col B M C) by (conclude_def Col ).
assert (Col C B M) by (forward_using lemma_collinearorder).
assert (Col C B c) by (forward_using lemma_collinearorder).
assert (neq C B) by (forward_using lemma_NCdistinct).
assert (Col B M c) by (conclude lemma_collinear4).
assert (Par B D M L) by (conclude_def PG ).
assert (Col L M A) by (conclude_def Col ).
assert (Col M L A) by (forward_using lemma_collinearorder).
assert (neq L A) by (forward_using lemma_betweennotequal).
assert (neq A L) by (conclude lemma_inequalitysymmetric).
assert (Par B D A L) by (conclude lemma_collinearparallel).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Par D B L A) by (forward_using lemma_parallelflip).
assert (¬ Meet D B L A) by (conclude_def Par ).
assert (nCol D M L) by (forward_using lemma_parallelNC).
assert (neq M D) by (forward_using lemma_NCdistinct).
assert (nCol B D L) by (forward_using lemma_parallelNC).
assert (neq D B) by (forward_using lemma_NCdistinct).
assert (neq M A) by (forward_using lemma_betweennotequal).
assert (neq L M) by (forward_using lemma_betweennotequal).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (Col D B B) by (conclude_def Col ).
assert (BetS B c M) by (conclude lemma_collinearbetween).
assert (BetS B c C) by (conclude lemma_3_6b).
assert (nCol D B A) by (forward_using lemma_parallelNC).
assert (¬ eq B c).
{
intro.
assert (Col D B c) by (conclude_def Col ).
assert (Col D c A) by (conclude_def Col ).
assert (Col c D B) by (forward_using lemma_collinearorder).
assert (Col c D A) by (forward_using lemma_collinearorder).
assert (neq D c) by (forward_using lemma_betweennotequal).
assert (neq c D) by (conclude lemma_inequalitysymmetric).
assert (Col D B A) by (conclude lemma_collinear4).
contradict.
}
assert (Out B c C) by (conclude lemma_ray4).
assert (Out B C c) by (conclude lemma_ray5).
assert (nCol C B A) by (forward_using lemma_NCorder).
assert (CongA C B A C B A) by (conclude lemma_equalanglesreflexive).
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 (CongA C B A c B A) by (conclude lemma_equalangleshelper).
assert (nCol C D B) by (forward_using lemma_parallelNC).
assert (nCol D B C) by (forward_using lemma_NCorder).
assert (CongA D B C D B C) by (conclude lemma_equalanglesreflexive).
assert (neq B D) by (conclude lemma_inequalitysymmetric).
assert (Out B D D) by (conclude lemma_ray4).
assert (CongA D B C D B c) by (conclude lemma_equalangleshelper).
assert (SumA D B C C B A D B A) by (conclude_def SumA ).
assert (CongA F B A D B C) by (conclude lemma_Euclid4).
assert (CongA A B C C B A) by (conclude lemma_ABCequalsCBA).
assert (CongA F B C D B A) by (conclude lemma_angleaddition).
assert (CongA D B A F B C) by (conclude lemma_equalanglessymmetric).
assert (¬ Col C B F).
{
intro.
assert (Col F B C) by (forward_using lemma_collinearorder).
assert (Per C B A) by (conclude lemma_collinearright).
assert (¬ Per C B A) by (conclude lemma_8_7).
contradict.
}
assert (nCol F B C) by (assert (nCol C B F) by auto;forward_using lemma_NCorder).
assert (CongA F B C C B F) by (conclude lemma_ABCequalsCBA).
assert (CongA D B A C B F) by (conclude lemma_equalanglestransitive).
assert (Cong A B B F) by (conclude_def SQ ).
assert (Cong A B F B) by (forward_using lemma_congruenceflip).
assert (Cong F B A B) by (conclude lemma_congruencesymmetric).
assert (Cong B F B A) by (forward_using lemma_congruenceflip).
assert (Cong B A B F) by (conclude lemma_congruencesymmetric).
assert (Cong B C D B) by (conclude_def SQ ).
assert (Cong D B B C) by (conclude lemma_congruencesymmetric).
assert (Cong B D B C) by (forward_using lemma_congruenceflip).
assert (Triangle D B A) by (conclude_def Triangle ).
assert (Triangle C B F) by (conclude_def Triangle ).
assert ((Cong D A C F ∧ CongA B D A B C F ∧ CongA B A D B F C)) by (conclude proposition_04).
assert (Cong A D F C) by (forward_using lemma_congruenceflip).
assert (Cong_3 A B D F B C) by (conclude_def Cong_3 ).
assert (ET A B D F B C) by (conclude axiom_congruentequal).
assert (Par B M L D) by (conclude_def PG ).
assert (Par B D M L) by (conclude_def PG ).
assert (Par M L B D) by (conclude lemma_parallelsymmetric).
assert (Par M B D L) by (forward_using lemma_parallelflip).
assert (PG M B D L) by (conclude_def PG ).
assert (Col M L A) by (forward_using lemma_collinearorder).
assert (ET M B D A B D) by (conclude proposition_41).
assert (PG A B F G) by (conclude lemma_squareparallelogram).
assert (PG B A G F) by (conclude lemma_PGflip).
assert (Col G A C) by (conclude_def Col ).
assert (Col A G C) by (forward_using lemma_collinearorder).
assert (ET A B F C B F) by (conclude proposition_41).
assert (ET A B F F B C) by (forward_using axiom_ETpermutation).
assert (ET F B C A B D) by (conclude axiom_ETsymmetric).
assert (ET A B F A B D) by (conclude axiom_ETtransitive).
assert (ET A B D M B D) by (conclude axiom_ETsymmetric).
assert (ET A B F M B D) by (conclude axiom_ETtransitive).
assert (Cong_3 A B F F G A) by (conclude proposition_34).
assert (ET A B F F G A) by (conclude axiom_congruentequal).
assert (PG B M L D) by (conclude lemma_PGflip).
assert (Cong_3 M B D D L M) by (conclude proposition_34).
assert (ET M B D D L M) by (conclude axiom_congruentequal).
assert (ET F G A A B F) by (conclude axiom_ETsymmetric).
assert (ET F G A A B D) by (conclude axiom_ETtransitive).
assert (ET F G A M B D) by (conclude axiom_ETtransitive).
assert (ET F G A D L M) by (conclude axiom_ETtransitive).
assert (ET F G A D M L) by (forward_using axiom_ETpermutation).
assert (ET D M L F G A) by (conclude axiom_ETsymmetric).
assert (ET D M L F A G) by (forward_using axiom_ETpermutation).
assert (ET F A G D M L) by (conclude axiom_ETsymmetric).
assert (ET A B F D M B) by (forward_using axiom_ETpermutation).
assert (ET D M B A B F) by (conclude axiom_ETsymmetric).
assert (ET D M B F A B) by (forward_using axiom_ETpermutation).
assert (ET F A B D M B) by (conclude axiom_ETsymmetric).
let Tf:=fresh in
assert (Tf:∃ m, (Midpoint A m F ∧ Midpoint B m G)) by (conclude lemma_diagonalsbisect);destruct Tf as [m];spliter.
assert (BetS A m F) by (conclude_def Midpoint ).
assert (BetS B m G) by (conclude_def Midpoint ).
assert (Col A m F) by (conclude_def Col ).
assert (Col F A m) by (forward_using lemma_collinearorder).
assert (nCol A B F) by (forward_using lemma_parallelNC).
assert (nCol F A B) by (forward_using lemma_NCorder).
assert (TS B F A G) by (conclude_def TS ).
let Tf:=fresh in
assert (Tf:∃ n, (Midpoint B n L ∧ Midpoint M n D)) by (conclude lemma_diagonalsbisect);destruct Tf as [n];spliter.
assert (BetS B n L) by (conclude_def Midpoint ).
assert (BetS M n D) by (conclude_def Midpoint ).
assert (Col M n D) by (conclude_def Col ).
assert (Col D M n) by (forward_using lemma_collinearorder).
assert (nCol B M D) by (forward_using lemma_parallelNC).
assert (nCol D M B) by (forward_using lemma_NCorder).
assert (TS B D M L) by (conclude_def TS ).
assert (EF F B A G D B M L) by (conclude axiom_paste3).
assert (EF F B A G B M L D) by (forward_using axiom_EFpermutation).
assert (EF B M L D F B A G) by (conclude axiom_EFsymmetric).
assert (EF B M L D A B F G) by (forward_using axiom_EFpermutation).
assert (EF A B F G B M L D) by (conclude axiom_EFsymmetric).
close.
Qed.
End Euclid.