Require Export GeoCoq.Elements.OriginalProofs.lemma_triangletoparallelogram.
Require Export GeoCoq.Elements.OriginalProofs.lemma_PGrotate.
Require Export GeoCoq.Elements.OriginalProofs.proposition_35.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_37 : 
   forall A B C D, 
   Par A D B C ->
   ET A B C D B C.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @Par Ax0 A D B C), @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
intros.
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Par B C A D) by (conclude lemma_parallelsymmetric).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Par C B A D) by (forward_using lemma_parallelflip).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Col A D A) by (conclude_def Col ).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Col A D D) by (conclude_def Col ).
let Tf:=fresh in
assert (Tf:exists E, (PG A E B C /\ Col A D E)) by (conclude lemma_triangletoparallelogram);destruct Tf as [E];spliter.
let Tf:=fresh in
assert (Tf:exists F, (PG D F B C /\ Col A D F)) by (conclude lemma_triangletoparallelogram);destruct Tf as [F];spliter.
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (PG E B C A) by (conclude lemma_PGrotate).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (PG F B C D) by (conclude lemma_PGrotate).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Col D A F) by (forward_using lemma_collinearorder).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Col D A E) by (forward_using lemma_collinearorder).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (nCol C A D) by (forward_using lemma_parallelNC).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (neq A D) by (forward_using lemma_NCdistinct).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (neq D A) by (conclude lemma_inequalitysymmetric).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Col A F E) by (conclude lemma_collinear4).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Col E A D) by (forward_using lemma_collinearorder).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Col E A F) by (forward_using lemma_collinearorder).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (EF E B C A F B C D) by (conclude proposition_35).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Cong_3 B E A A C B) by (conclude proposition_34).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Cong_3 B F D D C B) by (conclude proposition_34).
let Tf:=fresh in
assert (Tf:exists M, (BetS E M C /\ BetS B M A)) by (conclude lemma_diagonalsmeet);destruct Tf as [M];spliter.
let Tf:=fresh in
assert (Tf:exists m, (BetS F m C /\ BetS B m D)) by (conclude lemma_diagonalsmeet);destruct Tf as [m];spliter.
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Col B M A) by (conclude_def Col ).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Col B m D) by (conclude_def Col ).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Col B A M) by (forward_using lemma_collinearorder).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Col B D m) by (forward_using lemma_collinearorder).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Par E B C A) by (conclude_def PG ).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (nCol E B A) by (forward_using lemma_parallelNC).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (nCol B A E) by (forward_using lemma_NCorder).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (TS E B A C) by (conclude_def TS ).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (TS C B A E) by (conclude lemma_oppositesidesymmetric).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (Par D F B C) by (conclude_def PG ).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (nCol D F B) by (forward_using lemma_parallelNC).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (nCol B D F) by (forward_using lemma_NCorder).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (TS F B D C) by (conclude_def TS ).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (TS C B D F) by (conclude lemma_oppositesidesymmetric).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (ET B E A A C B) by (conclude axiom_congruentequal).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (ET B E A C B A) by (forward_using axiom_ETpermutation).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (ET C B A B E A) by (conclude axiom_ETsymmetric).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (ET C B A B A E) by (forward_using axiom_ETpermutation).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (ET B F D D C B) by (conclude axiom_congruentequal).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (ET B F D C B D) by (forward_using axiom_ETpermutation).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (ET C B D B F D) by (conclude axiom_ETsymmetric).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (ET C B D B D F) by (forward_using axiom_ETpermutation).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (EF E B C A C B F D) by (forward_using axiom_EFpermutation).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (EF C B F D E B C A) by (conclude axiom_EFsymmetric).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (EF C B F D C B E A) by (forward_using axiom_EFpermutation).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (EF C B E A C B F D) by (conclude axiom_EFsymmetric).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (ET C B A C B D) by (conclude axiom_halvesofequals).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (ET C B A D B C) by (forward_using axiom_ETpermutation).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (ET D B C C B A) by (conclude axiom_ETsymmetric).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (ET D B C A B C) by (forward_using axiom_ETpermutation).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
assert (ET A B C D B C) by (conclude axiom_ETsymmetric).
(* Goal: @ET Ax0 Ax1 Ax2 Ax A B C D B C *)
close.
Qed.

End Euclid.


