# Library GeoCoq.Elements.OriginalProofs.lemma_erectedperpendicularunique

Require Export GeoCoq.Elements.OriginalProofs.lemma_sameside2.

Require Export GeoCoq.Elements.OriginalProofs.lemma_10_12.

Require Export GeoCoq.Elements.OriginalProofs.proposition_07.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_erectedperpendicularunique :

∀ A B C E,

Per A B C → Per A B E → OS C E A B →

Out B C E.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ D, (BetS A B D ∧ Cong A B D B ∧ Cong A C D C ∧ neq B C)) by (conclude_def Per );destruct Tf as [D];spliter.

assert (neq B E) by (conclude_def Per ).

rename_H H;let Tf:=fresh in

assert (Tf:∃ H, (Out B E H ∧ Cong B H B C)) by (conclude lemma_layoff);destruct Tf as [H];spliter.

assert (eq B B) by (conclude cn_equalityreflexive).

assert (Col A B B) by (conclude_def Col ).

assert (OS C H A B) by (conclude lemma_sameside2).

assert (Per A B H) by (conclude lemma_8_3).

assert (Cong B C B H) by (conclude lemma_congruencesymmetric).

assert (Cong A C A H) by (conclude lemma_10_12).

assert (Cong C A H A) by (forward_using lemma_congruenceflip).

assert (Cong C B H B) by (forward_using lemma_congruenceflip).

assert (¬ eq A B).

{

intro.

assert (Col A B C) by (conclude_def Col ).

assert (nCol A B C) by (conclude lemma_rightangleNC).

contradict.

}

assert (eq C H) by (conclude proposition_07).

assert (Out B E C) by (conclude cn_equalitysub).

assert (Out B C E) by (conclude lemma_ray5).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_10_12.

Require Export GeoCoq.Elements.OriginalProofs.proposition_07.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_erectedperpendicularunique :

∀ A B C E,

Per A B C → Per A B E → OS C E A B →

Out B C E.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ D, (BetS A B D ∧ Cong A B D B ∧ Cong A C D C ∧ neq B C)) by (conclude_def Per );destruct Tf as [D];spliter.

assert (neq B E) by (conclude_def Per ).

rename_H H;let Tf:=fresh in

assert (Tf:∃ H, (Out B E H ∧ Cong B H B C)) by (conclude lemma_layoff);destruct Tf as [H];spliter.

assert (eq B B) by (conclude cn_equalityreflexive).

assert (Col A B B) by (conclude_def Col ).

assert (OS C H A B) by (conclude lemma_sameside2).

assert (Per A B H) by (conclude lemma_8_3).

assert (Cong B C B H) by (conclude lemma_congruencesymmetric).

assert (Cong A C A H) by (conclude lemma_10_12).

assert (Cong C A H A) by (forward_using lemma_congruenceflip).

assert (Cong C B H B) by (forward_using lemma_congruenceflip).

assert (¬ eq A B).

{

intro.

assert (Col A B C) by (conclude_def Col ).

assert (nCol A B C) by (conclude lemma_rightangleNC).

contradict.

}

assert (eq C H) by (conclude proposition_07).

assert (Out B E C) by (conclude cn_equalitysub).

assert (Out B C E) by (conclude lemma_ray5).

close.

Qed.

End Euclid.