Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearparallel2.
Require Export GeoCoq.Elements.OriginalProofs.proposition_33.
Require Export GeoCoq.Elements.OriginalProofs.proposition_35.
Require Export GeoCoq.Elements.OriginalProofs.lemma_PGsymmetric.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_36A : 
   forall A B C D E F G H M, 
   PG A B C D -> PG E F G H -> Col A D E -> Col A D H -> Col B C F -> Col B C G -> Cong B C F G -> BetS B M H -> BetS C M E ->
   EF A B C D E F G H.
Proof.
(* Goal: forall (A B C D E F G H M : @Point Ax0) (_ : @PG Ax0 A B C D) (_ : @PG Ax0 E F G H) (_ : @Col Ax0 A D E) (_ : @Col Ax0 A D H) (_ : @Col Ax0 B C F) (_ : @Col Ax0 B C G) (_ : @Cong Ax0 B C F G) (_ : @BetS Ax0 B M H) (_ : @BetS Ax0 C M E), @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
intros.
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert ((Par A B C D /\ Par A D B C)) by (conclude_def PG ).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert ((Par E F G H /\ Par E H F G)) by (conclude_def PG ).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (nCol A C D) by (forward_using lemma_parallelNC).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (neq A D) by (forward_using lemma_NCdistinct).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Cong A D B C) by (forward_using proposition_34).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Cong E H F G) by (forward_using proposition_34).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Cong F G E H) by (conclude lemma_congruencesymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Cong B C E H) by (conclude lemma_congruencetransitive).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Par B C A D) by (conclude lemma_parallelsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (nCol A B C) by (forward_using lemma_parallelNC).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (neq B C) by (forward_using lemma_NCdistinct).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (neq E H) by (conclude axiom_nocollapse).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Par B C E H) by (conclude lemma_collinearparallel2).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert ((Par B E C H /\ Cong B E C H)) by (conclude proposition_33).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Par E B C H) by (forward_using lemma_parallelflip).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Par E H B C) by (conclude lemma_parallelsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (PG E B C H) by (conclude_def PG ).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (EF A B C D E B C H) by (conclude proposition_35).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Cong F G B C) by (conclude lemma_congruencesymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Cong G F C B) by (forward_using lemma_congruenceflip).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (PG C H E B) by (conclude lemma_PGsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (nCol A B C) by (forward_using lemma_parallelNC).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (neq B C) by (forward_using lemma_NCdistinct).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (neq C B) by (conclude lemma_inequalitysymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Col C F G) by (conclude lemma_collinear4).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Col G F C) by (forward_using lemma_collinearorder).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Col C B F) by (forward_using lemma_collinearorder).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Col C B G) by (forward_using lemma_collinearorder).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Col B F G) by (conclude lemma_collinear4).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (Col G F B) by (forward_using lemma_collinearorder).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (PG G H E F) by (conclude lemma_PGsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (EF G H E F C H E B) by (conclude proposition_35).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (EF G H E F E B C H) by (forward_using axiom_EFpermutation).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (EF E B C H G H E F) by (conclude axiom_EFsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (EF A B C D G H E F) by (conclude axiom_EFtransitive).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
assert (EF A B C D E F G H) by (forward_using axiom_EFpermutation).
(* Goal: @EF Ax0 Ax1 Ax2 Ax A B C D E F G H *)
close.
Qed.

End Euclid.


