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

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_extensionunique : 
   forall A B E F, 
   BetS A B E -> BetS A B F -> Cong B E B F ->
   eq E F.
Proof.
(* Goal: forall (A B E F : @Point Ax) (_ : @BetS Ax A B E) (_ : @BetS Ax A B F) (_ : @Cong Ax B E B F), @eq Ax E F *)
intros.
(* Goal: @eq Ax E F *)
assert (Cong B E B E) by (conclude cn_congruencereflexive).
(* Goal: @eq Ax E F *)
assert (Cong B F B E) by (conclude lemma_congruencesymmetric).
(* Goal: @eq Ax E F *)
assert (Cong A E A E) by (conclude cn_congruencereflexive).
(* Goal: @eq Ax E F *)
assert (Cong A B A B) by (conclude cn_congruencereflexive).
(* Goal: @eq Ax E F *)
assert (Cong B E B F) by (conclude lemma_congruencesymmetric).
(* Goal: @eq Ax E F *)
assert (Cong E E E F) by (conclude axiom_5_line).
(* Goal: @eq Ax E F *)
assert (Cong E F E E) by (conclude lemma_congruencesymmetric).
(* Goal: @eq Ax E F *)
assert (~ neq E F).
(* Goal: not (@neq Ax E F) *)
(* Goal: @eq Ax E F *)
 {
(* Goal: not (@neq Ax E F) *)
 intro.
(* Goal: False *)
 assert (neq E E) by (conclude axiom_nocollapse).
(* Goal: False *)
 assert (eq E E) by (conclude cn_equalityreflexive).
(* Goal: False *)
 contradict.
 }
(* Goal: @eq Ax E F *)
close.
Qed.

End Euclid.


