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 : 
   forall A B C E, 
   Per A B C -> Per A B E -> OS C E A B ->
   Out B C E.
Proof.
(* Goal: forall (A B C E : @Point Ax0) (_ : @Per Ax0 A B C) (_ : @Per Ax0 A B E) (_ : @OS Ax0 C E A B), @Out Ax0 B C E *)
intros.
let Tf:=fresh in
assert (Tf:exists 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.
(* Goal: @Out Ax0 B C E *)
assert (neq B E) by (conclude_def Per ).
rename_H H;let Tf:=fresh in
assert (Tf:exists H, (Out B E H /\ Cong B H B C)) by (conclude lemma_layoff);destruct Tf as [H];spliter.
(* Goal: @Out Ax0 B C E *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @Out Ax0 B C E *)
assert (Col A B B) by (conclude_def Col ).
(* Goal: @Out Ax0 B C E *)
assert (OS C H A B) by (conclude lemma_sameside2).
(* Goal: @Out Ax0 B C E *)
assert (Per A B H) by (conclude lemma_8_3).
(* Goal: @Out Ax0 B C E *)
assert (Cong B C B H) by (conclude lemma_congruencesymmetric).
(* Goal: @Out Ax0 B C E *)
assert (Cong A C A H) by (conclude lemma_10_12).
(* Goal: @Out Ax0 B C E *)
assert (Cong C A H A) by (forward_using lemma_congruenceflip).
(* Goal: @Out Ax0 B C E *)
assert (Cong C B H B) by (forward_using lemma_congruenceflip).
(* Goal: @Out Ax0 B C E *)
assert (~ eq A B).
(* Goal: not (@eq Ax0 A B) *)
(* Goal: @Out Ax0 B C E *)
 {
(* Goal: not (@eq Ax0 A B) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 assert (nCol A B C) by (conclude lemma_rightangleNC).
(* Goal: False *)
 contradict.
 }
(* Goal: @Out Ax0 B C E *)
assert (eq C H) by (conclude proposition_07).
(* Goal: @Out Ax0 B C E *)
assert (Out B E C) by (conclude cn_equalitysub).
(* Goal: @Out Ax0 B C E *)
assert (Out B C E) by (conclude lemma_ray5).
(* Goal: @Out Ax0 B C E *)
close.
Qed.

End Euclid.


