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 : 
   forall 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.
(* Goal: forall (A B C D E : @Point Ax0) (_ : @Triangle Ax0 A B C) (_ : @BetS Ax0 A E C) (_ : @BetS Ax0 B D E), and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
intros.
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (BetS E D B) by (conclude axiom_betweennesssymmetry).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Col A E C) by (conclude_def Col ).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Col A C E) by (forward_using lemma_collinearorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (neq A E) by (forward_using lemma_betweennotequal).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol A C B) by (forward_using lemma_NCorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Col A C A) by (conclude_def Col ).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol A E B) by (conclude lemma_NChelper).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol A B E) by (forward_using lemma_NCorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Triangle A B E) by (conclude_def Triangle ).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (TG B A A E B E) by (conclude proposition_20).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (TT B A A C B E E C) by (conclude lemma_21helper).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol A C B) by (forward_using lemma_NCorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Col A E C) by (conclude_def Col ).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Col A C E) by (forward_using lemma_collinearorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Col A C C) by (conclude_def Col ).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (neq E C) by (forward_using lemma_betweennotequal).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol E C B) by (conclude lemma_NChelper).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol E B C) by (forward_using lemma_NCorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Col E D B) by (conclude_def Col ).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Col E B D) by (forward_using lemma_collinearorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (eq E E) by (conclude cn_equalityreflexive).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Col E B E) by (conclude_def Col ).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (neq E D) by (forward_using lemma_betweennotequal).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol E D C) by (conclude lemma_NChelper).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol E C D) by (forward_using lemma_NCorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Triangle E C D) by (conclude_def Triangle ).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (TG C E E D C D) by (conclude proposition_20).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (TT C E E B C D D B) by (conclude lemma_21helper).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (TT E B C E C D D B) by (conclude lemma_TTorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (TT B E E C C D D B) by (conclude lemma_TTflip).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (TT B A A C C D D B) by (conclude lemma_TTtransitive).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (TT B A A C B D D C) by (conclude lemma_TTflip2).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol C E D) by (forward_using lemma_NCorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Triangle C E D) by (conclude_def Triangle ).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (LtA D E C C D B) by (conclude proposition_16).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol E B C) by (forward_using lemma_NCorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Col E B B) by (conclude_def Col ).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Col E D B) by (conclude_def Col ).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Col E B D) by (forward_using lemma_collinearorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (neq B D) by (forward_using lemma_betweennotequal).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (neq D B) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol D B C) by (conclude lemma_NChelper).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol B A E) by (forward_using lemma_NCorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Triangle B A E) by (conclude_def Triangle ).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (LtA E A B B E C) by (conclude proposition_16).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (CongA B A E E A B) by (conclude lemma_ABCequalsCBA).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (LtA B A E B E C) by (conclude lemma_angleorderrespectscongruence2).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol C E B) by (forward_using lemma_NCorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (CongA C E B B E C) by (conclude lemma_ABCequalsCBA).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (LtA B A E C E B) by (conclude lemma_angleorderrespectscongruence).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (neq A E) by (forward_using lemma_betweennotequal).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Out A E C) by (conclude lemma_ray4).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Out A C E) by (conclude lemma_ray5).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (neq A B) by (forward_using lemma_NCdistinct).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Out A B B) by (conclude lemma_ray4).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol B A C) by (forward_using lemma_NCorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (CongA B A C B A C) by (conclude lemma_equalanglesreflexive).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (CongA B A C B A E) by (conclude lemma_equalangleshelper).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (BetS E D B) by (conclude axiom_betweennesssymmetry).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Out E D B) by (conclude lemma_ray4).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (Out E C C) by (conclude lemma_ray4).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol C E D) by (forward_using lemma_NCorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (CongA C E D C E D) by (conclude lemma_equalanglesreflexive).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (CongA C E D C E B) by (conclude lemma_equalangleshelper).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (LtA B A E C E D) by (conclude lemma_angleorderrespectscongruence).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (LtA B A C C E D) by (conclude lemma_angleorderrespectscongruence2).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol D E C) by (forward_using lemma_NCorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (CongA D E C C E D) by (conclude lemma_ABCequalsCBA).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (LtA B A C D E C) by (conclude lemma_angleorderrespectscongruence).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (LtA B A C C D B) by (conclude lemma_angleordertransitive).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (nCol B D C) by (forward_using lemma_NCorder).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (CongA B D C C D B) by (conclude lemma_ABCequalsCBA).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
assert (LtA B A C B D C) by (conclude lemma_angleorderrespectscongruence).
(* Goal: and (@TT Ax0 B A A C B D D C) (@LtA Ax0 B A C B D C) *)
close.
Qed.

End Euclid.

