Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearright.
Require Export GeoCoq.Elements.OriginalProofs.lemma_rightreverse.
Require Export GeoCoq.Elements.OriginalProofs.lemma_altitudebisectsbase.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_droppedperpendicularunique : 
   forall A J M P, 
   Per A M P -> Per A J P -> Col A M J ->
   eq M J.
Proof.
(* Goal: forall (A J M P : @Point Ax0) (_ : @Per Ax0 A M P) (_ : @Per Ax0 A J P) (_ : @Col Ax0 A M J), @eq Ax0 M J *)
intros.
(* Goal: @eq Ax0 M J *)
assert (~ neq M J).
(* Goal: not (@neq Ax0 M J) *)
(* Goal: @eq Ax0 M J *)
 {
(* Goal: not (@neq Ax0 M J) *)
 intro.
(* Goal: False *)
 assert (neq J M) by (conclude lemma_inequalitysymmetric).
 let Tf:=fresh in
 assert (Tf:exists E, (BetS M J E /\ Cong J E M J)) by (conclude lemma_extension);destruct Tf as [E];spliter.
(* Goal: False *)
 assert (neq M E) by (forward_using lemma_betweennotequal).
 let Tf:=fresh in
 assert (Tf:exists F, (BetS J M F /\ Cong M F M E)) by (conclude lemma_extension);destruct Tf as [F];spliter.
(* Goal: False *)
 assert (BetS E J M) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (BetS E J F) by (conclude lemma_3_7b).
(* Goal: False *)
 assert (BetS F J E) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (BetS E M F) by (conclude lemma_3_7a).
(* Goal: False *)
 assert (neq J F) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq F J) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col J M F) by (conclude_def Col ).
(* Goal: False *)
 assert (Col M J F) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col M J A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq J M) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq M J) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col J F A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A J F) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Per F J P) by (conclude lemma_collinearright).
(* Goal: False *)
 assert (Col J M F) by (conclude_def Col ).
(* Goal: False *)
 assert (Col J M A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col M F A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A M F) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq M F) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq F M) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Per F M P) by (conclude lemma_collinearright).
(* Goal: False *)
 assert (Cong F M M E) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Per F M P) by (conclude lemma_collinearright).
(* Goal: False *)
 assert (BetS F M E) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (Cong F P E P) by (conclude lemma_rightreverse).
(* Goal: False *)
 assert (Midpoint F J E) by (conclude lemma_altitudebisectsbase).
(* Goal: False *)
 assert (BetS F M E) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (Cong F M M E) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Midpoint F M E) by (conclude_def Midpoint ).
(* Goal: False *)
 assert (eq J M) by (conclude lemma_midpointunique).
(* Goal: False *)
 contradict.
 }
(* Goal: @eq Ax0 M J *)
close.
Qed.

End Euclid.


