Require Export GeoCoq.Elements.OriginalProofs.lemma_angletrichotomy.
Require Export GeoCoq.Elements.OriginalProofs.proposition_18.
Require Export GeoCoq.Elements.OriginalProofs.lemma_trichotomy1.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_19 : 
   forall A B C, 
   Triangle A B C -> LtA B C A A B C ->
   Lt A B A C.
Proof.
(* Goal: forall (A B C : @Point Ax0) (_ : @Triangle Ax0 A B C) (_ : @LtA Ax0 B C A A B C), @Lt Ax0 A B A C *)
intros.
(* Goal: @Lt Ax0 A B A C *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: @Lt Ax0 A B A C *)
assert (nCol B C A) by (forward_using lemma_NCorder).
(* Goal: @Lt Ax0 A B A C *)
assert (nCol A C B) by (forward_using lemma_NCorder).
(* Goal: @Lt Ax0 A B A C *)
assert (~ Cong A C A B).
(* Goal: not (not (@Lt Ax0 A B A C)) *)
(* Goal: @Lt Ax0 A B A C *)
 {
(* Goal: not (not (@Lt Ax0 A B A C)) *)
 intro.
(* Goal: False *)
 assert (Cong A B A C) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 assert (isosceles A B C) by (conclude_def isosceles ).
(* Goal: False *)
 assert (CongA A B C A C B) by (conclude proposition_05).
(* Goal: False *)
 assert (CongA A C B A B C) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (CongA B C A A C B) by (conclude lemma_ABCequalsCBA).
(* Goal: False *)
 assert (CongA B C A A B C) by (conclude lemma_equalanglestransitive).
(* Goal: False *)
 assert (LtA B C A B C A) by (conclude lemma_angleorderrespectscongruence).
(* Goal: False *)
 assert (~ LtA B C A B C A) by (conclude lemma_angletrichotomy).
(* Goal: False *)
 contradict.
 }
(* Goal: @Lt Ax0 A B A C *)
assert (~ Lt A C A B).
(* Goal: not (not (@Lt Ax0 A B A C)) *)
(* Goal: @Lt Ax0 A B A C *)
 {
(* Goal: not (not (@Lt Ax0 A B A C)) *)
 intro.
(* Goal: False *)
 assert (Triangle A C B) by (conclude_def Triangle ).
(* Goal: False *)
 assert (LtA C B A A C B) by (conclude proposition_18).
(* Goal: False *)
 assert (CongA A B C C B A) by (conclude lemma_ABCequalsCBA).
(* Goal: False *)
 assert (LtA A B C A C B) by (conclude lemma_angleorderrespectscongruence2).
(* Goal: False *)
 assert (CongA B C A A C B) by (conclude lemma_ABCequalsCBA).
(* Goal: False *)
 assert (LtA A B C B C A) by (conclude lemma_angleorderrespectscongruence).
(* Goal: False *)
 assert (~ LtA A B C B C A) by (conclude lemma_angletrichotomy).
(* Goal: False *)
 contradict.
 }
(* Goal: @Lt Ax0 A B A C *)
assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).
(* Goal: @Lt Ax0 A B A C *)
assert (neq A B) by (forward_using lemma_angledistinct).
(* Goal: @Lt Ax0 A B A C *)
assert (neq A C) by (forward_using lemma_angledistinct).
(* Goal: @Lt Ax0 A B A C *)
assert (~ ~ Lt A B A C).
(* Goal: not (not (@Lt Ax0 A B A C)) *)
(* Goal: @Lt Ax0 A B A C *)
 {
(* Goal: not (not (@Lt Ax0 A B A C)) *)
 intro.
(* Goal: False *)
 assert (Cong A B A C) by (conclude lemma_trichotomy1).
(* Goal: False *)
 assert (Cong A C A B) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 contradict.
 }
(* Goal: @Lt Ax0 A B A C *)
close.
Qed.

End Euclid.


