Library GeoCoq.Elements.OriginalProofs.proposition_21

Require Export GeoCoq.Elements.OriginalProofs.lemma_NChelper.
Require Export GeoCoq.Elements.OriginalProofs.proposition_20.
Require Export GeoCoq.Elements.OriginalProofs.lemma_21helper.
Require Export GeoCoq.Elements.OriginalProofs.lemma_TTorder.
Require Export GeoCoq.Elements.OriginalProofs.lemma_TTflip.
Require Export GeoCoq.Elements.OriginalProofs.lemma_TTtransitive.
Require Export GeoCoq.Elements.OriginalProofs.lemma_TTflip2.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NCdistinct.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_21 :
   ∀ A B C D E,
   Triangle A B C → BetS A E C → BetS B D E →
   TT B A A C B D D C ∧ LtA B A C B D C.
Proof.
intros.
assert (BetS E D B) by (conclude axiom_betweennesssymmetry).
assert (nCol A B C) by (conclude_def Triangle ).
assert (Col A E C) by (conclude_def Col ).
assert (Col A C E) by (forward_using lemma_collinearorder).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (nCol A C B) by (forward_using lemma_NCorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A C A) by (conclude_def Col ).
assert (nCol A E B) by (conclude lemma_NChelper).
assert (nCol A B E) by (forward_using lemma_NCorder).
assert (Triangle A B E) by (conclude_def Triangle ).
assert (TG B A A E B E) by (conclude proposition_20).
assert (TG A B A E B E) by (forward_using lemma_TGflip).
assert (Cong E C E C) by (conclude cn_congruencereflexive).
assert (TT B A A C B E E C) by (conclude lemma_21helper).
assert (nCol A C B) by (forward_using lemma_NCorder).
assert (Col A E C) by (conclude_def Col ).
assert (Col A C E) by (forward_using lemma_collinearorder).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col A C C) by (conclude_def Col ).
assert (neq E C) by (forward_using lemma_betweennotequal).
assert (nCol E C B) by (conclude lemma_NChelper).
assert (nCol E B C) by (forward_using lemma_NCorder).
assert (Col E D B) by (conclude_def Col ).
assert (Col E B D) by (forward_using lemma_collinearorder).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (Col E B E) by (conclude_def Col ).
assert (neq E D) by (forward_using lemma_betweennotequal).
assert (nCol E D C) by (conclude lemma_NChelper).
assert (nCol E C D) by (forward_using lemma_NCorder).
assert (Triangle E C D) by (conclude_def Triangle ).
assert (TG C E E D C D) by (conclude proposition_20).
assert (TT C E E B C D D B) by (conclude lemma_21helper).
assert (TT E B C E C D D B) by (conclude lemma_TTorder).
assert (TT B E E C C D D B) by (conclude lemma_TTflip).
assert (TT B A A C C D D B) by (conclude lemma_TTtransitive).
assert (TT B A A C B D D C) by (conclude lemma_TTflip2).
assert (nCol C E D) by (forward_using lemma_NCorder).
assert (Triangle C E D) by (conclude_def Triangle ).
assert (LtA D E C C D B) by (conclude proposition_16).
assert (CongA C E D D E C) by (conclude lemma_ABCequalsCBA).
assert (LtA C E D C D B) by (conclude lemma_angleorderrespectscongruence2).
assert (nCol E B C) by (forward_using lemma_NCorder).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col E B B) by (conclude_def Col ).
assert (Col E D B) by (conclude_def Col ).
assert (Col E B D) by (forward_using lemma_collinearorder).
assert (neq B D) by (forward_using lemma_betweennotequal).
assert (neq D B) by (conclude lemma_inequalitysymmetric).
assert (nCol D B C) by (conclude lemma_NChelper).
assert (nCol B D C) by (forward_using lemma_NCorder).
assert (CongA B D C C D B) by (conclude lemma_ABCequalsCBA).
assert (LtA C E D B D C) by (conclude lemma_angleorderrespectscongruence).
assert (nCol B A E) by (forward_using lemma_NCorder).
assert (Triangle B A E) by (conclude_def Triangle ).
assert (LtA E A B B E C) by (conclude proposition_16).
assert (CongA B A E E A B) by (conclude lemma_ABCequalsCBA).
assert (LtA B A E B E C) by (conclude lemma_angleorderrespectscongruence2).
assert (nCol C E B) by (forward_using lemma_NCorder).
assert (CongA C E B B E C) by (conclude lemma_ABCequalsCBA).
assert (LtA B A E C E B) by (conclude lemma_angleorderrespectscongruence).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (Out A E C) by (conclude lemma_ray4).
assert (Out A C E) by (conclude lemma_ray5).
assert (neq A B) by (forward_using lemma_NCdistinct).
assert (Out A B B) by (conclude lemma_ray4).
assert (nCol B A C) by (forward_using lemma_NCorder).
assert (CongA B A C B A C) by (conclude lemma_equalanglesreflexive).
assert (CongA B A C B A E) by (conclude lemma_equalangleshelper).
assert (LtA B A C C E B) by (conclude lemma_angleorderrespectscongruence2).
assert (BetS E D B) by (conclude axiom_betweennesssymmetry).
assert (Out E D B) by (conclude lemma_ray4).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Out E C C) by (conclude lemma_ray4).
assert (nCol C E D) by (forward_using lemma_NCorder).
assert (CongA C E D C E D) by (conclude lemma_equalanglesreflexive).
assert (CongA C E D C E B) by (conclude lemma_equalangleshelper).
assert (LtA B A E C E D) by (conclude lemma_angleorderrespectscongruence).
assert (CongA B A E B A C) by (conclude lemma_equalanglessymmetric).
assert (LtA B A C C E D) by (conclude lemma_angleorderrespectscongruence2).
assert (nCol D E C) by (forward_using lemma_NCorder).
assert (CongA D E C C E D) by (conclude lemma_ABCequalsCBA).
assert (LtA B A C D E C) by (conclude lemma_angleorderrespectscongruence).
assert (LtA B A C C D B) by (conclude lemma_angleordertransitive).
assert (nCol B D C) by (forward_using lemma_NCorder).
assert (CongA B D C C D B) by (conclude lemma_ABCequalsCBA).
assert (LtA B A C B D C) by (conclude lemma_angleorderrespectscongruence).
close.
Qed.

End Euclid.