# Library GeoCoq.Elements.OriginalProofs.lemma_fiveline

Require Export GeoCoq.Elements.OriginalProofs.lemma_betweennesspreserved.

Require Export GeoCoq.Elements.OriginalProofs.lemma_inequalitysymmetric.

Require Export GeoCoq.Elements.OriginalProofs.lemma_interior5.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_fiveline :

∀ A B C D a b c d,

Col A B C → Cong A B a b → Cong B C b c → Cong A D a d → Cong C D c d → Cong A C a c → neq A C →

Cong B D b d.

Proof.

intros.

assert ((eq A B ∨ eq A C ∨ eq B C ∨ BetS B A C ∨ BetS A B C ∨ BetS A C B)) by (conclude_def Col ).

assert (Cong B D b d).

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

{

assert (Cong B B a b) by (conclude cn_equalitysub).

assert (Cong a b B B) by (conclude lemma_congruencesymmetric).

assert (eq a b) by (conclude axiom_nullsegment1).

assert (Cong B D a d) by (conclude cn_equalitysub).

assert (Cong B D b d) by (conclude cn_equalitysub).

close.

}

{

assert (¬ ¬ Cong B D b d).

{

intro.

contradict.

}

close.

}

{

assert (Cong B B b c) by (conclude cn_equalitysub).

assert (Cong b c B B) by (conclude lemma_congruencesymmetric).

assert (eq b c) by (conclude axiom_nullsegment1).

assert (eq c b) by (conclude lemma_equalitysymmetric).

assert (Cong B D c d) by (conclude cn_equalitysub).

assert (Cong B D b d) by (conclude cn_equalitysub).

close.

}

{

assert (BetS C A B) by (conclude axiom_betweennesssymmetry).

assert (Cong C A c a) by (forward_using lemma_congruenceflip).

assert (Cong C B c b) by (forward_using lemma_congruenceflip).

assert (BetS c a b) by (conclude lemma_betweennesspreserved).

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

assert (Cong D B d b) by (conclude axiom_5_line).

assert (Cong B D b d) by (forward_using lemma_congruenceflip).

close.

}

{

assert (BetS a b c) by (conclude lemma_betweennesspreserved).

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

assert (Cong B D b d) by (conclude lemma_interior5).

close.

}

{

assert (Cong C B c b) by (forward_using lemma_congruenceflip).

assert (BetS a c b) by (conclude lemma_betweennesspreserved).

assert (Cong D B d b) by (conclude axiom_5_line).

assert (Cong B D b d) by (forward_using lemma_congruenceflip).

close.

}

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_inequalitysymmetric.

Require Export GeoCoq.Elements.OriginalProofs.lemma_interior5.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_fiveline :

∀ A B C D a b c d,

Col A B C → Cong A B a b → Cong B C b c → Cong A D a d → Cong C D c d → Cong A C a c → neq A C →

Cong B D b d.

Proof.

intros.

assert ((eq A B ∨ eq A C ∨ eq B C ∨ BetS B A C ∨ BetS A B C ∨ BetS A C B)) by (conclude_def Col ).

assert (Cong B D b d).

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

{

assert (Cong B B a b) by (conclude cn_equalitysub).

assert (Cong a b B B) by (conclude lemma_congruencesymmetric).

assert (eq a b) by (conclude axiom_nullsegment1).

assert (Cong B D a d) by (conclude cn_equalitysub).

assert (Cong B D b d) by (conclude cn_equalitysub).

close.

}

{

assert (¬ ¬ Cong B D b d).

{

intro.

contradict.

}

close.

}

{

assert (Cong B B b c) by (conclude cn_equalitysub).

assert (Cong b c B B) by (conclude lemma_congruencesymmetric).

assert (eq b c) by (conclude axiom_nullsegment1).

assert (eq c b) by (conclude lemma_equalitysymmetric).

assert (Cong B D c d) by (conclude cn_equalitysub).

assert (Cong B D b d) by (conclude cn_equalitysub).

close.

}

{

assert (BetS C A B) by (conclude axiom_betweennesssymmetry).

assert (Cong C A c a) by (forward_using lemma_congruenceflip).

assert (Cong C B c b) by (forward_using lemma_congruenceflip).

assert (BetS c a b) by (conclude lemma_betweennesspreserved).

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

assert (Cong D B d b) by (conclude axiom_5_line).

assert (Cong B D b d) by (forward_using lemma_congruenceflip).

close.

}

{

assert (BetS a b c) by (conclude lemma_betweennesspreserved).

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

assert (Cong B D b d) by (conclude lemma_interior5).

close.

}

{

assert (Cong C B c b) by (forward_using lemma_congruenceflip).

assert (BetS a c b) by (conclude lemma_betweennesspreserved).

assert (Cong D B d b) by (conclude axiom_5_line).

assert (Cong B D b d) by (forward_using lemma_congruenceflip).

close.

}

close.

Qed.

End Euclid.