# Library GeoCoq.Elements.OriginalProofs.lemma_pointreflectionisometry

Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthancongruence2.

Require Export GeoCoq.Elements.OriginalProofs.proposition_03.

Require Export GeoCoq.Elements.OriginalProofs.proposition_15.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_pointreflectionisometry :

∀ A B C P Q,

Midpoint A B C → Midpoint P B Q →

Cong A P C Q.

Proof.

intros.

assert ((BetS A B C ∧ Cong A B B C)) by (conclude_def Midpoint ).

assert ((BetS P B Q ∧ Cong P B B Q)) by (conclude_def Midpoint ).

assert (Cong A P C Q).

by cases on (Col A B P ∨ nCol A B P).

{

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

assert (Cong A P C Q).

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

{

assert (¬ ¬ Cong A P C Q).

{

intro.

assert (BetS A B C) by (conclude_def Midpoint ).

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

contradict.

}

close.

}

{

assert (BetS A B Q) by (conclude cn_equalitysub).

assert (Cong B C A B) by (conclude lemma_congruencesymmetric).

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

assert (Cong A B P B) by (conclude cn_equalitysub).

assert (Cong B C P B) by (conclude lemma_congruencetransitive).

assert (Cong B C B Q) by (conclude lemma_congruencetransitive).

assert (eq C Q) by (conclude lemma_extensionunique).

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

assert (Cong C Q C C) by (conclude cn_equalitysub).

assert (Cong C C C Q) by (conclude lemma_congruencesymmetric).

assert (Cong A P A P) by (conclude cn_congruencereflexive).

assert (Cong A P A A) by (conclude cn_equalitysub).

assert (Cong A A C C) by (conclude axiom_nullsegment2).

assert (Cong A P C C) by (conclude lemma_congruencetransitive).

assert (Cong A P C Q) by (conclude lemma_congruencetransitive).

close.

}

{

assert (¬ ¬ Cong A P C Q).

{

intro.

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

assert (neq B P) by (conclude lemma_inequalitysymmetric).

contradict.

}

close.

}

{

assert (Cong P B Q B) by (forward_using lemma_congruenceflip).

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

assert (Cong B C A B) by (conclude lemma_congruencesymmetric).

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

assert (Cong Q B B P) by (forward_using lemma_doublereverse).

assert (Cong B Q B P) by (forward_using lemma_congruenceflip).

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

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

assert (Cong B A C B) by (forward_using lemma_doublereverse).

assert (Lt C B B P) by (conclude_def Lt ).

assert (Cong B P B Q) by (conclude lemma_congruencesymmetric).

assert (Lt C B B Q) by (conclude lemma_lessthancongruence).

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

assert (Lt B C B Q) by (conclude lemma_lessthancongruence2).

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

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

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

rename_H H;let Tf:=fresh in

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

assert (Out B Q H) by (conclude lemma_ray4).

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

assert (BetS P B C) by (conclude lemma_3_7a).

assert (Out B C Q) by (conclude_def Out ).

assert (Out B Q C) by (conclude lemma_ray5).

assert (Cong B C B H) by (conclude lemma_congruencesymmetric).

assert (eq C H) by (conclude lemma_layoffunique).

assert (BetS B C Q) by (conclude cn_equalitysub).

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

assert (Cong B A B C) by (conclude lemma_congruencesymmetric).

assert (Cong A P C Q) by (conclude lemma_differenceofparts).

close.

}

{

assert (¬ ¬ Cong A P C Q).

{

intro.

assert (¬ BetS B P C).

{

intro.

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

assert (BetS C B Q) by (conclude lemma_3_7a).

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

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

assert (Cong B P Q B) by (forward_using lemma_congruenceflip).

assert (Cong B P B Q) by (forward_using lemma_congruenceflip).

assert (Cong A P C Q) by (conclude lemma_sumofparts).

contradict.

}

assert (¬ BetS B C P).

{

intro.

assert (BetS A B P) by (conclude lemma_3_7b).

assert (BetS Q B P) by (conclude axiom_betweennesssymmetry).

assert (BetS Q B C) by (conclude axiom_innertransitivity).

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

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

assert (Cong B P B Q) by (forward_using lemma_congruenceflip).

assert (Cong A P C Q) by (conclude lemma_sumofparts).

contradict.

}

assert (eq P C) by (conclude lemma_outerconnectivity).

assert (Cong A B B P) by (conclude cn_equalitysub).

assert (Cong B P B Q) by (forward_using lemma_congruenceflip).

assert (Cong A B B Q) by (conclude lemma_congruencetransitive).

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

assert (BetS P B A) by (conclude cn_equalitysub).

assert (Cong B Q A B) by (conclude lemma_congruencesymmetric).

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

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

assert (neq Q B) by (conclude lemma_inequalitysymmetric).

assert (eq Q A) by (conclude lemma_extensionunique).

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

assert (Cong A P C A) by (conclude cn_equalitysub).

assert (Cong A P C Q) by (conclude cn_equalitysub).

contradict.

}

close.

}

{

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

assert (Cong P B Q B) by (forward_using lemma_congruenceflip).

assert (Cong B Q P B) by (conclude lemma_congruencesymmetric).

assert (Cong B Q B P) by (forward_using lemma_congruenceflip).

assert (Cong C B B A) by (forward_using lemma_doublereverse).

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

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

assert (Cong Q B B P) by (forward_using lemma_congruenceflip).

assert (Cong B P Q B) by (forward_using lemma_doublereverse).

assert (Lt Q B B A) by (conclude_def Lt ).

assert (Cong B A B C) by (conclude lemma_congruencesymmetric).

assert (Lt Q B B C) by (conclude lemma_lessthancongruence).

assert (Cong Q B B Q) by (conclude cn_equalityreverse).

assert (Lt B Q B C) by (conclude lemma_lessthancongruence2).

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

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

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

rename_H H;let Tf:=fresh in

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

assert (BetS P B C) by (conclude lemma_3_6a).

assert (Out B C Q) by (conclude_def Out ).

assert (Out B Q C) by (conclude lemma_ray5).

assert (Out B C H) by (conclude lemma_ray4).

assert (Cong B Q B H) by (conclude lemma_congruencesymmetric).

assert (eq Q H) by (conclude lemma_layoffunique).

assert (BetS B Q C) by (conclude cn_equalitysub).

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

assert (Cong B P B Q) by (conclude lemma_congruencesymmetric).

assert (Cong P A Q C) by (conclude lemma_differenceofparts).

assert (Cong A P C Q) by (forward_using lemma_congruenceflip).

close.

}

close.

}

{

assert (CongA A B P Q B C) by (conclude proposition_15a).

assert (Triangle A B P) by (conclude_def Triangle ).

assert (¬ Col C B Q).

{

intro.

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

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

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

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

assert (Col B Q A) by (conclude lemma_collinear4).

assert (Col P B Q) by (conclude_def Col ).

assert (Col Q B P) by (forward_using lemma_collinearorder).

assert (Col Q B A) by (forward_using lemma_collinearorder).

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

assert (neq Q B) by (conclude lemma_inequalitysymmetric).

assert (Col B P A) by (conclude lemma_collinear4).

assert (Col A B P) by (forward_using lemma_collinearorder).

contradict.

}

assert (¬ Col Q B C).

{

intro.

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

contradict.

}

assert (CongA Q B C C B Q) by (conclude lemma_ABCequalsCBA).

assert (CongA A B P C B Q) by (conclude lemma_equalanglestransitive).

assert (Triangle C B Q) by (conclude_def Triangle ).

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

assert (Cong B P B Q) by (forward_using lemma_congruenceflip).

assert (Cong A P C Q) by (conclude proposition_04).

close.

}

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.proposition_03.

Require Export GeoCoq.Elements.OriginalProofs.proposition_15.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_pointreflectionisometry :

∀ A B C P Q,

Midpoint A B C → Midpoint P B Q →

Cong A P C Q.

Proof.

intros.

assert ((BetS A B C ∧ Cong A B B C)) by (conclude_def Midpoint ).

assert ((BetS P B Q ∧ Cong P B B Q)) by (conclude_def Midpoint ).

assert (Cong A P C Q).

by cases on (Col A B P ∨ nCol A B P).

{

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

assert (Cong A P C Q).

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

{

assert (¬ ¬ Cong A P C Q).

{

intro.

assert (BetS A B C) by (conclude_def Midpoint ).

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

contradict.

}

close.

}

{

assert (BetS A B Q) by (conclude cn_equalitysub).

assert (Cong B C A B) by (conclude lemma_congruencesymmetric).

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

assert (Cong A B P B) by (conclude cn_equalitysub).

assert (Cong B C P B) by (conclude lemma_congruencetransitive).

assert (Cong B C B Q) by (conclude lemma_congruencetransitive).

assert (eq C Q) by (conclude lemma_extensionunique).

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

assert (Cong C Q C C) by (conclude cn_equalitysub).

assert (Cong C C C Q) by (conclude lemma_congruencesymmetric).

assert (Cong A P A P) by (conclude cn_congruencereflexive).

assert (Cong A P A A) by (conclude cn_equalitysub).

assert (Cong A A C C) by (conclude axiom_nullsegment2).

assert (Cong A P C C) by (conclude lemma_congruencetransitive).

assert (Cong A P C Q) by (conclude lemma_congruencetransitive).

close.

}

{

assert (¬ ¬ Cong A P C Q).

{

intro.

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

assert (neq B P) by (conclude lemma_inequalitysymmetric).

contradict.

}

close.

}

{

assert (Cong P B Q B) by (forward_using lemma_congruenceflip).

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

assert (Cong B C A B) by (conclude lemma_congruencesymmetric).

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

assert (Cong Q B B P) by (forward_using lemma_doublereverse).

assert (Cong B Q B P) by (forward_using lemma_congruenceflip).

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

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

assert (Cong B A C B) by (forward_using lemma_doublereverse).

assert (Lt C B B P) by (conclude_def Lt ).

assert (Cong B P B Q) by (conclude lemma_congruencesymmetric).

assert (Lt C B B Q) by (conclude lemma_lessthancongruence).

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

assert (Lt B C B Q) by (conclude lemma_lessthancongruence2).

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

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

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

rename_H H;let Tf:=fresh in

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

assert (Out B Q H) by (conclude lemma_ray4).

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

assert (BetS P B C) by (conclude lemma_3_7a).

assert (Out B C Q) by (conclude_def Out ).

assert (Out B Q C) by (conclude lemma_ray5).

assert (Cong B C B H) by (conclude lemma_congruencesymmetric).

assert (eq C H) by (conclude lemma_layoffunique).

assert (BetS B C Q) by (conclude cn_equalitysub).

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

assert (Cong B A B C) by (conclude lemma_congruencesymmetric).

assert (Cong A P C Q) by (conclude lemma_differenceofparts).

close.

}

{

assert (¬ ¬ Cong A P C Q).

{

intro.

assert (¬ BetS B P C).

{

intro.

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

assert (BetS C B Q) by (conclude lemma_3_7a).

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

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

assert (Cong B P Q B) by (forward_using lemma_congruenceflip).

assert (Cong B P B Q) by (forward_using lemma_congruenceflip).

assert (Cong A P C Q) by (conclude lemma_sumofparts).

contradict.

}

assert (¬ BetS B C P).

{

intro.

assert (BetS A B P) by (conclude lemma_3_7b).

assert (BetS Q B P) by (conclude axiom_betweennesssymmetry).

assert (BetS Q B C) by (conclude axiom_innertransitivity).

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

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

assert (Cong B P B Q) by (forward_using lemma_congruenceflip).

assert (Cong A P C Q) by (conclude lemma_sumofparts).

contradict.

}

assert (eq P C) by (conclude lemma_outerconnectivity).

assert (Cong A B B P) by (conclude cn_equalitysub).

assert (Cong B P B Q) by (forward_using lemma_congruenceflip).

assert (Cong A B B Q) by (conclude lemma_congruencetransitive).

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

assert (BetS P B A) by (conclude cn_equalitysub).

assert (Cong B Q A B) by (conclude lemma_congruencesymmetric).

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

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

assert (neq Q B) by (conclude lemma_inequalitysymmetric).

assert (eq Q A) by (conclude lemma_extensionunique).

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

assert (Cong A P C A) by (conclude cn_equalitysub).

assert (Cong A P C Q) by (conclude cn_equalitysub).

contradict.

}

close.

}

{

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

assert (Cong P B Q B) by (forward_using lemma_congruenceflip).

assert (Cong B Q P B) by (conclude lemma_congruencesymmetric).

assert (Cong B Q B P) by (forward_using lemma_congruenceflip).

assert (Cong C B B A) by (forward_using lemma_doublereverse).

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

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

assert (Cong Q B B P) by (forward_using lemma_congruenceflip).

assert (Cong B P Q B) by (forward_using lemma_doublereverse).

assert (Lt Q B B A) by (conclude_def Lt ).

assert (Cong B A B C) by (conclude lemma_congruencesymmetric).

assert (Lt Q B B C) by (conclude lemma_lessthancongruence).

assert (Cong Q B B Q) by (conclude cn_equalityreverse).

assert (Lt B Q B C) by (conclude lemma_lessthancongruence2).

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

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

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

rename_H H;let Tf:=fresh in

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

assert (BetS P B C) by (conclude lemma_3_6a).

assert (Out B C Q) by (conclude_def Out ).

assert (Out B Q C) by (conclude lemma_ray5).

assert (Out B C H) by (conclude lemma_ray4).

assert (Cong B Q B H) by (conclude lemma_congruencesymmetric).

assert (eq Q H) by (conclude lemma_layoffunique).

assert (BetS B Q C) by (conclude cn_equalitysub).

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

assert (Cong B P B Q) by (conclude lemma_congruencesymmetric).

assert (Cong P A Q C) by (conclude lemma_differenceofparts).

assert (Cong A P C Q) by (forward_using lemma_congruenceflip).

close.

}

close.

}

{

assert (CongA A B P Q B C) by (conclude proposition_15a).

assert (Triangle A B P) by (conclude_def Triangle ).

assert (¬ Col C B Q).

{

intro.

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

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

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

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

assert (Col B Q A) by (conclude lemma_collinear4).

assert (Col P B Q) by (conclude_def Col ).

assert (Col Q B P) by (forward_using lemma_collinearorder).

assert (Col Q B A) by (forward_using lemma_collinearorder).

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

assert (neq Q B) by (conclude lemma_inequalitysymmetric).

assert (Col B P A) by (conclude lemma_collinear4).

assert (Col A B P) by (forward_using lemma_collinearorder).

contradict.

}

assert (¬ Col Q B C).

{

intro.

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

contradict.

}

assert (CongA Q B C C B Q) by (conclude lemma_ABCequalsCBA).

assert (CongA A B P C B Q) by (conclude lemma_equalanglestransitive).

assert (Triangle C B Q) by (conclude_def Triangle ).

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

assert (Cong B P B Q) by (forward_using lemma_congruenceflip).

assert (Cong A P C Q) by (conclude proposition_04).

close.

}

close.

Qed.

End Euclid.