Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthantransitive.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_midpointunique : 
   forall A B C D, 
   Midpoint A B C -> Midpoint A D C ->
   eq B D.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @Midpoint Ax0 A B C) (_ : @Midpoint Ax0 A D C), @eq Ax0 B D *)
intros.
(* Goal: @eq Ax0 B D *)
assert ((BetS A B C /\ Cong A B B C)) by (conclude_def Midpoint ).
(* Goal: @eq Ax0 B D *)
assert ((BetS A D C /\ Cong A D D C)) by (conclude_def Midpoint ).
(* Goal: @eq Ax0 B D *)
assert (Cong A B A B) by (conclude cn_congruencereflexive).
(* Goal: @eq Ax0 B D *)
assert (~ BetS C D B).
(* Goal: not (@BetS Ax0 C B D) *)
(* Goal: @eq Ax0 B D *)
 {
(* Goal: not (@BetS Ax0 C B D) *)
 intro.
(* Goal: False *)
 assert (BetS B D C) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (BetS A B D) by (conclude axiom_innertransitivity).
(* Goal: False *)
 assert (Lt A B A D) by (conclude_def Lt ).
(* Goal: False *)
 assert (Cong A D C D) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Lt A B C D) by (conclude lemma_lessthancongruence).
(* Goal: False *)
 assert (BetS C D B) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (Cong C D C D) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (Lt C D C B) by (conclude_def Lt ).
(* Goal: False *)
 assert (Lt A B C B) by (conclude lemma_lessthantransitive).
(* Goal: False *)
 assert (Cong C B B C) by (conclude cn_equalityreverse).
(* Goal: False *)
 assert (Lt A B B C) by (conclude lemma_lessthancongruence).
(* Goal: False *)
 assert (Cong B C A B) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 assert (Lt A B A B) by (conclude lemma_lessthancongruence).
 let Tf:=fresh in
 assert (Tf:exists E, (BetS A E B /\ Cong A E A B)) by (conclude_def Lt );destruct Tf as [E];spliter.
(* Goal: False *)
 assert (~ Cong A E A B) by (conclude lemma_partnotequalwhole).
(* Goal: False *)
 contradict.
 }
(* Goal: @eq Ax0 B D *)
assert (~ BetS C B D).
(* Goal: not (@BetS Ax0 C B D) *)
(* Goal: @eq Ax0 B D *)
 {
(* Goal: not (@BetS Ax0 C B D) *)
 intro.
(* Goal: False *)
 assert (BetS D B C) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (BetS A D B) by (conclude axiom_innertransitivity).
(* Goal: False *)
 assert (Cong A D A D) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (Lt A D A B) by (conclude_def Lt ).
(* Goal: False *)
 assert (Cong A B C B) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Lt A D C B) by (conclude lemma_lessthancongruence).
(* Goal: False *)
 assert (BetS C B D) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (Cong C B C B) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (Lt C B C D) by (conclude_def Lt ).
(* Goal: False *)
 assert (Lt A D C D) by (conclude lemma_lessthantransitive).
(* Goal: False *)
 assert (Cong C D D C) by (conclude cn_equalityreverse).
(* Goal: False *)
 assert (Lt A D D C) by (conclude lemma_lessthancongruence).
(* Goal: False *)
 assert (Cong D C C D) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 assert (Lt A D C D) by (conclude lemma_lessthancongruence).
(* Goal: False *)
 assert (Cong D C A D) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 assert (Cong C D A D) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Lt A D A D) by (conclude lemma_lessthancongruence).
 let Tf:=fresh in
 assert (Tf:exists F, (BetS A F D /\ Cong A F A D)) by (conclude_def Lt );destruct Tf as [F];spliter.
(* Goal: False *)
 assert (~ Cong A F A D) by (conclude lemma_partnotequalwhole).
(* Goal: False *)
 contradict.
 }
(* Goal: @eq Ax0 B D *)
assert (BetS C D A) by (conclude axiom_betweennesssymmetry).
(* Goal: @eq Ax0 B D *)
assert (BetS C B A) by (conclude axiom_betweennesssymmetry).
(* Goal: @eq Ax0 B D *)
assert (eq B D) by (conclude axiom_connectivity).
(* Goal: @eq Ax0 B D *)
close.
Qed.

End Euclid.


