Require Export GeoCoq.Elements.OriginalProofs.proposition_19.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_20 : 
   forall A B C, 
   Triangle A B C ->
   TG B A A C B C.
Proof.
(* Goal: forall (A B C : @Point Ax0) (_ : @Triangle Ax0 A B C), @TG Ax0 B A A C B C *)
intros.
(* Goal: @TG Ax0 B A A C B C *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: @TG Ax0 B A A C B C *)
assert (~ eq B A).
(* Goal: not (@Col Ax0 C D B) *)
(* Goal: @TG Ax0 B A A C B C *)
 {
(* Goal: not (@Col Ax0 C D B) *)
 intro.
(* Goal: False *)
 assert (Col B A C) by (conclude_def Col ).
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @TG Ax0 B A A C B C *)
assert (~ eq B C).
(* Goal: not (@Col Ax0 C D B) *)
(* Goal: @TG Ax0 B A A C B C *)
 {
(* Goal: not (@Col Ax0 C D B) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @TG Ax0 B A A C B C *)
assert (neq C B) by (conclude lemma_inequalitysymmetric).
(* Goal: @TG Ax0 B A A C B C *)
assert (~ eq C A).
(* Goal: not (@Col Ax0 C D B) *)
(* Goal: @TG Ax0 B A A C B C *)
 {
(* Goal: not (@Col Ax0 C D B) *)
 intro.
(* Goal: False *)
 assert (Col B C A) by (conclude_def Col ).
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists D, (BetS B A D /\ Cong A D C A)) by (conclude lemma_extension);destruct Tf as [D];spliter.
(* Goal: False *)
assert (neq A D) by (forward_using lemma_betweennotequal).
(* Goal: False *)
assert (neq D A) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
assert (neq B D) by (forward_using lemma_betweennotequal).
(* Goal: False *)
assert (neq D B) by (conclude lemma_inequalitysymmetric).
(* Goal: @TG Ax0 B A A C B C *)
assert (Cong A D A C) by (forward_using lemma_congruenceflip).
(* Goal: @TG Ax0 B A A C B C *)
assert (~ Col A D C).
(* Goal: not (@Col Ax0 C D B) *)
(* Goal: @TG Ax0 B A A C B C *)
 {
(* Goal: not (@Col Ax0 C D B) *)
 intro.
(* Goal: False *)
 assert (Col B A D) by (conclude_def Col ).
(* Goal: False *)
 assert (Col D A B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col D A C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq A D) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq D A) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col A B C) by (conclude lemma_collinear4).
(* Goal: False *)
 contradict.
 }
(* Goal: @TG Ax0 B A A C B C *)
assert (~ eq D C).
(* Goal: not (@Col Ax0 C D B) *)
(* Goal: @TG Ax0 B A A C B C *)
 {
(* Goal: not (@Col Ax0 C D B) *)
 intro.
(* Goal: False *)
 assert (Col A D C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @TG Ax0 B A A C B C *)
assert (Triangle A D C) by (conclude_def Triangle ).
(* Goal: @TG Ax0 B A A C B C *)
assert (isosceles A D C) by (conclude_def isosceles ).
(* Goal: @TG Ax0 B A A C B C *)
assert (CongA A D C A C D) by (conclude proposition_05).
(* Goal: @TG Ax0 B A A C B C *)
assert (~ Col A C D).
(* Goal: not (@Col Ax0 C D B) *)
(* Goal: @TG Ax0 B A A C B C *)
 {
(* Goal: not (@Col Ax0 C D B) *)
 intro.
(* Goal: False *)
 assert (Col A D C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @TG Ax0 B A A C B C *)
assert (CongA A C D D C A) by (conclude lemma_ABCequalsCBA).
(* Goal: @TG Ax0 B A A C B C *)
assert (CongA A D C D C A) by (conclude lemma_equalanglestransitive).
(* Goal: @TG Ax0 B A A C B C *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: @TG Ax0 B A A C B C *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @TG Ax0 B A A C B C *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: @TG Ax0 B A A C B C *)
assert (~ eq C D).
(* Goal: not (@Col Ax0 C D B) *)
(* Goal: @TG Ax0 B A A C B C *)
 {
(* Goal: not (@Col Ax0 C D B) *)
 intro.
(* Goal: False *)
 assert (Col A C D) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @TG Ax0 B A A C B C *)
assert (Out C D D) by (conclude lemma_ray4).
(* Goal: @TG Ax0 B A A C B C *)
assert (Out C B B) by (conclude lemma_ray4).
(* Goal: @TG Ax0 B A A C B C *)
assert (BetS D A B) by (conclude axiom_betweennesssymmetry).
(* Goal: @TG Ax0 B A A C B C *)
assert (LtA A D C D C B) by (conclude_def LtA ).
(* Goal: @TG Ax0 B A A C B C *)
assert (Out D A B) by (conclude lemma_ray4).
(* Goal: @TG Ax0 B A A C B C *)
assert (Out D C C) by (conclude lemma_ray4).
(* Goal: @TG Ax0 B A A C B C *)
assert (Out D B B) by (conclude lemma_ray4).
(* Goal: @TG Ax0 B A A C B C *)
assert (Cong D B D B) by (conclude cn_congruencereflexive).
(* Goal: @TG Ax0 B A A C B C *)
assert (Cong D C D C) by (conclude cn_congruencereflexive).
(* Goal: @TG Ax0 B A A C B C *)
assert (Cong B C B C) by (conclude cn_congruencereflexive).
(* Goal: @TG Ax0 B A A C B C *)
assert (CongA A D C B D C) by (conclude_def CongA ).
(* Goal: @TG Ax0 B A A C B C *)
assert (CongA B D C A D C) by (conclude lemma_equalanglessymmetric).
(* Goal: @TG Ax0 B A A C B C *)
assert (LtA B D C D C B) by (conclude lemma_angleorderrespectscongruence2).
(* Goal: @TG Ax0 B A A C B C *)
assert (~ Col B C D).
(* Goal: not (@Col Ax0 C D B) *)
(* Goal: @TG Ax0 B A A C B C *)
 {
(* Goal: not (@Col Ax0 C D B) *)
 intro.
(* Goal: False *)
 assert (Col B A D) by (conclude_def Col ).
(* Goal: False *)
 assert (Col D B A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col D B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq B D) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq D B) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col B A C) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @TG Ax0 B A A C B C *)
assert (~ Col C D B).
(* Goal: not (@Col Ax0 C D B) *)
(* Goal: @TG Ax0 B A A C B C *)
 {
(* Goal: not (@Col Ax0 C D B) *)
 intro.
(* Goal: False *)
 assert (Col B C D) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @TG Ax0 B A A C B C *)
assert (CongA C D B B D C) by (conclude lemma_ABCequalsCBA).
(* Goal: @TG Ax0 B A A C B C *)
assert (CongA B C D D C B) by (conclude lemma_ABCequalsCBA).
(* Goal: @TG Ax0 B A A C B C *)
assert (LtA C D B D C B) by (conclude lemma_angleorderrespectscongruence2).
(* Goal: @TG Ax0 B A A C B C *)
assert (LtA C D B B C D) by (conclude lemma_angleorderrespectscongruence).
(* Goal: @TG Ax0 B A A C B C *)
assert (Triangle B C D) by (conclude_def Triangle ).
(* Goal: @TG Ax0 B A A C B C *)
assert (Lt B C B D) by (conclude proposition_19).
(* Goal: @TG Ax0 B A A C B C *)
assert (TG B A A C B C) by (conclude_def TG ).
(* Goal: @TG Ax0 B A A C B C *)
close.
Qed.

End Euclid.


