Library GeoCoq.Elements.OriginalProofs.proposition_12

Require Export GeoCoq.Elements.OriginalProofs.proposition_10.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_12 :
   ∀ A B C,
   nCol A B C →
   ∃ X, Perp_at C X A B X.
Proof.
intros.
assert (¬ eq B C).
 {
 intro.
 assert (Col A B C) by (conclude_def Col ).
 contradict.
 }
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert (¬ eq A B).
 {
 intro.
 assert (Col A B C) by (conclude_def Col ).
 contradict.
 }
let Tf:=fresh in
assert (Tf:∃ E, (BetS C B E ∧ Cong B E C B)) by (conclude postulate_extension);destruct Tf as [E];spliter.
assert (neq B E) by (forward_using lemma_betweennotequal).
assert (neq C E) by (forward_using lemma_betweennotequal).
assert (neq E C) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ F, (BetS E C F ∧ Cong C F E C)) by (conclude postulate_extension);destruct Tf as [F];spliter.
assert (Cong E C C E) by (conclude cn_equalityreverse).
assert (Cong C E C E) by (conclude cn_congruencereflexive).
assert (Cong C F C E) by (conclude lemma_congruencetransitive).
assert (BetS E B C) by (conclude axiom_betweennesssymmetry).
assert (BetS E B F) by (conclude lemma_3_6b).
let Tf:=fresh in
assert (Tf:∃ K, CI K C C E) by (conclude circle);destruct Tf as [K];spliter.
assert (Cong C B C B) by (conclude cn_congruencereflexive).
assert (Lt C B C E) by (conclude_def Lt ).
assert ((CI K C C E ∧ InCirc B K)) by (conclude inside).
let Tf:=fresh in
assert (Tf:∃ P Q, (Col A B P ∧ Col A B Q ∧ OnCirc P K ∧ OnCirc Q K ∧ BetS P B Q)) by (conclude postulate_line_circle);destruct Tf as [P[Q]];spliter.
assert (Cong C P C E) by (conclude on).
assert (Cong C Q C E) by (conclude on).
assert (Cong C E C Q) by (conclude lemma_congruencesymmetric).
assert (Cong C P C Q) by (conclude lemma_congruencetransitive).
assert (Cong P C Q C) by (forward_using lemma_congruenceflip).
assert (neq P Q) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:∃ M, (BetS P M Q ∧ Cong M P M Q)) by (conclude proposition_10);destruct Tf as [M];spliter.
assert (Cong P M Q M) by (forward_using lemma_congruenceflip).
assert (Col P M Q) by (conclude_def Col ).
assert (neq P Q) by (forward_using lemma_betweennotequal).
assert (Col P Q M) by (forward_using lemma_collinearorder).
assert (Col P B Q) by (conclude_def Col ).
assert (Col P Q B) by (forward_using lemma_collinearorder).
assert (Col P Q M) by (forward_using lemma_collinearorder).
assert (Col Q B M) by (conclude lemma_collinear4).
assert (Col Q B A) by (forward_using lemma_collinearorder).
assert (neq B Q) by (forward_using lemma_betweennotequal).
assert (neq Q B) by (conclude lemma_inequalitysymmetric).
assert (Col B M A) by (conclude lemma_collinear4).
assert (Col A B M) by (forward_using lemma_collinearorder).
assert (¬ eq M C).
 {
 intro.
 assert (Col A B C) by (conclude cn_equalitysub).
 contradict.
 }
assert (Per P M C) by (conclude_def Per ).
assert (eq M M) by (conclude cn_equalityreflexive).
assert (Col C M M) by (conclude_def Col ).
assert (Col P Q M) by (conclude_def Col ).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col C M C) by (conclude_def Col ).
assert (Perp_at C M A B M) by (conclude_def Perp_at ).
close.
Qed.

End Euclid.