Library GeoCoq.Elements.OriginalProofs.lemma_midpointunique

Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthantransitive.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_midpointunique :
   ∀ A B C D,
   Midpoint A B C → Midpoint A D C →
   eq B D.
Proof.
intros.
assert ((BetS A B C ∧ Cong A B B C)) by (conclude_def Midpoint ).
assert ((BetS A D C ∧ Cong A D D C)) by (conclude_def Midpoint ).
assert (Cong A B A B) by (conclude cn_congruencereflexive).
assert (¬ BetS C D B).
 {
 intro.
 assert (BetS B D C) by (conclude axiom_betweennesssymmetry).
 assert (BetS A B D) by (conclude axiom_innertransitivity).
 assert (Lt A B A D) by (conclude_def Lt ).
 assert (Cong A D C D) by (forward_using lemma_congruenceflip).
 assert (Lt A B C D) by (conclude lemma_lessthancongruence).
 assert (BetS C D B) by (conclude axiom_betweennesssymmetry).
 assert (Cong C D C D) by (conclude cn_congruencereflexive).
 assert (Lt C D C B) by (conclude_def Lt ).
 assert (Lt A B C B) by (conclude lemma_lessthantransitive).
 assert (Cong C B B C) by (conclude cn_equalityreverse).
 assert (Lt A B B C) by (conclude lemma_lessthancongruence).
 assert (Cong B C A B) by (conclude lemma_congruencesymmetric).
 assert (Lt A B A B) by (conclude lemma_lessthancongruence).
 let Tf:=fresh in
 assert (Tf:∃ E, (BetS A E B ∧ Cong A E A B)) by (conclude_def Lt );destruct Tf as [E];spliter.
 assert (¬ Cong A E A B) by (conclude lemma_partnotequalwhole).
 contradict.
 }
assert (¬ BetS C B D).
 {
 intro.
 assert (BetS D B C) by (conclude axiom_betweennesssymmetry).
 assert (BetS A D B) by (conclude axiom_innertransitivity).
 assert (Cong A D A D) by (conclude cn_congruencereflexive).
 assert (Lt A D A B) by (conclude_def Lt ).
 assert (Cong A B C B) by (forward_using lemma_congruenceflip).
 assert (Lt A D C B) by (conclude lemma_lessthancongruence).
 assert (BetS C B D) by (conclude axiom_betweennesssymmetry).
 assert (Cong C B C B) by (conclude cn_congruencereflexive).
 assert (Lt C B C D) by (conclude_def Lt ).
 assert (Lt A D C D) by (conclude lemma_lessthantransitive).
 assert (Cong C D D C) by (conclude cn_equalityreverse).
 assert (Lt A D D C) by (conclude lemma_lessthancongruence).
 assert (Cong D C C D) by (conclude lemma_congruencesymmetric).
 assert (Lt A D C D) by (conclude lemma_lessthancongruence).
 assert (Cong D C A D) by (conclude lemma_congruencesymmetric).
 assert (Cong C D A D) by (forward_using lemma_congruenceflip).
 assert (Lt A D A D) by (conclude lemma_lessthancongruence).
 let Tf:=fresh in
 assert (Tf:∃ F, (BetS A F D ∧ Cong A F A D)) by (conclude_def Lt );destruct Tf as [F];spliter.
 assert (¬ Cong A F A D) by (conclude lemma_partnotequalwhole).
 contradict.
 }
assert (BetS C D A) by (conclude axiom_betweennesssymmetry).
assert (BetS C B A) by (conclude axiom_betweennesssymmetry).
assert (eq B D) by (conclude axiom_connectivity).
close.
Qed.

End Euclid.