Library GeoCoq.Elements.OriginalProofs.proposition_23

Require Export GeoCoq.Elements.OriginalProofs.proposition_20.
Require Export GeoCoq.Elements.OriginalProofs.lemma_TGsymmetric.
Require Export GeoCoq.Elements.OriginalProofs.lemma_TGflip.
Require Export GeoCoq.Elements.OriginalProofs.proposition_22.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_23 :
   ∀ A B C D E,
   neq A B → nCol D C E →
   ∃ X Y, Out A B Y ∧ CongA X A Y D C E.
Proof.
intros.
assert (¬ Col D E C).
 {
 intro.
 assert (Col D C E) by (forward_using lemma_collinearorder).
 contradict.
 }
assert (¬ Col E C D).
 {
 intro.
 assert (Col D C E) by (forward_using lemma_collinearorder).
 contradict.
 }
assert (¬ Col C E D).
 {
 intro.
 assert (Col D C E) by (forward_using lemma_collinearorder).
 contradict.
 }
assert (Triangle D C E) by (conclude_def Triangle ).
assert (Triangle C E D) by (conclude_def Triangle ).
assert (Triangle E C D) by (conclude_def Triangle ).
assert (TG C D D E C E) by (conclude proposition_20).
assert (TG C E E D C D) by (conclude proposition_20).
assert (TG E C C D E D) by (conclude proposition_20).
assert (TG C D E C E D) by (conclude lemma_TGsymmetric).
assert (TG C D D E E C) by (forward_using lemma_TGflip).
assert (TG D E C D E C) by (conclude lemma_TGsymmetric).
assert (TG E D C D E C) by (forward_using lemma_TGflip).
assert (TG C D E D E C) by (conclude lemma_TGsymmetric).
assert (TG E C E D C D) by (forward_using lemma_TGflip).
let Tf:=fresh in
assert (Tf:∃ G F, (Cong A G E C ∧ Cong A F C D ∧ Cong G F E D ∧ Out A B G ∧ Triangle A G F))
 by (conclude proposition_22);destruct Tf as [G[F]];spliter.
assert (Cong A G C E) by (forward_using lemma_congruenceflip).
assert (Cong F G D E) by (forward_using lemma_congruenceflip).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (eq G G) by (conclude cn_equalityreflexive).
assert (¬ eq C E).
 {
 intro.
 assert (Col D C E) by (conclude_def Col ).
 contradict.
 }
assert (¬ eq C D).
 {
 intro.
 assert (Col C D E) by (conclude_def Col ).
 assert (Col D C E) by (forward_using lemma_collinearorder).
 contradict.
 }
assert (Out C E E) by (conclude lemma_ray4).
assert (Out C D D) by (conclude lemma_ray4).
assert (¬ Col F A G).
 {
 intro.
 assert (Col A G F) by (forward_using lemma_collinearorder).
 assert (nCol A G F) by (conclude_def Triangle ).
 contradict.
 }
assert (¬ eq A F).
 {
 intro.
 assert (Col A F G) by (conclude_def Col ).
 assert (Col F A G) by (forward_using lemma_collinearorder).
 contradict.
 }
assert (Out A F F) by (conclude lemma_ray4).
assert (¬ eq A G).
 {
 intro.
 assert (Col A G F) by (conclude_def Col ).
 assert (Col F A G) by (forward_using lemma_collinearorder).
 contradict.
 }
assert (Out A G G) by (conclude lemma_ray4).
assert (CongA F A G D C E) by (conclude_def CongA ).
close.
Qed.

End Euclid.