Require Export GeoCoq.Elements.OriginalProofs.proposition_16.
Require Export GeoCoq.Elements.OriginalProofs.proposition_05.
Require Export GeoCoq.Elements.OriginalProofs.lemma_angleordertransitive.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

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

End Euclid.


