# Library GeoCoq.Elements.OriginalProofs.lemma_droppedperpendicularunique

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}.

Lemma lemma_droppedperpendicularunique :

∀ A J M P,

Per A M P → Per A J P → Col A M J →

eq M J.

Proof.

intros.

assert (Per P M A) by (conclude lemma_8_2).

let Tf:=fresh in

assert (Tf:∃ Q, (BetS P M Q ∧ Cong P M Q M ∧ Cong P A Q A ∧ neq M A)) by (conclude_def Per );destruct Tf as [Q];spliter.

assert (¬ neq M J).

{

intro.

assert (neq J M) by (conclude lemma_inequalitysymmetric).

let Tf:=fresh in

assert (Tf:∃ E, (BetS M J E ∧ Cong J E M J)) by (conclude postulate_extension);destruct Tf as [E];spliter.

assert (neq M E) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

assert (Tf:∃ F, (BetS J M F ∧ Cong M F M E)) by (conclude postulate_extension);destruct Tf as [F];spliter.

assert (BetS E J M) by (conclude axiom_betweennesssymmetry).

assert (BetS E J F) by (conclude lemma_3_7b).

assert (BetS F J E) by (conclude axiom_betweennesssymmetry).

assert (BetS E M F) by (conclude lemma_3_7a).

assert (neq J F) by (forward_using lemma_betweennotequal).

assert (neq F J) by (conclude lemma_inequalitysymmetric).

assert (Col J M F) by (conclude_def Col ).

assert (Col M J F) by (forward_using lemma_collinearorder).

assert (Col M J A) by (forward_using lemma_collinearorder).

assert (neq J M) by (forward_using lemma_betweennotequal).

assert (neq M J) by (conclude lemma_inequalitysymmetric).

assert (Col J F A) by (conclude lemma_collinear4).

assert (Col A J F) by (forward_using lemma_collinearorder).

assert (Per F J P) by (conclude lemma_collinearright).

assert (Col J M F) by (conclude_def Col ).

assert (Col J M A) by (forward_using lemma_collinearorder).

assert (Col M F A) by (conclude lemma_collinear4).

assert (Col A M F) by (forward_using lemma_collinearorder).

assert (neq M F) by (forward_using lemma_betweennotequal).

assert (neq F M) by (conclude lemma_inequalitysymmetric).

assert (Per F M P) by (conclude lemma_collinearright).

assert (Cong F M M E) by (forward_using lemma_congruenceflip).

assert (Per F M P) by (conclude lemma_collinearright).

assert (BetS F M E) by (conclude axiom_betweennesssymmetry).

assert (Cong F P E P) by (conclude lemma_rightreverse).

assert (Midpoint F J E) by (conclude lemma_altitudebisectsbase).

assert (BetS F M E) by (conclude axiom_betweennesssymmetry).

assert (Cong F M M E) by (forward_using lemma_congruenceflip).

assert (Midpoint F M E) by (conclude_def Midpoint ).

assert (eq J M) by (conclude lemma_midpointunique).

contradict.

}

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_rightreverse.

Require Export GeoCoq.Elements.OriginalProofs.lemma_altitudebisectsbase.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_droppedperpendicularunique :

∀ A J M P,

Per A M P → Per A J P → Col A M J →

eq M J.

Proof.

intros.

assert (Per P M A) by (conclude lemma_8_2).

let Tf:=fresh in

assert (Tf:∃ Q, (BetS P M Q ∧ Cong P M Q M ∧ Cong P A Q A ∧ neq M A)) by (conclude_def Per );destruct Tf as [Q];spliter.

assert (¬ neq M J).

{

intro.

assert (neq J M) by (conclude lemma_inequalitysymmetric).

let Tf:=fresh in

assert (Tf:∃ E, (BetS M J E ∧ Cong J E M J)) by (conclude postulate_extension);destruct Tf as [E];spliter.

assert (neq M E) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

assert (Tf:∃ F, (BetS J M F ∧ Cong M F M E)) by (conclude postulate_extension);destruct Tf as [F];spliter.

assert (BetS E J M) by (conclude axiom_betweennesssymmetry).

assert (BetS E J F) by (conclude lemma_3_7b).

assert (BetS F J E) by (conclude axiom_betweennesssymmetry).

assert (BetS E M F) by (conclude lemma_3_7a).

assert (neq J F) by (forward_using lemma_betweennotequal).

assert (neq F J) by (conclude lemma_inequalitysymmetric).

assert (Col J M F) by (conclude_def Col ).

assert (Col M J F) by (forward_using lemma_collinearorder).

assert (Col M J A) by (forward_using lemma_collinearorder).

assert (neq J M) by (forward_using lemma_betweennotequal).

assert (neq M J) by (conclude lemma_inequalitysymmetric).

assert (Col J F A) by (conclude lemma_collinear4).

assert (Col A J F) by (forward_using lemma_collinearorder).

assert (Per F J P) by (conclude lemma_collinearright).

assert (Col J M F) by (conclude_def Col ).

assert (Col J M A) by (forward_using lemma_collinearorder).

assert (Col M F A) by (conclude lemma_collinear4).

assert (Col A M F) by (forward_using lemma_collinearorder).

assert (neq M F) by (forward_using lemma_betweennotequal).

assert (neq F M) by (conclude lemma_inequalitysymmetric).

assert (Per F M P) by (conclude lemma_collinearright).

assert (Cong F M M E) by (forward_using lemma_congruenceflip).

assert (Per F M P) by (conclude lemma_collinearright).

assert (BetS F M E) by (conclude axiom_betweennesssymmetry).

assert (Cong F P E P) by (conclude lemma_rightreverse).

assert (Midpoint F J E) by (conclude lemma_altitudebisectsbase).

assert (BetS F M E) by (conclude axiom_betweennesssymmetry).

assert (Cong F M M E) by (forward_using lemma_congruenceflip).

assert (Midpoint F M E) by (conclude_def Midpoint ).

assert (eq J M) by (conclude lemma_midpointunique).

contradict.

}

close.

Qed.

End Euclid.