Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthancongruence2.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ray4.
Require Export GeoCoq.Elements.OriginalProofs.lemma_layoffunique.
Require Export GeoCoq.Elements.OriginalProofs.lemma_trichotomy2.
Require Export GeoCoq.Elements.OriginalProofs.lemma_outerconnectivity.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_lessthanadditive : 
   forall A B C D E F, 
   Lt A B C D -> BetS A B E -> BetS C D F -> Cong B E D F ->
   Lt A E C F.
Proof.
(* Goal: forall (A B C D E F : @Point Ax0) (_ : @Lt Ax0 A B C D) (_ : @BetS Ax0 A B E) (_ : @BetS Ax0 C D F) (_ : @Cong Ax0 B E D F), @Lt Ax0 A E C F *)
intros.
let Tf:=fresh in
assert (Tf:exists b, (BetS C b D /\ Cong C b A B)) by (conclude_def Lt );destruct Tf as [b];spliter.
(* Goal: @Lt Ax0 A E C F *)
assert (Cong A B C b) by (conclude lemma_congruencesymmetric).
(* Goal: @Lt Ax0 A E C F *)
assert (neq C b) by (forward_using lemma_betweennotequal).
(* Goal: @Lt Ax0 A E C F *)
assert (neq b C) by (conclude lemma_inequalitysymmetric).
(* Goal: @Lt Ax0 A E C F *)
assert (neq B E) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists e, (BetS C b e /\ Cong b e B E)) by (conclude lemma_extension);destruct Tf as [e];spliter.
(* Goal: @Lt Ax0 A E C F *)
assert (Cong B E b e) by (conclude lemma_congruencesymmetric).
(* Goal: @Lt Ax0 A E C F *)
assert (Cong A E C e) by (conclude cn_sumofparts).
(* Goal: @Lt Ax0 A E C F *)
assert (Cong e D e D) by (conclude cn_congruencereflexive).
(* Goal: @Lt Ax0 A E C F *)
assert (BetS e b C) by (conclude axiom_betweennesssymmetry).
(* Goal: @Lt Ax0 A E C F *)
assert (BetS C b F) by (conclude lemma_3_6b).
(* Goal: @Lt Ax0 A E C F *)
assert (~ BetS b F e).
(* Goal: not (not (@BetS Ax0 b e F)) *)
(* Goal: @Lt Ax0 A E C F *)
 {
(* Goal: not (not (@BetS Ax0 b e F)) *)
 intro.
(* Goal: False *)
 assert (Cong b F b F) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (Lt b F b e) by (conclude_def Lt ).
(* Goal: False *)
 assert (Cong F D F D) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (BetS b D F) by (conclude lemma_3_6a).
(* Goal: False *)
 assert (BetS F D b) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (Lt F D F b) by (conclude_def Lt ).
(* Goal: False *)
 assert (Cong F b b F) by (conclude cn_equalityreverse).
(* Goal: False *)
 assert (Lt F D b F) by (conclude lemma_lessthancongruence).
(* Goal: False *)
 assert (Cong F D D F) by (conclude cn_equalityreverse).
(* Goal: False *)
 assert (Lt D F b F) by (conclude lemma_lessthancongruence2).
(* Goal: False *)
 assert (Cong b e D F) by (conclude lemma_congruencetransitive).
(* Goal: False *)
 assert (Cong D F b e) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 assert (Lt b e b F) by (conclude lemma_lessthancongruence2).
 let Tf:=fresh in
 assert (Tf:exists q, (BetS b q F /\ Cong b q b e)) by (conclude_def Lt );destruct Tf as [q];spliter.
(* Goal: False *)
 assert (neq b q) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq b F) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Out b F q) by (conclude lemma_ray4).
(* Goal: False *)
 assert (Out b F e) by (conclude lemma_ray4).
(* Goal: False *)
 assert (eq q e) by (conclude lemma_layoffunique).
(* Goal: False *)
 assert (BetS b e F) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (BetS F e F) by (conclude lemma_3_6a).
(* Goal: False *)
 assert (~ BetS F e F) by (conclude axiom_betweennessidentity).
(* Goal: False *)
 contradict.
 }
(* Goal: @Lt Ax0 A E C F *)
assert (~ eq F e).
(* Goal: not (not (@BetS Ax0 b e F)) *)
(* Goal: @Lt Ax0 A E C F *)
 {
(* Goal: not (not (@BetS Ax0 b e F)) *)
 intro.
(* Goal: False *)
 assert (Cong b F B E) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (BetS b D F) by (conclude lemma_3_6a).
(* Goal: False *)
 assert (BetS F D b) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (Cong F D F D) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (Lt F D F b) by (conclude_def Lt ).
(* Goal: False *)
 assert (Cong F b b F) by (conclude cn_equalityreverse).
(* Goal: False *)
 assert (Lt F D b F) by (conclude lemma_lessthancongruence).
(* Goal: False *)
 assert (Cong D F B E) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 assert (Cong F D B E) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Lt B E b F) by (conclude lemma_lessthancongruence2).
(* Goal: False *)
 assert (Cong b F b e) by (conclude lemma_congruencetransitive).
(* Goal: False *)
 assert (Lt B E b e) by (conclude lemma_lessthancongruence).
(* Goal: False *)
 assert (Lt B E B E) by (conclude lemma_lessthancongruence).
(* Goal: False *)
 assert (~ Lt B E B E) by (conclude lemma_trichotomy2).
(* Goal: False *)
 contradict.
 }
(* Goal: @Lt Ax0 A E C F *)
assert (~ ~ BetS b e F).
(* Goal: not (not (@BetS Ax0 b e F)) *)
(* Goal: @Lt Ax0 A E C F *)
 {
(* Goal: not (not (@BetS Ax0 b e F)) *)
 intro.
(* Goal: False *)
 assert (eq F e) by (conclude lemma_outerconnectivity).
(* Goal: False *)
 contradict.
 }
(* Goal: @Lt Ax0 A E C F *)
assert (BetS C e F) by (conclude lemma_3_7a).
(* Goal: @Lt Ax0 A E C F *)
assert (Cong A E C e) by (conclude cn_sumofparts).
(* Goal: @Lt Ax0 A E C F *)
assert (Cong C e A E) by (conclude lemma_congruencesymmetric).
(* Goal: @Lt Ax0 A E C F *)
assert (Lt A E C F) by (conclude_def Lt ).
(* Goal: @Lt Ax0 A E C F *)
close.
Qed.

End Euclid.


