Library GeoCoq.Elements.OriginalProofs.proposition_47A
Require Export GeoCoq.Elements.OriginalProofs.lemma_squareparallelogram.
Require Export GeoCoq.Elements.OriginalProofs.lemma_samesideflip.
Require Export GeoCoq.Elements.OriginalProofs.lemma_erectedperpendicularunique.
Require Export GeoCoq.Elements.OriginalProofs.lemma_twoperpsparallel.
Require Export GeoCoq.Elements.OriginalProofs.proposition_29C.
Require Export GeoCoq.Elements.OriginalProofs.lemma_altitudeofrighttriangle.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_47A :
∀ A B C D E,
Triangle A B C → Per B A C → 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.
Proof.
intros.
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 C A B) by (conclude lemma_8_2).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (nCol C A B) by (conclude lemma_rightangleNC).
assert (neq A B) by (forward_using lemma_NCdistinct).
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).
let Tf:=fresh in
assert (Tf:∃ q, (BetS D q A ∧ Col C B q ∧ nCol C B D)) by (conclude_def TS );destruct Tf as [q];spliter.
assert (PG B C E D) by (conclude lemma_squareparallelogram).
assert (Par B C E D) by (conclude_def PG ).
assert (Par B C D E) by (forward_using lemma_parallelflip).
assert (¬ Meet B C E D) by (conclude_def Par ).
assert (¬ eq A E).
{
intro.
assert (BetS D q E) by (conclude cn_equalitysub).
assert (Col D q E) by (conclude_def Col ).
assert (Col E D q) by (forward_using lemma_collinearorder).
assert (Col B C q) by (forward_using lemma_collinearorder).
assert (Meet B C E D) by (conclude_def Meet ).
contradict.
}
assert (¬ Col D E A).
{
intro.
assert (Col D A E) by (forward_using lemma_collinearorder).
assert (Col D q A) by (conclude_def Col ).
assert (Col D A q) by (forward_using lemma_collinearorder).
assert (neq D A) by (forward_using lemma_betweennotequal).
assert (Col A E q) by (conclude lemma_collinear4).
assert (Col q A E) by (forward_using lemma_collinearorder).
assert (Col q A D) by (forward_using lemma_collinearorder).
assert (neq q A) by (forward_using lemma_betweennotequal).
assert (Col A E D) by (conclude lemma_collinear4).
assert (Col A E q) by (forward_using lemma_collinearorder).
assert (Col E D q) by (conclude lemma_collinear4).
assert (Col D E q) by (forward_using lemma_collinearorder).
assert (Col B C q) by (forward_using lemma_collinearorder).
assert (Meet B C E D) by (conclude_def Meet ).
contradict.
}
let Tf:=fresh in
assert (Tf:∃ L, Perp_at A L D E L) by (conclude proposition_12);destruct Tf as [L];spliter.
let Tf:=fresh in
assert (Tf:∃ p, (Col A L L ∧ Col D E L ∧ Col D E p ∧ Per p L A)) by (conclude_def Perp_at );destruct Tf as [p];spliter.
assert (Per A L p) by (conclude lemma_8_2).
assert (neq L p) by (conclude_def Per ).
assert (Col E D L) by (forward_using lemma_collinearorder).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (Col E D D) by (conclude_def Col ).
assert (neq A D) by (assert (nCol D E A) by auto;forward_using lemma_NCdistinct).
assert (nCol A B C) by (conclude_def Triangle ).
assert (neq B A) by (forward_using lemma_NCdistinct).
assert (¬ eq B N).
{
intro.
assert (BetS D B A) by (conclude cn_equalitysub).
assert (Col D B A) by (conclude_def Col ).
assert (Col B D A) by (forward_using lemma_collinearorder).
assert (Per D B C) by (conclude_def SQ ).
assert (Per A B C) by (conclude lemma_collinearright).
assert (¬ Per C A B) by (conclude lemma_8_7).
assert (Per C A B) by (conclude lemma_8_2).
contradict.
}
assert (Par B C E D) by (conclude_def PG ).
assert (Par B C D E) by (forward_using lemma_parallelflip).
assert (Par D E B C) by (conclude lemma_parallelsymmetric).
assert (Par D E C B) by (forward_using lemma_parallelflip).
assert (neq N B) by (conclude lemma_inequalitysymmetric).
assert (Par D E N B) by (conclude lemma_collinearparallel).
assert (Par D E B N) by (forward_using lemma_parallelflip).
assert (TP D E B N) by (conclude lemma_paralleldef2B).
assert (OS B N D E) by (conclude_def TP ).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (Col D D E) by (conclude_def Col ).
assert (neq D N) by (forward_using lemma_betweennotequal).
assert (Out D N A) by (conclude lemma_ray4).
assert (OS B A D E) by (conclude lemma_sameside2).
assert (OS B A E D) by (conclude lemma_samesideflip).
assert (OS A B E D) by (forward_using lemma_samesidesymmetric).
assert (¬ eq D L).
{
intro.
assert (Per A D p) by (conclude cn_equalitysub).
assert (Per E D B) by (conclude_def SQ ).
assert (Per p D A) by (conclude lemma_8_2).
assert (Col p D E) by (forward_using lemma_collinearorder).
assert (Per E D A) by (conclude lemma_collinearright).
assert (Per E D B) by (conclude_def SQ ).
assert (Out D A B) by (conclude lemma_erectedperpendicularunique).
assert (Col D A B) by (conclude lemma_rayimpliescollinear).
assert (Col A D B) by (forward_using lemma_collinearorder).
assert (Col D N A) by (conclude_def Col ).
assert (Col A D N) by (forward_using lemma_collinearorder).
assert (neq D A) by (forward_using lemma_betweennotequal).
assert (neq A D) by (conclude lemma_inequalitysymmetric).
assert (Col D B N) by (conclude lemma_collinear4).
assert (Col N B C) by (forward_using lemma_collinearorder).
assert (Col N B D) by (forward_using lemma_collinearorder).
assert (Col B C D) by (conclude lemma_collinear4).
assert (Per D B C) by (conclude_def SQ ).
assert (nCol D B C) by (conclude lemma_rightangleNC).
assert (nCol B C D) by (forward_using lemma_NCorder).
contradict.
}
assert (neq L D) by (conclude lemma_inequalitysymmetric).
assert (Par B C E D) by (forward_using lemma_parallelflip).
assert (Col E D L) by (forward_using lemma_collinearorder).
assert (Par B C L D) by (conclude lemma_collinearparallel).
assert (Par L D B C) by (conclude lemma_parallelsymmetric).
assert (TP B C L D) by (conclude lemma_paralleldef2B).
assert (OS L D B C) by (conclude_def TP ).
assert (OS D L B C) by (forward_using lemma_samesidesymmetric).
assert (nCol B C D) by (forward_using lemma_parallelNC).
assert (Col B C N) by (forward_using lemma_collinearorder).
assert (TS D B C A) by (conclude_def TS ).
assert (TS L B C A) by (conclude lemma_planeseparation).
let Tf:=fresh in
assert (Tf:∃ M, (BetS L M A ∧ Col B C M ∧ nCol B C L)) by (conclude_def TS );destruct Tf as [M];spliter.
assert (Par L D C B) by (forward_using lemma_parallelflip).
assert (Col C B M) by (forward_using lemma_collinearorder).
assert (nCol B D E) by (forward_using lemma_parallelNC).
assert (neq D E) by (forward_using lemma_NCdistinct).
assert (neq E D) by (conclude lemma_inequalitysymmetric).
assert (neq L M) by (forward_using lemma_betweennotequal).
assert (Out L M A) by (conclude lemma_ray4).
assert (Out L A M) by (conclude lemma_ray5).
assert (Per E D B) by (conclude_def SQ ).
assert (Col E D p) by (forward_using lemma_collinearorder).
assert (Col E D L) by (forward_using lemma_collinearorder).
assert (Col D p L) by (conclude lemma_collinear4).
assert (nCol p L A) by (conclude lemma_rightangleNC).
assert (neq p L) by (forward_using lemma_NCdistinct).
assert (Col p L D) by (forward_using lemma_collinearorder).
assert (neq L p) by (conclude lemma_inequalitysymmetric).
assert (Per D L A) by (conclude lemma_collinearright).
assert (Per D L M) by (conclude lemma_8_3).
assert (¬ eq B M).
{
intro.
assert (Per D L B) by (conclude cn_equalitysub).
assert (Per L D B) by (conclude lemma_collinearright).
assert (Per B D L) by (conclude lemma_8_2).
assert (¬ Per B D L) by (conclude lemma_8_7).
contradict.
}
assert (neq M B) by (conclude lemma_inequalitysymmetric).
assert (Par L D C B) by (forward_using lemma_parallelflip).
assert (Col C B M) by (forward_using lemma_collinearorder).
assert (Par L D M B) by (conclude lemma_collinearparallel).
assert (Par L D B M) by (forward_using lemma_parallelflip).
assert (Par B M L D) by (conclude lemma_parallelsymmetric).
assert (Par B M D L) by (forward_using lemma_parallelflip).
assert (Par D L B M) by (conclude lemma_parallelsymmetric).
assert (TP D L B M) by (conclude lemma_paralleldef2B).
assert (OS B M D L) by (conclude_def TP ).
assert (Par B M L D) by (conclude lemma_parallelsymmetric).
assert (Per L D B) by (conclude lemma_collinearright).
assert (Per B D L) by (conclude lemma_8_2).
assert (Par B D L M) by (conclude lemma_twoperpsparallel).
assert (Par B D M L) by (forward_using lemma_parallelflip).
assert (PG B M L D) by (conclude_def PG ).
assert (Par M L B D) by (conclude lemma_parallelsymmetric).
assert (TP M L B D) by (conclude lemma_paralleldef2B).
assert (OS B D M L) by (conclude_def TP ).
assert (BetS A M L) by (conclude axiom_betweennesssymmetry).
assert (Par M B L D) by (forward_using lemma_parallelflip).
assert (CongA A M B M L D) by (conclude proposition_29C).
assert (Per M L D) by (conclude lemma_8_2).
assert (Per A M B) by (conclude lemma_equaltorightisright).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col B C B) by (conclude_def Col ).
assert (BetS B M C) by (conclude lemma_altitudeofrighttriangle).
assert (¬ eq M C).
{
intro.
assert (Per A C B) by (conclude cn_equalitysub).
assert (¬ Per B A C) by (conclude lemma_8_7).
contradict.
}
assert (¬ eq L E).
{
intro.
assert (Par B D C E) by (conclude_def PG ).
assert (Par C E B D) by (conclude lemma_parallelsymmetric).
assert (Par M E B D) by (conclude cn_equalitysub).
assert (Par B D M E) by (conclude lemma_parallelsymmetric).
assert (Par B D C E) by (conclude lemma_parallelsymmetric).
assert (Par B D E C) by (forward_using lemma_parallelflip).
assert (Par B D E M) by (forward_using lemma_parallelflip).
assert (Col E C M) by (conclude lemma_Playfair).
assert (Col M C E) by (forward_using lemma_collinearorder).
assert (Col M C B) by (forward_using lemma_collinearorder).
assert (Col C E B) by (conclude lemma_collinear4).
assert (Col B C E) by (forward_using lemma_collinearorder).
assert (nCol B C E) by (forward_using lemma_parallelNC).
contradict.
}
assert (Par B M L D) by (conclude_def PG ).
assert (Par B M D L) by (forward_using lemma_parallelflip).
assert (Col D L E) by (forward_using lemma_collinearorder).
assert (neq E L) by (conclude lemma_inequalitysymmetric).
assert (Par B M E L) by (conclude lemma_collinearparallel).
assert (Par E L B M) by (conclude lemma_parallelsymmetric).
assert (Col B M C) by (forward_using lemma_collinearorder).
assert (neq C M) by (conclude lemma_inequalitysymmetric).
assert (Par E L C M) by (conclude lemma_collinearparallel).
assert (Par C M E L) by (conclude lemma_parallelsymmetric).
assert (Par M C E L) by (forward_using lemma_parallelflip).
assert (Col D L E) by (forward_using lemma_collinearorder).
assert (neq M L) by (forward_using lemma_betweennotequal).
assert (Per E L M) by (conclude lemma_collinearright).
assert (Per M L E) by (conclude lemma_8_2).
assert (Per C E D) by (conclude_def SQ ).
assert (Per D E C) by (conclude lemma_8_2).
assert (Per L E C) by (conclude lemma_collinearright).
assert (Par M C L E) by (forward_using lemma_parallelflip).
assert (Par L E M C) by (conclude lemma_parallelsymmetric).
assert (TP L E M C) by (conclude lemma_paralleldef2B).
assert (OS M C L E) by (conclude_def TP ).
assert (Par M L E C) by (conclude lemma_twoperpsparallel).
assert (Par M L C E) by (forward_using lemma_parallelflip).
assert (PG M C E L) by (conclude_def PG ).
assert (Cong B M D L) by (forward_using proposition_34).
assert (Cong M C L E) by (forward_using proposition_34).
assert (Cong B C D E) by (forward_using proposition_34).
assert (BetS D L E) by (conclude lemma_betweennesspreserved).
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.lemma_samesideflip.
Require Export GeoCoq.Elements.OriginalProofs.lemma_erectedperpendicularunique.
Require Export GeoCoq.Elements.OriginalProofs.lemma_twoperpsparallel.
Require Export GeoCoq.Elements.OriginalProofs.proposition_29C.
Require Export GeoCoq.Elements.OriginalProofs.lemma_altitudeofrighttriangle.
Section Euclid.
Context `{Ax:area}.
Lemma proposition_47A :
∀ A B C D E,
Triangle A B C → Per B A C → 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.
Proof.
intros.
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 C A B) by (conclude lemma_8_2).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (nCol C A B) by (conclude lemma_rightangleNC).
assert (neq A B) by (forward_using lemma_NCdistinct).
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).
let Tf:=fresh in
assert (Tf:∃ q, (BetS D q A ∧ Col C B q ∧ nCol C B D)) by (conclude_def TS );destruct Tf as [q];spliter.
assert (PG B C E D) by (conclude lemma_squareparallelogram).
assert (Par B C E D) by (conclude_def PG ).
assert (Par B C D E) by (forward_using lemma_parallelflip).
assert (¬ Meet B C E D) by (conclude_def Par ).
assert (¬ eq A E).
{
intro.
assert (BetS D q E) by (conclude cn_equalitysub).
assert (Col D q E) by (conclude_def Col ).
assert (Col E D q) by (forward_using lemma_collinearorder).
assert (Col B C q) by (forward_using lemma_collinearorder).
assert (Meet B C E D) by (conclude_def Meet ).
contradict.
}
assert (¬ Col D E A).
{
intro.
assert (Col D A E) by (forward_using lemma_collinearorder).
assert (Col D q A) by (conclude_def Col ).
assert (Col D A q) by (forward_using lemma_collinearorder).
assert (neq D A) by (forward_using lemma_betweennotequal).
assert (Col A E q) by (conclude lemma_collinear4).
assert (Col q A E) by (forward_using lemma_collinearorder).
assert (Col q A D) by (forward_using lemma_collinearorder).
assert (neq q A) by (forward_using lemma_betweennotequal).
assert (Col A E D) by (conclude lemma_collinear4).
assert (Col A E q) by (forward_using lemma_collinearorder).
assert (Col E D q) by (conclude lemma_collinear4).
assert (Col D E q) by (forward_using lemma_collinearorder).
assert (Col B C q) by (forward_using lemma_collinearorder).
assert (Meet B C E D) by (conclude_def Meet ).
contradict.
}
let Tf:=fresh in
assert (Tf:∃ L, Perp_at A L D E L) by (conclude proposition_12);destruct Tf as [L];spliter.
let Tf:=fresh in
assert (Tf:∃ p, (Col A L L ∧ Col D E L ∧ Col D E p ∧ Per p L A)) by (conclude_def Perp_at );destruct Tf as [p];spliter.
assert (Per A L p) by (conclude lemma_8_2).
assert (neq L p) by (conclude_def Per ).
assert (Col E D L) by (forward_using lemma_collinearorder).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (Col E D D) by (conclude_def Col ).
assert (neq A D) by (assert (nCol D E A) by auto;forward_using lemma_NCdistinct).
assert (nCol A B C) by (conclude_def Triangle ).
assert (neq B A) by (forward_using lemma_NCdistinct).
assert (¬ eq B N).
{
intro.
assert (BetS D B A) by (conclude cn_equalitysub).
assert (Col D B A) by (conclude_def Col ).
assert (Col B D A) by (forward_using lemma_collinearorder).
assert (Per D B C) by (conclude_def SQ ).
assert (Per A B C) by (conclude lemma_collinearright).
assert (¬ Per C A B) by (conclude lemma_8_7).
assert (Per C A B) by (conclude lemma_8_2).
contradict.
}
assert (Par B C E D) by (conclude_def PG ).
assert (Par B C D E) by (forward_using lemma_parallelflip).
assert (Par D E B C) by (conclude lemma_parallelsymmetric).
assert (Par D E C B) by (forward_using lemma_parallelflip).
assert (neq N B) by (conclude lemma_inequalitysymmetric).
assert (Par D E N B) by (conclude lemma_collinearparallel).
assert (Par D E B N) by (forward_using lemma_parallelflip).
assert (TP D E B N) by (conclude lemma_paralleldef2B).
assert (OS B N D E) by (conclude_def TP ).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (Col D D E) by (conclude_def Col ).
assert (neq D N) by (forward_using lemma_betweennotequal).
assert (Out D N A) by (conclude lemma_ray4).
assert (OS B A D E) by (conclude lemma_sameside2).
assert (OS B A E D) by (conclude lemma_samesideflip).
assert (OS A B E D) by (forward_using lemma_samesidesymmetric).
assert (¬ eq D L).
{
intro.
assert (Per A D p) by (conclude cn_equalitysub).
assert (Per E D B) by (conclude_def SQ ).
assert (Per p D A) by (conclude lemma_8_2).
assert (Col p D E) by (forward_using lemma_collinearorder).
assert (Per E D A) by (conclude lemma_collinearright).
assert (Per E D B) by (conclude_def SQ ).
assert (Out D A B) by (conclude lemma_erectedperpendicularunique).
assert (Col D A B) by (conclude lemma_rayimpliescollinear).
assert (Col A D B) by (forward_using lemma_collinearorder).
assert (Col D N A) by (conclude_def Col ).
assert (Col A D N) by (forward_using lemma_collinearorder).
assert (neq D A) by (forward_using lemma_betweennotequal).
assert (neq A D) by (conclude lemma_inequalitysymmetric).
assert (Col D B N) by (conclude lemma_collinear4).
assert (Col N B C) by (forward_using lemma_collinearorder).
assert (Col N B D) by (forward_using lemma_collinearorder).
assert (Col B C D) by (conclude lemma_collinear4).
assert (Per D B C) by (conclude_def SQ ).
assert (nCol D B C) by (conclude lemma_rightangleNC).
assert (nCol B C D) by (forward_using lemma_NCorder).
contradict.
}
assert (neq L D) by (conclude lemma_inequalitysymmetric).
assert (Par B C E D) by (forward_using lemma_parallelflip).
assert (Col E D L) by (forward_using lemma_collinearorder).
assert (Par B C L D) by (conclude lemma_collinearparallel).
assert (Par L D B C) by (conclude lemma_parallelsymmetric).
assert (TP B C L D) by (conclude lemma_paralleldef2B).
assert (OS L D B C) by (conclude_def TP ).
assert (OS D L B C) by (forward_using lemma_samesidesymmetric).
assert (nCol B C D) by (forward_using lemma_parallelNC).
assert (Col B C N) by (forward_using lemma_collinearorder).
assert (TS D B C A) by (conclude_def TS ).
assert (TS L B C A) by (conclude lemma_planeseparation).
let Tf:=fresh in
assert (Tf:∃ M, (BetS L M A ∧ Col B C M ∧ nCol B C L)) by (conclude_def TS );destruct Tf as [M];spliter.
assert (Par L D C B) by (forward_using lemma_parallelflip).
assert (Col C B M) by (forward_using lemma_collinearorder).
assert (nCol B D E) by (forward_using lemma_parallelNC).
assert (neq D E) by (forward_using lemma_NCdistinct).
assert (neq E D) by (conclude lemma_inequalitysymmetric).
assert (neq L M) by (forward_using lemma_betweennotequal).
assert (Out L M A) by (conclude lemma_ray4).
assert (Out L A M) by (conclude lemma_ray5).
assert (Per E D B) by (conclude_def SQ ).
assert (Col E D p) by (forward_using lemma_collinearorder).
assert (Col E D L) by (forward_using lemma_collinearorder).
assert (Col D p L) by (conclude lemma_collinear4).
assert (nCol p L A) by (conclude lemma_rightangleNC).
assert (neq p L) by (forward_using lemma_NCdistinct).
assert (Col p L D) by (forward_using lemma_collinearorder).
assert (neq L p) by (conclude lemma_inequalitysymmetric).
assert (Per D L A) by (conclude lemma_collinearright).
assert (Per D L M) by (conclude lemma_8_3).
assert (¬ eq B M).
{
intro.
assert (Per D L B) by (conclude cn_equalitysub).
assert (Per L D B) by (conclude lemma_collinearright).
assert (Per B D L) by (conclude lemma_8_2).
assert (¬ Per B D L) by (conclude lemma_8_7).
contradict.
}
assert (neq M B) by (conclude lemma_inequalitysymmetric).
assert (Par L D C B) by (forward_using lemma_parallelflip).
assert (Col C B M) by (forward_using lemma_collinearorder).
assert (Par L D M B) by (conclude lemma_collinearparallel).
assert (Par L D B M) by (forward_using lemma_parallelflip).
assert (Par B M L D) by (conclude lemma_parallelsymmetric).
assert (Par B M D L) by (forward_using lemma_parallelflip).
assert (Par D L B M) by (conclude lemma_parallelsymmetric).
assert (TP D L B M) by (conclude lemma_paralleldef2B).
assert (OS B M D L) by (conclude_def TP ).
assert (Par B M L D) by (conclude lemma_parallelsymmetric).
assert (Per L D B) by (conclude lemma_collinearright).
assert (Per B D L) by (conclude lemma_8_2).
assert (Par B D L M) by (conclude lemma_twoperpsparallel).
assert (Par B D M L) by (forward_using lemma_parallelflip).
assert (PG B M L D) by (conclude_def PG ).
assert (Par M L B D) by (conclude lemma_parallelsymmetric).
assert (TP M L B D) by (conclude lemma_paralleldef2B).
assert (OS B D M L) by (conclude_def TP ).
assert (BetS A M L) by (conclude axiom_betweennesssymmetry).
assert (Par M B L D) by (forward_using lemma_parallelflip).
assert (CongA A M B M L D) by (conclude proposition_29C).
assert (Per M L D) by (conclude lemma_8_2).
assert (Per A M B) by (conclude lemma_equaltorightisright).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col B C B) by (conclude_def Col ).
assert (BetS B M C) by (conclude lemma_altitudeofrighttriangle).
assert (¬ eq M C).
{
intro.
assert (Per A C B) by (conclude cn_equalitysub).
assert (¬ Per B A C) by (conclude lemma_8_7).
contradict.
}
assert (¬ eq L E).
{
intro.
assert (Par B D C E) by (conclude_def PG ).
assert (Par C E B D) by (conclude lemma_parallelsymmetric).
assert (Par M E B D) by (conclude cn_equalitysub).
assert (Par B D M E) by (conclude lemma_parallelsymmetric).
assert (Par B D C E) by (conclude lemma_parallelsymmetric).
assert (Par B D E C) by (forward_using lemma_parallelflip).
assert (Par B D E M) by (forward_using lemma_parallelflip).
assert (Col E C M) by (conclude lemma_Playfair).
assert (Col M C E) by (forward_using lemma_collinearorder).
assert (Col M C B) by (forward_using lemma_collinearorder).
assert (Col C E B) by (conclude lemma_collinear4).
assert (Col B C E) by (forward_using lemma_collinearorder).
assert (nCol B C E) by (forward_using lemma_parallelNC).
contradict.
}
assert (Par B M L D) by (conclude_def PG ).
assert (Par B M D L) by (forward_using lemma_parallelflip).
assert (Col D L E) by (forward_using lemma_collinearorder).
assert (neq E L) by (conclude lemma_inequalitysymmetric).
assert (Par B M E L) by (conclude lemma_collinearparallel).
assert (Par E L B M) by (conclude lemma_parallelsymmetric).
assert (Col B M C) by (forward_using lemma_collinearorder).
assert (neq C M) by (conclude lemma_inequalitysymmetric).
assert (Par E L C M) by (conclude lemma_collinearparallel).
assert (Par C M E L) by (conclude lemma_parallelsymmetric).
assert (Par M C E L) by (forward_using lemma_parallelflip).
assert (Col D L E) by (forward_using lemma_collinearorder).
assert (neq M L) by (forward_using lemma_betweennotequal).
assert (Per E L M) by (conclude lemma_collinearright).
assert (Per M L E) by (conclude lemma_8_2).
assert (Per C E D) by (conclude_def SQ ).
assert (Per D E C) by (conclude lemma_8_2).
assert (Per L E C) by (conclude lemma_collinearright).
assert (Par M C L E) by (forward_using lemma_parallelflip).
assert (Par L E M C) by (conclude lemma_parallelsymmetric).
assert (TP L E M C) by (conclude lemma_paralleldef2B).
assert (OS M C L E) by (conclude_def TP ).
assert (Par M L E C) by (conclude lemma_twoperpsparallel).
assert (Par M L C E) by (forward_using lemma_parallelflip).
assert (PG M C E L) by (conclude_def PG ).
assert (Cong B M D L) by (forward_using proposition_34).
assert (Cong M C L E) by (forward_using proposition_34).
assert (Cong B C D E) by (forward_using proposition_34).
assert (BetS D L E) by (conclude lemma_betweennesspreserved).
close.
Qed.
End Euclid.