Require Export GeoCoq.Elements.OriginalProofs.lemma_congruenceflip.
Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthancongruence.
Require Export GeoCoq.Elements.OriginalProofs.lemma_outerconnectivity.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_trichotomy1 : 
   forall A B C D, 
   ~ Lt A B C D -> ~ Lt C D A B -> neq A B -> neq C D ->
   Cong A B C D.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : not (@Lt Ax0 A B C D)) (_ : not (@Lt Ax0 C D A B)) (_ : @neq Ax0 A B) (_ : @neq Ax0 C D), @Cong Ax0 A B C D *)
intros.
(* Goal: @Cong Ax0 A B C D *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists P, (BetS B A P /\ Cong A P A B)) by (conclude lemma_extension);destruct Tf as [P];spliter.
(* Goal: @Cong Ax0 A B C D *)
assert (BetS P A B) by (conclude axiom_betweennesssymmetry).
(* Goal: @Cong Ax0 A B C D *)
assert (neq A P) by (forward_using lemma_betweennotequal).
(* Goal: @Cong Ax0 A B C D *)
assert (neq P A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists E, (BetS P A E /\ Cong A E C D)) by (conclude lemma_extension);destruct Tf as [E];spliter.
(* Goal: @Cong Ax0 A B C D *)
assert (~ BetS A B E).
(* Goal: not (@BetS Ax0 A E B) *)
(* Goal: @Cong Ax0 A B C D *)
 {
(* Goal: not (@BetS Ax0 A E B) *)
 intro.
(* Goal: @Cong Ax0 A B C D *)
 assert (Cong A B A B) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (Lt A B A E) by (conclude_def Lt ).
(* Goal: False *)
 assert (Lt A B C D) by (conclude lemma_lessthancongruence).
(* Goal: False *)
 contradict.
 }
(* Goal: @Cong Ax0 A B C D *)
assert (~ BetS A E B).
(* Goal: not (@BetS Ax0 A E B) *)
(* Goal: @Cong Ax0 A B C D *)
 {
(* Goal: not (@BetS Ax0 A E B) *)
 intro.
(* Goal: False *)
 assert (Lt C D A B) by (conclude_def Lt ).
(* Goal: False *)
 contradict.
 }
(* Goal: @Cong Ax0 A B C D *)
assert (eq E B) by (conclude lemma_outerconnectivity).
(* Goal: @Cong Ax0 A B C D *)
assert (Cong A B A B) by (conclude cn_congruencereflexive).
(* Goal: @Cong Ax0 A B C D *)
assert (Cong A B A E) by (conclude cn_equalitysub).
(* Goal: @Cong Ax0 A B C D *)
assert (Cong A B C D) by (conclude lemma_congruencetransitive).
(* Goal: @Cong Ax0 A B C D *)
close.
Qed.

End Euclid.


