# 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.

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.