# Library GeoCoq.Elements.OriginalProofs.lemma_8_3

Require Export GeoCoq.Elements.OriginalProofs.lemma_ray1.

Require Export GeoCoq.Elements.OriginalProofs.lemma_interior5.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_8_3 :

∀ A B C D,

Per A B C → Out B C D →

Per A B D.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ E, (BetS A B E ∧ Cong A B E B ∧ Cong A C E C ∧ neq B C)) by (conclude_def Per );destruct Tf as [E];spliter.

assert (Cong B C B C) by (conclude cn_congruencereflexive).

assert (Cong C D C D) by (conclude cn_congruencereflexive).

assert (Cong B A B E) by (forward_using lemma_congruenceflip).

assert (Cong C A C E) by (forward_using lemma_congruenceflip).

assert ((BetS B D C ∨ eq C D ∨ BetS B C D)) by (conclude lemma_ray1).

assert (Per A B D).

by cases on (BetS B D C ∨ eq C D ∨ BetS B C D).

{

assert (Cong B D B D) by (conclude cn_congruencereflexive).

assert (Cong D C D C) by (conclude cn_congruencereflexive).

assert (Cong D A D E) by (conclude lemma_interior5).

assert (Cong A D E D) by (forward_using lemma_congruenceflip).

assert (neq B D) by (forward_using lemma_betweennotequal).

assert (Per A B D) by (conclude_def Per ).

close.

}

{

assert (Per A B D) by (conclude cn_equalitysub).

close.

}

{

assert (Cong A D E D) by (conclude axiom_5_line).

assert (neq B D) by (forward_using lemma_betweennotequal).

assert (Per A B D) by (conclude_def Per ).

close.

}

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_interior5.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_8_3 :

∀ A B C D,

Per A B C → Out B C D →

Per A B D.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ E, (BetS A B E ∧ Cong A B E B ∧ Cong A C E C ∧ neq B C)) by (conclude_def Per );destruct Tf as [E];spliter.

assert (Cong B C B C) by (conclude cn_congruencereflexive).

assert (Cong C D C D) by (conclude cn_congruencereflexive).

assert (Cong B A B E) by (forward_using lemma_congruenceflip).

assert (Cong C A C E) by (forward_using lemma_congruenceflip).

assert ((BetS B D C ∨ eq C D ∨ BetS B C D)) by (conclude lemma_ray1).

assert (Per A B D).

by cases on (BetS B D C ∨ eq C D ∨ BetS B C D).

{

assert (Cong B D B D) by (conclude cn_congruencereflexive).

assert (Cong D C D C) by (conclude cn_congruencereflexive).

assert (Cong D A D E) by (conclude lemma_interior5).

assert (Cong A D E D) by (forward_using lemma_congruenceflip).

assert (neq B D) by (forward_using lemma_betweennotequal).

assert (Per A B D) by (conclude_def Per ).

close.

}

{

assert (Per A B D) by (conclude cn_equalitysub).

close.

}

{

assert (Cong A D E D) by (conclude axiom_5_line).

assert (neq B D) by (forward_using lemma_betweennotequal).

assert (Per A B D) by (conclude_def Per ).

close.

}

close.

Qed.

End Euclid.