Require Export GeoCoq.Elements.OriginalProofs.proposition_31short.
Require Export GeoCoq.Elements.OriginalProofs.proposition_38.
Require Export GeoCoq.Elements.OriginalProofs.proposition_39.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_40 : 
   forall A B C D E H, 
   Cong B C H E -> ET A B C D H E -> Triangle A B C -> Triangle D H E -> Col B C H -> Col B C E -> OS A D B C -> neq A D ->
   Par A D B C.
Proof.
(* Goal: forall (A B C D E H : @Point Ax0) (_ : @Cong Ax0 B C H E) (_ : @ET Ax0 Ax1 Ax2 Ax A B C D H E) (_ : @Triangle Ax0 A B C) (_ : @Triangle Ax0 D H E) (_ : @Col Ax0 B C H) (_ : @Col Ax0 B C E) (_ : @OS Ax0 A D B C) (_ : @neq Ax0 A D), @Par Ax0 A D B C *)
intros.
(* Goal: @Par Ax0 A D B C *)
assert (nCol D H E) by (conclude_def Triangle ).
(* Goal: @Par Ax0 A D B C *)
assert (neq H E) by (forward_using lemma_NCdistinct).
(* Goal: @Par Ax0 A D B C *)
assert (neq E H) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists R, (BetS E H R /\ Cong H R E H)) by (conclude lemma_extension);destruct Tf as [R];spliter.
(* Goal: @Par Ax0 A D B C *)
assert (BetS R H E) by (conclude axiom_betweennesssymmetry).
(* Goal: @Par Ax0 A D B C *)
assert (nCol H E D) by (forward_using lemma_NCorder).
(* Goal: @Par Ax0 A D B C *)
assert (Col R H E) by (conclude_def Col ).
(* Goal: @Par Ax0 A D B C *)
assert (Col H E R) by (forward_using lemma_collinearorder).
(* Goal: @Par Ax0 A D B C *)
assert (eq E E) by (conclude cn_equalityreflexive).
(* Goal: @Par Ax0 A D B C *)
assert (Col H E E) by (conclude_def Col ).
(* Goal: @Par Ax0 A D B C *)
assert (neq R E) by (forward_using lemma_betweennotequal).
(* Goal: @Par Ax0 A D B C *)
assert (nCol R E D) by (conclude lemma_NChelper).
let Tf:=fresh in
assert (Tf:exists P Q M, (BetS P D Q /\ CongA P D H D H E /\ Par P Q R E /\ BetS P M E /\ BetS D M H)) by (conclude proposition_31short);destruct Tf as [P[Q[M]]];spliter.
(* Goal: @Par Ax0 A D B C *)
assert (Col R E H) by (forward_using lemma_collinearorder).
(* Goal: @Par Ax0 A D B C *)
assert (Par P Q H E) by (conclude lemma_collinearparallel).
(* Goal: @Par Ax0 A D B C *)
assert (Col P D Q) by (conclude_def Col ).
(* Goal: @Par Ax0 A D B C *)
assert (Col P Q D) by (forward_using lemma_collinearorder).
(* Goal: @Par Ax0 A D B C *)
assert (Cong H E B C) by (conclude lemma_congruencesymmetric).
(* Goal: @Par Ax0 A D B C *)
assert (Col C B H) by (forward_using lemma_collinearorder).
(* Goal: @Par Ax0 A D B C *)
assert (Col C B E) by (forward_using lemma_collinearorder).
(* Goal: @Par Ax0 A D B C *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: @Par Ax0 A D B C *)
assert (neq B C) by (forward_using lemma_NCdistinct).
(* Goal: @Par Ax0 A D B C *)
assert (neq C B) by (conclude lemma_inequalitysymmetric).
(* Goal: @Par Ax0 A D B C *)
assert (Col B H E) by (conclude lemma_collinear4).
(* Goal: @Par Ax0 A D B C *)
assert (Col H E B) by (forward_using lemma_collinearorder).
(* Goal: @Par Ax0 A D B C *)
assert (Col B C H) by (forward_using lemma_collinearorder).
(* Goal: @Par Ax0 A D B C *)
assert (Col B C E) by (forward_using lemma_collinearorder).
(* Goal: @Par Ax0 A D B C *)
assert (Col C H E) by (conclude lemma_collinear4).
(* Goal: @Par Ax0 A D B C *)
assert (Col H E C) by (forward_using lemma_collinearorder).
(* Goal: @Par Ax0 A D B C *)
assert (ET D H E D B C) by (conclude proposition_38).
(* Goal: @Par Ax0 A D B C *)
assert (ET A B C D B C) by (conclude axiom_ETtransitive).
(* Goal: @Par Ax0 A D B C *)
assert (nCol H E D) by (forward_using lemma_NCorder).
(* Goal: @Par Ax0 A D B C *)
assert (nCol B C D) by (conclude lemma_NChelper).
(* Goal: @Par Ax0 A D B C *)
assert (nCol D B C) by (forward_using lemma_NCorder).
(* Goal: @Par Ax0 A D B C *)
assert (Triangle D B C) by (conclude_def Triangle ).
(* Goal: @Par Ax0 A D B C *)
assert (Par A D B C) by (conclude proposition_39).
(* Goal: @Par Ax0 A D B C *)
close.
Qed.

End Euclid.


