Library GeoCoq.Elements.OriginalProofs.proposition_40

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 :
   ∀ 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.
intros.
assert (nCol D H E) by (conclude_def Triangle ).
assert (neq H E) by (forward_using lemma_NCdistinct).
assert (neq E H) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ R, (BetS E H R ∧ Cong H R E H)) by (conclude postulate_extension);destruct Tf as [R];spliter.
assert (BetS R H E) by (conclude axiom_betweennesssymmetry).
assert (nCol H E D) by (forward_using lemma_NCorder).
assert (Col R H E) by (conclude_def Col ).
assert (Col H E R) by (forward_using lemma_collinearorder).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (Col H E E) by (conclude_def Col ).
assert (neq R E) by (forward_using lemma_betweennotequal).
assert (nCol R E D) by (conclude lemma_NChelper).
let Tf:=fresh in
assert (Tf:∃ 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.
assert (Col R E H) by (forward_using lemma_collinearorder).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (Col R E E) by (conclude_def Col ).
assert (Par P Q H E) by (conclude lemma_collinearparallel).
assert (Col P D Q) by (conclude_def Col ).
assert (Col P Q D) by (forward_using lemma_collinearorder).
assert (Cong H E B C) by (conclude lemma_congruencesymmetric).
assert (Col C B H) by (forward_using lemma_collinearorder).
assert (Col C B E) by (forward_using lemma_collinearorder).
assert (nCol A B C) by (conclude_def Triangle ).
assert (neq B C) by (forward_using lemma_NCdistinct).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert (Col B H E) by (conclude lemma_collinear4).
assert (Col H E B) by (forward_using lemma_collinearorder).
assert (Col B C H) by (forward_using lemma_collinearorder).
assert (Col B C E) by (forward_using lemma_collinearorder).
assert (Col C H E) by (conclude lemma_collinear4).
assert (Col H E C) by (forward_using lemma_collinearorder).
assert (ET D H E D B C) by (conclude proposition_38).
assert (ET A B C D B C) by (conclude axiom_ETtransitive).
assert (nCol H E D) by (forward_using lemma_NCorder).
assert (nCol B C D) by (conclude lemma_NChelper).
assert (nCol D B C) by (forward_using lemma_NCorder).
assert (Triangle D B C) by (conclude_def Triangle ).
assert (Par A D B C) by (conclude proposition_39).
close.
Qed.

End Euclid.