# Library GeoCoq.Elements.OriginalProofs.lemma_interior5

Require Export GeoCoq.Elements.OriginalProofs.lemma_betweennotequal.

Require Export GeoCoq.Elements.OriginalProofs.lemma_equalitysymmetric.

Require Export GeoCoq.Elements.OriginalProofs.lemma_nullsegment3.

Require Export GeoCoq.Elements.OriginalProofs.lemma_sumofparts.

Require Export GeoCoq.Elements.OriginalProofs.lemma_doublereverse.

Require Export GeoCoq.Elements.OriginalProofs.lemma_congruenceflip.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_interior5 :

∀ A B C D a b c d,

BetS A B C → BetS a b c → Cong A B a b → Cong B C b c → Cong A D a d → Cong C D c d →

Cong B D b d.

Proof.

intros.

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

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

assert (¬ eq C A).

{

intro.

assert (eq A C) by (conclude lemma_equalitysymmetric).

contradict.

}

let Tf:=fresh in

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

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

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

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

assert (Cong A M M A) by (conclude cn_equalityreverse).

assert (Cong M A A M) by (conclude lemma_congruencesymmetric).

assert (Cong M A B C) by (conclude lemma_congruencetransitive).

assert (neq b c) by (conclude lemma_nullsegment3).

assert (neq a c) by (forward_using lemma_betweennotequal).

assert (¬ eq c a).

{

intro.

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ m, (BetS c a m ∧ Cong a m b c)) by (conclude postulate_extension);destruct Tf as [m];spliter.

assert (BetS m a c) by (conclude axiom_betweennesssymmetry).

assert (Cong m a a m) by (conclude cn_equalityreverse).

assert (Cong m a b c) by (conclude lemma_congruencetransitive).

assert (Cong b c m a) by (conclude lemma_congruencesymmetric).

assert (Cong B C m a) by (conclude lemma_congruencetransitive).

assert (Cong M A m a) by (conclude lemma_congruencetransitive).

assert (Cong A C a c) by (conclude lemma_sumofparts).

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

assert (Cong C A c a) by (conclude lemma_congruencesymmetric).

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

assert (¬ eq B A).

{

intro.

assert (eq A B) by (conclude lemma_equalitysymmetric).

contradict.

}

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

assert (BetS B A M) by (conclude lemma_3_6a).

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

assert (BetS b a m) by (conclude lemma_3_6a).

assert (Cong A M a m) by (forward_using lemma_congruenceflip).

assert (Cong b a B A) by (forward_using lemma_doublereverse).

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

assert (Cong D M d m) by (conclude axiom_5_line).

assert (BetS m a b) by (conclude axiom_betweennesssymmetry).

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

assert (Cong M D m d) by (forward_using lemma_congruenceflip).

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

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

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_equalitysymmetric.

Require Export GeoCoq.Elements.OriginalProofs.lemma_nullsegment3.

Require Export GeoCoq.Elements.OriginalProofs.lemma_sumofparts.

Require Export GeoCoq.Elements.OriginalProofs.lemma_doublereverse.

Require Export GeoCoq.Elements.OriginalProofs.lemma_congruenceflip.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_interior5 :

∀ A B C D a b c d,

BetS A B C → BetS a b c → Cong A B a b → Cong B C b c → Cong A D a d → Cong C D c d →

Cong B D b d.

Proof.

intros.

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

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

assert (¬ eq C A).

{

intro.

assert (eq A C) by (conclude lemma_equalitysymmetric).

contradict.

}

let Tf:=fresh in

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

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

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

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

assert (Cong A M M A) by (conclude cn_equalityreverse).

assert (Cong M A A M) by (conclude lemma_congruencesymmetric).

assert (Cong M A B C) by (conclude lemma_congruencetransitive).

assert (neq b c) by (conclude lemma_nullsegment3).

assert (neq a c) by (forward_using lemma_betweennotequal).

assert (¬ eq c a).

{

intro.

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ m, (BetS c a m ∧ Cong a m b c)) by (conclude postulate_extension);destruct Tf as [m];spliter.

assert (BetS m a c) by (conclude axiom_betweennesssymmetry).

assert (Cong m a a m) by (conclude cn_equalityreverse).

assert (Cong m a b c) by (conclude lemma_congruencetransitive).

assert (Cong b c m a) by (conclude lemma_congruencesymmetric).

assert (Cong B C m a) by (conclude lemma_congruencetransitive).

assert (Cong M A m a) by (conclude lemma_congruencetransitive).

assert (Cong A C a c) by (conclude lemma_sumofparts).

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

assert (Cong C A c a) by (conclude lemma_congruencesymmetric).

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

assert (¬ eq B A).

{

intro.

assert (eq A B) by (conclude lemma_equalitysymmetric).

contradict.

}

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

assert (BetS B A M) by (conclude lemma_3_6a).

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

assert (BetS b a m) by (conclude lemma_3_6a).

assert (Cong A M a m) by (forward_using lemma_congruenceflip).

assert (Cong b a B A) by (forward_using lemma_doublereverse).

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

assert (Cong D M d m) by (conclude axiom_5_line).

assert (BetS m a b) by (conclude axiom_betweennesssymmetry).

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

assert (Cong M D m d) by (forward_using lemma_congruenceflip).

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

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

close.

Qed.

End Euclid.