Require Export GeoCoq.Elements.OriginalProofs.lemma_betweennotequal.
Require Export GeoCoq.Elements.OriginalProofs.lemma_localextension.
Require Export GeoCoq.Elements.OriginalProofs.lemma_congruencesymmetric.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_betweennesspreserved : 
   forall A B C a b c, 
   Cong A B a b -> Cong A C a c -> Cong B C b c -> BetS A B C ->
   BetS a b c.
Proof.
(* Goal: forall (A B C a b c : @Point Ax0) (_ : @Cong Ax0 A B a b) (_ : @Cong Ax0 A C a c) (_ : @Cong Ax0 B C b c) (_ : @BetS Ax0 A B C), @BetS Ax0 a b c *)
intros.
(* Goal: @BetS Ax0 a b c *)
assert (neq A B) by (forward_using lemma_betweennotequal).
(* Goal: @BetS Ax0 a b c *)
assert (neq a b) by (conclude axiom_nocollapse).
(* Goal: @BetS Ax0 a b c *)
assert (neq B C) by (forward_using lemma_betweennotequal).
(* Goal: @BetS Ax0 a b c *)
assert (neq b c) by (conclude axiom_nocollapse).
let Tf:=fresh in
assert (Tf:exists d, (BetS a b d /\ Cong b d b c)) by (conclude lemma_localextension);destruct Tf as [d];spliter.
(* Goal: @BetS Ax0 a b c *)
assert (Cong b c b d) by (conclude lemma_congruencesymmetric).
(* Goal: @BetS Ax0 a b c *)
assert (Cong b c B C) by (conclude lemma_congruencesymmetric).
(* Goal: @BetS Ax0 a b c *)
assert (Cong b d B C) by (conclude cn_congruencetransitive).
(* Goal: @BetS Ax0 a b c *)
assert (Cong B C b d) by (conclude lemma_congruencesymmetric).
(* Goal: @BetS Ax0 a b c *)
assert (Cong C C c d) by (conclude axiom_5_line).
(* Goal: @BetS Ax0 a b c *)
assert (Cong c d C C) by (conclude lemma_congruencesymmetric).
(* Goal: @BetS Ax0 a b c *)
assert (~ neq c d).
(* Goal: not (@neq Ax0 c d) *)
(* Goal: @BetS Ax0 a b c *)
 {
(* Goal: not (@neq Ax0 c d) *)
 intro.
(* Goal: False *)
 assert (neq C C) by (conclude axiom_nocollapse).
(* Goal: False *)
 assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: False *)
 contradict.
 }
(* Goal: @BetS Ax0 a b c *)
assert (BetS a b c) by (conclude cn_equalitysub).
(* Goal: @BetS Ax0 a b c *)
close.
Qed.

End Euclid.


