Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthantransitive.
Require Export GeoCoq.Elements.OriginalProofs.lemma_trichotomy2.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_subtractequals : 
   forall A B C D E, 
   BetS A B C -> BetS A D E -> Cong B C D E -> BetS A C E ->
   BetS A B D.
Proof.
(* Goal: forall (A B C D E : @Point Ax) (_ : @BetS Ax A B C) (_ : @BetS Ax A D E) (_ : @Cong Ax B C D E) (_ : @BetS Ax A C E), @BetS Ax A B D *)
intros.
(* Goal: @BetS Ax A B D *)
assert (~ BetS A D B).
(* Goal: not (not (@BetS Ax A B D)) *)
(* Goal: @BetS Ax A B D *)
 {
(* Goal: not (not (@BetS Ax A B D)) *)
 intro.
(* Goal: False *)
 assert (BetS A D C) by (conclude lemma_3_6b).
(* Goal: False *)
 assert (BetS A D C) by (conclude lemma_3_6b).
(* Goal: False *)
 assert (BetS B C E) by (conclude lemma_3_6a).
(* Goal: False *)
 assert (Cong B C B C) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (Lt B C B E) by (conclude_def Lt ).
(* Goal: False *)
 assert (Cong B E E B) by (conclude cn_equalityreverse).
(* Goal: False *)
 assert (Lt B C E B) by (conclude lemma_lessthancongruence).
(* Goal: False *)
 assert (BetS D C E) by (conclude lemma_3_6a).
(* Goal: False *)
 assert (BetS D B C) by (conclude lemma_3_6a).
(* Goal: False *)
 assert (BetS D B E) by (conclude lemma_3_6b).
(* Goal: False *)
 assert (BetS E B D) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (Cong E B E B) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (Lt E B E D) by (conclude_def Lt ).
(* Goal: False *)
 assert (Cong E D D E) by (conclude cn_equalityreverse).
(* Goal: False *)
 assert (Lt E B D E) by (conclude lemma_lessthancongruence).
(* Goal: False *)
 assert (Lt B C D E) by (conclude lemma_lessthantransitive).
(* Goal: False *)
 assert (Cong D E B C) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 assert (Lt B C B C) by (conclude lemma_lessthancongruence).
(* Goal: False *)
 assert (~ Lt B C B C) by (conclude lemma_trichotomy2).
(* Goal: False *)
 contradict.
 }
(* Goal: @BetS Ax A B D *)
assert (~ ~ BetS A B D).
(* Goal: not (not (@BetS Ax A B D)) *)
(* Goal: @BetS Ax A B D *)
 {
(* Goal: not (not (@BetS Ax A B D)) *)
 intro.
(* Goal: False *)
 assert (BetS A B E) by (conclude lemma_3_6b).
(* Goal: False *)
 assert (eq B D) by (conclude axiom_connectivity).
(* Goal: False *)
 assert (Cong A B A B) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (Cong A B A D) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (Cong A C A E) by (conclude cn_sumofparts).
(* Goal: False *)
 assert (BetS A B E) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (neq A B) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Out A B E) by (conclude lemma_ray4).
(* Goal: False *)
 assert (Out A B C) by (conclude lemma_ray4).
(* Goal: False *)
 assert (eq C E) by (conclude lemma_layoffunique).
(* Goal: False *)
 assert (neq C E) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 contradict.
 }
(* Goal: @BetS Ax A B D *)
close.
Qed.

End Euclid.


