# Library GeoCoq.Elements.OriginalProofs.lemma_twoperpsparallel

Require Export GeoCoq.Elements.OriginalProofs.lemma_Euclid4.

Require Export GeoCoq.Elements.OriginalProofs.proposition_28C.

Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelflip.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_twoperpsparallel :

∀ A B C D,

Per A B C → Per B C D → OS A D B C →

Par A B C D.

Proof.

intros.

assert (nCol A B C) by (conclude lemma_rightangleNC).

assert (neq B C) by (forward_using lemma_NCdistinct).

let Tf:=fresh in

assert (Tf:∃ E, (BetS B C E ∧ Cong C E B C)) by (conclude postulate_extension);destruct Tf as [E];spliter.

assert (Col B C E) by (conclude_def Col ).

assert (neq C E) by (forward_using lemma_betweennotequal).

assert (neq E C) by (conclude lemma_inequalitysymmetric).

assert (Col C B E) by (forward_using lemma_collinearorder).

assert (Per E C D) by (conclude lemma_collinearright).

assert (Per D C E) by (conclude lemma_8_2).

assert (eq D D) by (conclude cn_equalityreflexive).

assert (nCol B C D) by (conclude lemma_rightangleNC).

assert (neq C D) by (forward_using lemma_NCdistinct).

assert (Out C D D) by (conclude lemma_ray4).

assert (Supp B C D D E) by (conclude_def Supp ).

assert (CongA A B C B C D) by (conclude lemma_Euclid4).

assert (CongA B C D D C E) by (conclude lemma_Euclid4).

assert (RT A B C B C D) by (conclude_def RT ).

assert (Par B A C D) by (conclude proposition_28C).

assert (Par C D B A) by (conclude lemma_parallelsymmetric).

assert (Par C D A B) by (forward_using lemma_parallelflip).

assert (Par A B C D) by (conclude lemma_parallelsymmetric).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.proposition_28C.

Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelflip.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_twoperpsparallel :

∀ A B C D,

Per A B C → Per B C D → OS A D B C →

Par A B C D.

Proof.

intros.

assert (nCol A B C) by (conclude lemma_rightangleNC).

assert (neq B C) by (forward_using lemma_NCdistinct).

let Tf:=fresh in

assert (Tf:∃ E, (BetS B C E ∧ Cong C E B C)) by (conclude postulate_extension);destruct Tf as [E];spliter.

assert (Col B C E) by (conclude_def Col ).

assert (neq C E) by (forward_using lemma_betweennotequal).

assert (neq E C) by (conclude lemma_inequalitysymmetric).

assert (Col C B E) by (forward_using lemma_collinearorder).

assert (Per E C D) by (conclude lemma_collinearright).

assert (Per D C E) by (conclude lemma_8_2).

assert (eq D D) by (conclude cn_equalityreflexive).

assert (nCol B C D) by (conclude lemma_rightangleNC).

assert (neq C D) by (forward_using lemma_NCdistinct).

assert (Out C D D) by (conclude lemma_ray4).

assert (Supp B C D D E) by (conclude_def Supp ).

assert (CongA A B C B C D) by (conclude lemma_Euclid4).

assert (CongA B C D D C E) by (conclude lemma_Euclid4).

assert (RT A B C B C D) by (conclude_def RT ).

assert (Par B A C D) by (conclude proposition_28C).

assert (Par C D B A) by (conclude lemma_parallelsymmetric).

assert (Par C D A B) by (forward_using lemma_parallelflip).

assert (Par A B C D) by (conclude lemma_parallelsymmetric).

close.

Qed.

End Euclid.