# Library GeoCoq.Elements.OriginalProofs.lemma_paste5

Require Export GeoCoq.Elements.OriginalProofs.lemma_rectangleparallelogram.

Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelNC.

Require Export GeoCoq.Elements.OriginalProofs.proposition_34.

Require Export GeoCoq.Elements.OriginalProofs.lemma_crossimpliesopposite.

Section Euclid.

Context `{Ax:area}.

Lemma lemma_paste5 :

∀ B C D E L M b c d e l m,

EF B M L D b m l d → EF M C E L m c e l → BetS B M C → BetS b m c → BetS E L D → BetS e l d → RE M C E L → RE m c e l →

EF B C E D b c e d.

Proof.

intros.

assert (PG M C E L) by (conclude lemma_rectangleparallelogram).

assert (PG m c e l) by (conclude lemma_rectangleparallelogram).

assert (Par M C E L) by (conclude_def PG ).

assert (nCol M C L) by (forward_using lemma_parallelNC).

assert (Par m c e l) by (conclude_def PG ).

assert (nCol m c l) by (forward_using lemma_parallelNC).

assert (Cong_3 C M L L E C) by (conclude proposition_34).

assert (Cong_3 c m l l e c) by (conclude proposition_34).

assert (ET C M L L E C) by (conclude axiom_congruentequal).

assert (ET c m l l e c) by (conclude axiom_congruentequal).

assert (CR M E C L) by (conclude_def RE ).

assert (CR m e c l) by (conclude_def RE ).

assert (ET c m l c l e) by (forward_using axiom_ETpermutation).

assert (ET c l e c m l) by (conclude axiom_ETsymmetric).

assert (ET c l e m c l) by (forward_using axiom_ETpermutation).

assert (ET m c l c l e) by (conclude axiom_ETsymmetric).

assert (ET C M L C L E) by (forward_using axiom_ETpermutation).

assert (ET C L E C M L) by (conclude axiom_ETsymmetric).

assert (ET C L E M C L) by (forward_using axiom_ETpermutation).

assert (ET M C L C L E) by (conclude axiom_ETsymmetric).

assert (TS M C L E) by (forward_using lemma_crossimpliesopposite).

assert (TS m c l e) by (forward_using lemma_crossimpliesopposite).

assert (ET M C L m c l) by (conclude axiom_halvesofequals).

assert (EF M C E L e c m l) by (forward_using axiom_EFpermutation).

assert (EF e c m l M C E L) by (conclude axiom_EFsymmetric).

assert (EF e c m l E C M L) by (forward_using axiom_EFpermutation).

assert (EF E C M L e c m l) by (conclude axiom_EFsymmetric).

assert (TS E C L M) by (conclude lemma_oppositesidesymmetric).

assert (TS e c l m) by (conclude lemma_oppositesidesymmetric).

assert (ET M C L E C L) by (forward_using axiom_ETpermutation).

assert (ET E C L M C L) by (conclude axiom_ETsymmetric).

assert (ET E C L C L M) by (forward_using axiom_ETpermutation).

assert (ET m c l e c l) by (forward_using axiom_ETpermutation).

assert (ET e c l m c l) by (conclude axiom_ETsymmetric).

assert (ET e c l c l m) by (forward_using axiom_ETpermutation).

assert (ET E C L e c l) by (conclude axiom_halvesofequals).

assert (EF B M L D d b m l) by (forward_using axiom_EFpermutation).

assert (EF d b m l B M L D) by (conclude axiom_EFsymmetric).

assert (EF d b m l D B M L) by (forward_using axiom_EFpermutation).

assert (EF D B M L d b m l) by (conclude axiom_EFsymmetric).

assert (EF D B C L d b c l) by (conclude axiom_paste2).

assert (EF D B C L b d l c) by (forward_using axiom_EFpermutation).

assert (EF b d l c D B C L) by (conclude axiom_EFsymmetric).

assert (EF b d l c B D L C) by (forward_using axiom_EFpermutation).

assert (EF B D L C b d l c) by (conclude axiom_EFsymmetric).

assert (ET E C L l e c) by (forward_using axiom_ETpermutation).

assert (ET l e c E C L) by (conclude axiom_ETsymmetric).

assert (ET l e c L E C) by (forward_using axiom_ETpermutation).

assert (ET L E C l e c) by (conclude axiom_ETsymmetric).

assert (BetS D L E) by (conclude axiom_betweennesssymmetry).

assert (BetS d l e) by (conclude axiom_betweennesssymmetry).

assert (EF B D E C b d e c) by (conclude axiom_paste2).

assert (EF B D E C b c e d) by (forward_using axiom_EFpermutation).

assert (EF b c e d B D E C) by (conclude axiom_EFsymmetric).

assert (EF b c e d B C E D) by (forward_using axiom_EFpermutation).

assert (EF B C E D b c e d) by (conclude axiom_EFsymmetric).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelNC.

Require Export GeoCoq.Elements.OriginalProofs.proposition_34.

Require Export GeoCoq.Elements.OriginalProofs.lemma_crossimpliesopposite.

Section Euclid.

Context `{Ax:area}.

Lemma lemma_paste5 :

∀ B C D E L M b c d e l m,

EF B M L D b m l d → EF M C E L m c e l → BetS B M C → BetS b m c → BetS E L D → BetS e l d → RE M C E L → RE m c e l →

EF B C E D b c e d.

Proof.

intros.

assert (PG M C E L) by (conclude lemma_rectangleparallelogram).

assert (PG m c e l) by (conclude lemma_rectangleparallelogram).

assert (Par M C E L) by (conclude_def PG ).

assert (nCol M C L) by (forward_using lemma_parallelNC).

assert (Par m c e l) by (conclude_def PG ).

assert (nCol m c l) by (forward_using lemma_parallelNC).

assert (Cong_3 C M L L E C) by (conclude proposition_34).

assert (Cong_3 c m l l e c) by (conclude proposition_34).

assert (ET C M L L E C) by (conclude axiom_congruentequal).

assert (ET c m l l e c) by (conclude axiom_congruentequal).

assert (CR M E C L) by (conclude_def RE ).

assert (CR m e c l) by (conclude_def RE ).

assert (ET c m l c l e) by (forward_using axiom_ETpermutation).

assert (ET c l e c m l) by (conclude axiom_ETsymmetric).

assert (ET c l e m c l) by (forward_using axiom_ETpermutation).

assert (ET m c l c l e) by (conclude axiom_ETsymmetric).

assert (ET C M L C L E) by (forward_using axiom_ETpermutation).

assert (ET C L E C M L) by (conclude axiom_ETsymmetric).

assert (ET C L E M C L) by (forward_using axiom_ETpermutation).

assert (ET M C L C L E) by (conclude axiom_ETsymmetric).

assert (TS M C L E) by (forward_using lemma_crossimpliesopposite).

assert (TS m c l e) by (forward_using lemma_crossimpliesopposite).

assert (ET M C L m c l) by (conclude axiom_halvesofequals).

assert (EF M C E L e c m l) by (forward_using axiom_EFpermutation).

assert (EF e c m l M C E L) by (conclude axiom_EFsymmetric).

assert (EF e c m l E C M L) by (forward_using axiom_EFpermutation).

assert (EF E C M L e c m l) by (conclude axiom_EFsymmetric).

assert (TS E C L M) by (conclude lemma_oppositesidesymmetric).

assert (TS e c l m) by (conclude lemma_oppositesidesymmetric).

assert (ET M C L E C L) by (forward_using axiom_ETpermutation).

assert (ET E C L M C L) by (conclude axiom_ETsymmetric).

assert (ET E C L C L M) by (forward_using axiom_ETpermutation).

assert (ET m c l e c l) by (forward_using axiom_ETpermutation).

assert (ET e c l m c l) by (conclude axiom_ETsymmetric).

assert (ET e c l c l m) by (forward_using axiom_ETpermutation).

assert (ET E C L e c l) by (conclude axiom_halvesofequals).

assert (EF B M L D d b m l) by (forward_using axiom_EFpermutation).

assert (EF d b m l B M L D) by (conclude axiom_EFsymmetric).

assert (EF d b m l D B M L) by (forward_using axiom_EFpermutation).

assert (EF D B M L d b m l) by (conclude axiom_EFsymmetric).

assert (EF D B C L d b c l) by (conclude axiom_paste2).

assert (EF D B C L b d l c) by (forward_using axiom_EFpermutation).

assert (EF b d l c D B C L) by (conclude axiom_EFsymmetric).

assert (EF b d l c B D L C) by (forward_using axiom_EFpermutation).

assert (EF B D L C b d l c) by (conclude axiom_EFsymmetric).

assert (ET E C L l e c) by (forward_using axiom_ETpermutation).

assert (ET l e c E C L) by (conclude axiom_ETsymmetric).

assert (ET l e c L E C) by (forward_using axiom_ETpermutation).

assert (ET L E C l e c) by (conclude axiom_ETsymmetric).

assert (BetS D L E) by (conclude axiom_betweennesssymmetry).

assert (BetS d l e) by (conclude axiom_betweennesssymmetry).

assert (EF B D E C b d e c) by (conclude axiom_paste2).

assert (EF B D E C b c e d) by (forward_using axiom_EFpermutation).

assert (EF b c e d B D E C) by (conclude axiom_EFsymmetric).

assert (EF b c e d B C E D) by (forward_using axiom_EFpermutation).

assert (EF B C E D b c e d) by (conclude axiom_EFsymmetric).

close.

Qed.

End Euclid.