# Library GeoCoq.Elements.OriginalProofs.lemma_rightreflection

Require Export GeoCoq.Elements.OriginalProofs.lemma_pointreflectionisometry.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_rightreflection :

∀ A B C E a b c,

Per A B C → Midpoint A E a → Midpoint B E b → Midpoint C E c →

Per a b c.

Proof.

intros.

let Tf:=fresh in

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

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

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

assert (Cong B C b c) by (conclude lemma_pointreflectionisometry).

assert (Per a b c).

by cases on (eq D E ∨ neq D E).

{

assert (Cong B E E b) by (conclude_def Midpoint ).

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

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

assert (Cong C E E c) by (conclude_def Midpoint ).

assert (Cong C D D c) by (conclude cn_equalitysub).

assert (Cong D C D c) by (forward_using lemma_congruenceflip).

assert (Cong A C D c) by (conclude lemma_congruencetransitive).

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

assert (Cong a c D c) by (conclude lemma_congruencetransitive).

assert (Cong A E E a) by (conclude_def Midpoint ).

assert (Cong A D D a) by (conclude cn_equalitysub).

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

assert (Cong B E E b) by (conclude_def Midpoint ).

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

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

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

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

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

assert (Cong a b D B) by (conclude lemma_congruencetransitive).

assert (Cong a b D b) by (conclude lemma_congruencetransitive).

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

assert (Cong a c D C) by (conclude lemma_congruencetransitive).

assert (Cong C E E c) by (conclude_def Midpoint ).

assert (Cong C D D c) by (conclude cn_equalitysub).

assert (Cong D C D c) by (forward_using lemma_congruenceflip).

assert (Cong a c D c) by (conclude lemma_congruencetransitive).

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

assert (Per a b c) by (conclude_def Per ).

close.

}

{

let Tf:=fresh in

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

assert (Cong E D d E) by (forward_using lemma_doublereverse).

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

assert (Midpoint D E d) by (conclude_def Midpoint ).

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

assert (Cong D C d c) by (conclude lemma_pointreflectionisometry).

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

assert (Cong a c D C) by (conclude lemma_congruencetransitive).

assert (Cong a c d c) by (conclude lemma_congruencetransitive).

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

assert (Cong A D a d) by (conclude lemma_pointreflectionisometry).

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

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

assert (Cong a b D B) by (conclude lemma_congruencetransitive).

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

assert (Cong a b d b) by (conclude lemma_congruencetransitive).

assert (Per a b c) by (conclude_def Per ).

close.

}

close.

Qed.

End Euclid.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_rightreflection :

∀ A B C E a b c,

Per A B C → Midpoint A E a → Midpoint B E b → Midpoint C E c →

Per a b c.

Proof.

intros.

let Tf:=fresh in

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

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

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

assert (Cong B C b c) by (conclude lemma_pointreflectionisometry).

assert (Per a b c).

by cases on (eq D E ∨ neq D E).

{

assert (Cong B E E b) by (conclude_def Midpoint ).

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

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

assert (Cong C E E c) by (conclude_def Midpoint ).

assert (Cong C D D c) by (conclude cn_equalitysub).

assert (Cong D C D c) by (forward_using lemma_congruenceflip).

assert (Cong A C D c) by (conclude lemma_congruencetransitive).

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

assert (Cong a c D c) by (conclude lemma_congruencetransitive).

assert (Cong A E E a) by (conclude_def Midpoint ).

assert (Cong A D D a) by (conclude cn_equalitysub).

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

assert (Cong B E E b) by (conclude_def Midpoint ).

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

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

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

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

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

assert (Cong a b D B) by (conclude lemma_congruencetransitive).

assert (Cong a b D b) by (conclude lemma_congruencetransitive).

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

assert (Cong a c D C) by (conclude lemma_congruencetransitive).

assert (Cong C E E c) by (conclude_def Midpoint ).

assert (Cong C D D c) by (conclude cn_equalitysub).

assert (Cong D C D c) by (forward_using lemma_congruenceflip).

assert (Cong a c D c) by (conclude lemma_congruencetransitive).

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

assert (Per a b c) by (conclude_def Per ).

close.

}

{

let Tf:=fresh in

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

assert (Cong E D d E) by (forward_using lemma_doublereverse).

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

assert (Midpoint D E d) by (conclude_def Midpoint ).

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

assert (Cong D C d c) by (conclude lemma_pointreflectionisometry).

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

assert (Cong a c D C) by (conclude lemma_congruencetransitive).

assert (Cong a c d c) by (conclude lemma_congruencetransitive).

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

assert (Cong A D a d) by (conclude lemma_pointreflectionisometry).

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

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

assert (Cong a b D B) by (conclude lemma_congruencetransitive).

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

assert (Cong a b d b) by (conclude lemma_congruencetransitive).

assert (Per a b c) by (conclude_def Per ).

close.

}

close.

Qed.

End Euclid.