Require Export GeoCoq.Elements.OriginalProofs.proposition_10.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_12 : 
   forall A B C, 
   nCol A B C ->
   exists X, Perp_at C X A B X.
Proof.
(* Goal: forall (A B C : @Point Ax0) (_ : @nCol Ax0 A B C), @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
intros.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (~ eq B C).
(* Goal: not (@eq Ax0 M C) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
 {
(* Goal: not (@eq Ax0 M C) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (neq C B) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (~ eq A B).
(* Goal: not (@eq Ax0 M C) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
 {
(* Goal: not (@eq Ax0 M C) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists E, (BetS C B E /\ Cong B E C B)) by (conclude lemma_extension);destruct Tf as [E];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (neq C E) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (neq E C) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists F, (BetS E C F /\ Cong C F E C)) by (conclude lemma_extension);destruct Tf as [F];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Cong E C C E) by (conclude cn_equalityreverse).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Cong C E C E) by (conclude cn_congruencereflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Cong C F C E) by (conclude lemma_congruencetransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (BetS E B C) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (BetS E B F) by (conclude lemma_3_6b).
let Tf:=fresh in
assert (Tf:exists K, CI K C C E) by (conclude postulate_Euclid3);destruct Tf as [K];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Cong C E C E) by (conclude cn_congruencereflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Cong C B C B) by (conclude cn_congruencereflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (InCirc B K) by (conclude_def InCirc ).
let Tf:=fresh in
assert (Tf:exists P Q, (Col A B P /\ BetS A B Q /\ OnCirc P K /\ OnCirc Q K /\ BetS P B Q)) by (conclude postulate_line_circle);destruct Tf as [P[Q]];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Col A B Q) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Cong C P C E) by (conclude axiom_circle_center_radius).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Cong C Q C E) by (conclude axiom_circle_center_radius).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Cong C E C Q) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Cong C P C Q) by (conclude lemma_congruencetransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Cong P C Q C) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (neq P Q) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists M, (BetS P M Q /\ Cong M P M Q)) by (conclude proposition_10);destruct Tf as [M];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Cong P M Q M) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Col P M Q) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Col P B Q) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Col P Q B) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Col P Q M) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Col Q B M) by (conclude lemma_collinear4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Col Q B A) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (neq B Q) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (neq Q B) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Col B M A) by (conclude lemma_collinear4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Col A B M) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (~ eq M C).
(* Goal: not (@eq Ax0 M C) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
 {
(* Goal: not (@eq Ax0 M C) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude cn_equalitysub).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Per P M C) by (conclude_def Per ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (eq M M) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Col C M M) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
assert (Perp_at C M A B M) by (conclude_def Perp_at ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @Perp_at Ax0 C X A B X) *)
close.
Qed.

End Euclid.


