# Library GeoCoq.Elements.OriginalProofs.proposition_11B

Require Export GeoCoq.Elements.OriginalProofs.lemma_notperp.

Require Export GeoCoq.Elements.OriginalProofs.lemma_pointreflectionisometry.

Require Export GeoCoq.Elements.OriginalProofs.lemma_planeseparation.

Require Export GeoCoq.Elements.OriginalProofs.lemma_oppositesidesymmetric.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_11B :

∀ A B C P,

BetS A C B → nCol A B P →

∃ X, Per A C X ∧ TS X A B P.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ M, (nCol A B M ∧ OS M P A B ∧ ¬ Per A C M)) by (conclude lemma_notperp);destruct Tf as [M];spliter.

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

let Tf:=fresh in

assert (Tf:∃ Q, Perp_at M Q A B Q) by (conclude proposition_12);destruct Tf as [Q];spliter.

let Tf:=fresh in

assert (Tf:∃ E, (Col M Q Q ∧ Col A B Q ∧ Col A B E ∧ Per E Q M)) by (conclude_def Perp_at );destruct Tf as [E];spliter.

assert (¬ eq M Q).

{

intro.

assert (Col A B M) by (conclude cn_equalitysub).

contradict.

}

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

assert (Per M Q E) by (conclude lemma_8_2).

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

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

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

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

assert (¬ eq C Q).

{

intro.

assert (Per E C M) by (conclude cn_equalitysub).

assert (Col A E C) by (conclude lemma_collinear4).

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

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

assert (Per A C M) by (conclude lemma_collinearright).

contradict.

}

assert (Col C Q E) by (conclude lemma_collinear5).

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

assert (Per C Q M) by (conclude lemma_collinearright).

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

let Tf:=fresh in

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

assert (¬ eq M G).

{

intro.

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

assert (Col Q M C) by (conclude_def Col ).

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

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

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

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

assert (Col C M B) by (conclude lemma_collinear4).

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

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

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

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

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

contradict.

}

rename_H H;let Tf:=fresh in

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

assert (Cong M G G H) by (conclude lemma_congruencesymmetric).

assert (Midpoint M G H) by (conclude_def Midpoint ).

assert (Cong Q G G C) by (forward_using lemma_congruenceflip).

assert (Midpoint Q G C) by (conclude_def Midpoint ).

assert (Col Q G C) by (conclude_def Col ).

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

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

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

assert (Per G Q M) by (conclude lemma_collinearright).

let Tf:=fresh in

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

assert (Cong M Q Q J) by (conclude lemma_congruencesymmetric).

assert (Per M Q G) by (conclude lemma_8_2).

assert (Cong M G J G) by (conclude lemma_rightreverse).

assert (BetS J Q M) by (conclude axiom_betweennesssymmetry).

assert (Cong J Q M Q) by (forward_using lemma_congruenceflip).

assert (Cong J G M G) by (conclude lemma_congruencesymmetric).

assert (Per J Q G) by (conclude_def Per ).

assert (¬ eq J G).

{

intro.

assert (Col J Q G) by (conclude_def Col ).

assert (nCol J Q G) by (conclude lemma_rightangleNC).

contradict.

}

let Tf:=fresh in

assert (Tf:∃ K, (BetS J G K ∧ Cong G K J G)) by (conclude postulate_extension);destruct Tf as [K];spliter.

assert (Cong J G G K) by (conclude lemma_congruencesymmetric).

assert (Midpoint J G K) by (conclude_def Midpoint ).

assert (Cong J Q K C) by (conclude lemma_pointreflectionisometry).

assert (Cong M Q H C) by (conclude lemma_pointreflectionisometry).

assert (Cong Q M C H) by (conclude lemma_pointreflectionisometry).

assert (Cong Q J C K) by (conclude lemma_pointreflectionisometry).

assert (Cong M J H K) by (conclude lemma_pointreflectionisometry).

assert (BetS H C K) by (conclude lemma_betweennesspreserved).

assert (Cong H G G M) by (forward_using lemma_congruenceflip).

assert (Cong G M J G) by (forward_using lemma_congruenceflip).

assert (Cong H G J G) by (conclude lemma_congruencetransitive).

assert (Cong J G G K) by (conclude lemma_congruencesymmetric).

assert (Cong H G G K) by (conclude lemma_congruencetransitive).

assert (Cong H G K G) by (forward_using lemma_congruenceflip).

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

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

assert (Cong M Q Q J) by (conclude lemma_congruencesymmetric).

assert (Cong H C Q J) by (conclude lemma_congruencetransitive).

assert (Cong H C C K) by (conclude lemma_congruencetransitive).

assert (Cong H C K C) by (forward_using lemma_congruenceflip).

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

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

assert (Per H C G) by (conclude_def Per ).

assert (Per G C H) by (conclude lemma_8_2).

assert (Col Q G C) by (conclude_def Col ).

assert (eq A A) by (conclude cn_equalityreflexive).

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

assert (Col Q C A) by (conclude lemma_collinear5).

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

assert (Col C A G) by (conclude lemma_collinear4).

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

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

assert (Per A C H) by (conclude lemma_collinearright).

assert (BetS H G M) by (conclude axiom_betweennesssymmetry).

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

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

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

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

assert (¬ Col A B H).

{

intro.

assert (Col B G H) by (conclude lemma_collinear4).

assert (Col M G H) by (conclude_def Col ).

assert (Col G H M) by (forward_using lemma_collinearorder).

assert (Col G H B) by (forward_using lemma_collinearorder).

assert (neq G H) by (forward_using lemma_betweennotequal).

assert (Col H M B) by (conclude lemma_collinear4).

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

assert (Col H B M) by (forward_using lemma_collinearorder).

assert (Col A B M).

by cases on (eq H B ∨ neq H B).

{

assert (BetS M G B) by (conclude cn_equalitysub).

assert (Col M G B) by (conclude_def Col ).

assert (Col G B M) by (forward_using lemma_collinearorder).

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

assert (neq G B) by (conclude cn_equalitysub).

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

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

close.

}

{

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

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

close.

}

contradict.

}

assert (TS H A B M) by (conclude_def TS ).

assert (OS P M A B) by (forward_using lemma_samesidesymmetric).

assert (TS M A B H) by (conclude_def TS ).

assert (TS P A B H) by (conclude lemma_planeseparation).

assert (TS H A B P) by (conclude lemma_oppositesidesymmetric).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_pointreflectionisometry.

Require Export GeoCoq.Elements.OriginalProofs.lemma_planeseparation.

Require Export GeoCoq.Elements.OriginalProofs.lemma_oppositesidesymmetric.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_11B :

∀ A B C P,

BetS A C B → nCol A B P →

∃ X, Per A C X ∧ TS X A B P.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ M, (nCol A B M ∧ OS M P A B ∧ ¬ Per A C M)) by (conclude lemma_notperp);destruct Tf as [M];spliter.

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

let Tf:=fresh in

assert (Tf:∃ Q, Perp_at M Q A B Q) by (conclude proposition_12);destruct Tf as [Q];spliter.

let Tf:=fresh in

assert (Tf:∃ E, (Col M Q Q ∧ Col A B Q ∧ Col A B E ∧ Per E Q M)) by (conclude_def Perp_at );destruct Tf as [E];spliter.

assert (¬ eq M Q).

{

intro.

assert (Col A B M) by (conclude cn_equalitysub).

contradict.

}

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

assert (Per M Q E) by (conclude lemma_8_2).

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

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

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

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

assert (¬ eq C Q).

{

intro.

assert (Per E C M) by (conclude cn_equalitysub).

assert (Col A E C) by (conclude lemma_collinear4).

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

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

assert (Per A C M) by (conclude lemma_collinearright).

contradict.

}

assert (Col C Q E) by (conclude lemma_collinear5).

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

assert (Per C Q M) by (conclude lemma_collinearright).

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

let Tf:=fresh in

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

assert (¬ eq M G).

{

intro.

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

assert (Col Q M C) by (conclude_def Col ).

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

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

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

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

assert (Col C M B) by (conclude lemma_collinear4).

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

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

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

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

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

contradict.

}

rename_H H;let Tf:=fresh in

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

assert (Cong M G G H) by (conclude lemma_congruencesymmetric).

assert (Midpoint M G H) by (conclude_def Midpoint ).

assert (Cong Q G G C) by (forward_using lemma_congruenceflip).

assert (Midpoint Q G C) by (conclude_def Midpoint ).

assert (Col Q G C) by (conclude_def Col ).

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

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

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

assert (Per G Q M) by (conclude lemma_collinearright).

let Tf:=fresh in

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

assert (Cong M Q Q J) by (conclude lemma_congruencesymmetric).

assert (Per M Q G) by (conclude lemma_8_2).

assert (Cong M G J G) by (conclude lemma_rightreverse).

assert (BetS J Q M) by (conclude axiom_betweennesssymmetry).

assert (Cong J Q M Q) by (forward_using lemma_congruenceflip).

assert (Cong J G M G) by (conclude lemma_congruencesymmetric).

assert (Per J Q G) by (conclude_def Per ).

assert (¬ eq J G).

{

intro.

assert (Col J Q G) by (conclude_def Col ).

assert (nCol J Q G) by (conclude lemma_rightangleNC).

contradict.

}

let Tf:=fresh in

assert (Tf:∃ K, (BetS J G K ∧ Cong G K J G)) by (conclude postulate_extension);destruct Tf as [K];spliter.

assert (Cong J G G K) by (conclude lemma_congruencesymmetric).

assert (Midpoint J G K) by (conclude_def Midpoint ).

assert (Cong J Q K C) by (conclude lemma_pointreflectionisometry).

assert (Cong M Q H C) by (conclude lemma_pointreflectionisometry).

assert (Cong Q M C H) by (conclude lemma_pointreflectionisometry).

assert (Cong Q J C K) by (conclude lemma_pointreflectionisometry).

assert (Cong M J H K) by (conclude lemma_pointreflectionisometry).

assert (BetS H C K) by (conclude lemma_betweennesspreserved).

assert (Cong H G G M) by (forward_using lemma_congruenceflip).

assert (Cong G M J G) by (forward_using lemma_congruenceflip).

assert (Cong H G J G) by (conclude lemma_congruencetransitive).

assert (Cong J G G K) by (conclude lemma_congruencesymmetric).

assert (Cong H G G K) by (conclude lemma_congruencetransitive).

assert (Cong H G K G) by (forward_using lemma_congruenceflip).

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

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

assert (Cong M Q Q J) by (conclude lemma_congruencesymmetric).

assert (Cong H C Q J) by (conclude lemma_congruencetransitive).

assert (Cong H C C K) by (conclude lemma_congruencetransitive).

assert (Cong H C K C) by (forward_using lemma_congruenceflip).

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

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

assert (Per H C G) by (conclude_def Per ).

assert (Per G C H) by (conclude lemma_8_2).

assert (Col Q G C) by (conclude_def Col ).

assert (eq A A) by (conclude cn_equalityreflexive).

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

assert (Col Q C A) by (conclude lemma_collinear5).

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

assert (Col C A G) by (conclude lemma_collinear4).

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

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

assert (Per A C H) by (conclude lemma_collinearright).

assert (BetS H G M) by (conclude axiom_betweennesssymmetry).

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

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

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

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

assert (¬ Col A B H).

{

intro.

assert (Col B G H) by (conclude lemma_collinear4).

assert (Col M G H) by (conclude_def Col ).

assert (Col G H M) by (forward_using lemma_collinearorder).

assert (Col G H B) by (forward_using lemma_collinearorder).

assert (neq G H) by (forward_using lemma_betweennotequal).

assert (Col H M B) by (conclude lemma_collinear4).

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

assert (Col H B M) by (forward_using lemma_collinearorder).

assert (Col A B M).

by cases on (eq H B ∨ neq H B).

{

assert (BetS M G B) by (conclude cn_equalitysub).

assert (Col M G B) by (conclude_def Col ).

assert (Col G B M) by (forward_using lemma_collinearorder).

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

assert (neq G B) by (conclude cn_equalitysub).

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

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

close.

}

{

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

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

close.

}

contradict.

}

assert (TS H A B M) by (conclude_def TS ).

assert (OS P M A B) by (forward_using lemma_samesidesymmetric).

assert (TS M A B H) by (conclude_def TS ).

assert (TS P A B H) by (conclude lemma_planeseparation).

assert (TS H A B P) by (conclude lemma_oppositesidesymmetric).

close.

Qed.

End Euclid.