Require Export GeoCoq.Elements.OriginalProofs.lemma_droppedperpendicularunique.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.


Lemma lemma_8_7 : 
   forall A B C, 
   Per C B A ->
   ~ Per A C B.
Proof.
(* Goal: forall (A B C : @Point Ax0) (_ : @Per Ax0 C B A), not (@Per Ax0 A C B) *)
intros.
(* Goal: not (@Per Ax0 A C B) *)
assert (neq B A) by (conclude_def Per ).
(* Goal: not (@Per Ax0 A C B) *)
assert (Per A B C) by (conclude lemma_8_2).
(* Goal: not (@Per Ax0 A C B) *)
assert (neq B C) by (conclude_def Per ).
(* Goal: not (@Per Ax0 A C B) *)
assert (neq C B) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists E, (BetS B C E /\ Cong C E C B)) by (conclude lemma_extension);destruct Tf as [E];spliter.
(* Goal: not (@Per Ax0 A C B) *)
assert (Col B C E) by (conclude_def Col ).
(* Goal: not (@Per Ax0 A C B) *)
assert (Col E C B) by (forward_using lemma_collinearorder).
(* Goal: not (@Per Ax0 A C B) *)
assert (Per A B C) by (conclude lemma_8_2).
(* Goal: not (@Per Ax0 A C B) *)
assert (Out B C E) by (conclude lemma_ray4).
(* Goal: not (@Per Ax0 A C B) *)
assert (Per A B E) by (conclude lemma_8_3).
(* Goal: not (@Per Ax0 A C B) *)
assert (Per E B A) by (conclude lemma_8_2).
(* Goal: not (@Per Ax0 A C B) *)
assert (~ Per A C B).
(* Goal: not (@Per Ax0 A C B) *)
(* Goal: not (@Per Ax0 A C B) *)
 {
(* Goal: not (@Per Ax0 A C B) *)
 intro.
(* Goal: False *)
 assert (Per B C A) by (conclude lemma_8_2).
 let Tf:=fresh in
 assert (Tf:exists F, (BetS B C F /\ Cong B C F C /\ Cong B A F A /\ neq C A)) by (conclude_def Per );destruct Tf as [F];spliter.
(* Goal: False *)
 assert (Cong F C B C) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 assert (Cong C F B C) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Cong C E B C) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Cong B C C E) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 assert (Cong C F C E) by (conclude lemma_congruencetransitive).
(* Goal: False *)
 assert (eq F E) by (conclude lemma_extensionunique).
(* Goal: False *)
 assert (BetS E C B) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (Cong F A B A) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 assert (Cong E A B A) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (Cong E C B C) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert (Per E C A) by (conclude_def Per ).
(* Goal: False *)
 assert (eq C B) by (conclude lemma_droppedperpendicularunique).
(* Goal: False *)
 contradict.
 }
(* Goal: not (@Per Ax0 A C B) *)
close.
Qed.

End Euclid.


