Library GeoCoq.Elements.OriginalProofs.proposition_10

Require Export GeoCoq.Elements.OriginalProofs.proposition_01.
Require Export GeoCoq.Elements.OriginalProofs.proposition_03.
Require Export GeoCoq.Elements.OriginalProofs.lemma_interior5.
Require Export GeoCoq.Elements.OriginalProofs.lemma_twolines.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_10 :
   ∀ A B,
   neq A B →
   ∃ X, BetS A X B ∧ Cong X A X B.
Proof.
intros.
let Tf:=fresh in
assert (Tf:∃ C, (equilateral A B C ∧ Triangle A B C)) by (conclude proposition_01);destruct Tf as [C];spliter.
assert (nCol A B C) by (conclude_def Triangle ).
assert ((Cong A B B C ∧ Cong B C C A)) by (conclude_def equilateral ).
assert (Cong A C C B) by (forward_using lemma_doublereverse).
assert (Cong A C B C) by (forward_using lemma_congruenceflip).
assert (¬ eq C B).
 {
 intro.
 assert (Col A C B) by (conclude_def Col ).
 assert (Col A B C) by (forward_using lemma_collinearorder).
 contradict.
 }
let Tf:=fresh in
assert (Tf:∃ D, (BetS C B D ∧ Cong B D A B)) by (conclude postulate_extension);destruct Tf as [D];spliter.
assert (¬ eq C A).
 {
 intro.
 assert (Col B C A) by (conclude_def Col ).
 assert (Col A B C) by (forward_using lemma_collinearorder).
 contradict.
 }
let Tf:=fresh in
assert (Tf:∃ E, (BetS C A E ∧ Cong A E A B)) by (conclude postulate_extension);destruct Tf as [E];spliter.
assert (BetS D B C) by (conclude axiom_betweennesssymmetry).
assert (BetS E A C) by (conclude axiom_betweennesssymmetry).
assert (¬ Col D C E).
 {
 intro.
 assert (Col C A E) by (conclude_def Col ).
 assert (Col C B D) by (conclude_def Col ).
 assert (Col E C D) by (forward_using lemma_collinearorder).
 assert (Col E C A) by (forward_using lemma_collinearorder).
 assert (neq C E) by (forward_using lemma_betweennotequal).
 assert (neq E C) by (conclude lemma_inequalitysymmetric).
 assert (Col C D A) by (conclude lemma_collinear4).
 assert (Col D C B) by (forward_using lemma_collinearorder).
 assert (Col D C A) by (forward_using lemma_collinearorder).
 assert (neq C D) by (forward_using lemma_betweennotequal).
 assert (neq D C) by (conclude lemma_inequalitysymmetric).
 assert (Col C B A) by (conclude lemma_collinear4).
 assert (Col A B C) by (forward_using lemma_collinearorder).
 contradict.
 }
let Tf:=fresh in
assert (Tf:∃ F, (BetS D F A ∧ BetS E F B)) by (conclude postulate_Pasch_inner);destruct Tf as [F];spliter.
assert (¬ Col C E B).
 {
 intro.
 assert (Col C A E) by (conclude_def Col ).
 assert (Col E A C) by (forward_using lemma_collinearorder).
 assert (Col C E A) by (forward_using lemma_collinearorder).
 assert (neq C E) by (forward_using lemma_betweennotequal).
 assert (Col E B A) by (conclude lemma_collinear4).
 assert (Col E A B) by (forward_using lemma_collinearorder).
 assert (neq E A) by (forward_using lemma_betweennotequal).
 assert (Col A B C) by (conclude lemma_collinear4).
 contradict.
 }
assert (BetS B F E) by (conclude axiom_betweennesssymmetry).
assert (BetS A F D) by (conclude axiom_betweennesssymmetry).
assert (neq C D) by (forward_using lemma_betweennotequal).
assert (neq D C) by (conclude lemma_inequalitysymmetric).
assert (¬ Col A D C).
 {
 intro.
 assert (Col C B D) by (conclude_def Col ).
 assert (Col D C A) by (forward_using lemma_collinearorder).
 assert (Col D C B) by (forward_using lemma_collinearorder).
 assert (Col C A B) by (conclude lemma_collinear4).
 assert (Col A B C) by (forward_using lemma_collinearorder).
 contradict.
 }
let Tf:=fresh in
assert (Tf:∃ M, (BetS A M B ∧ BetS C M F)) by (conclude postulate_Pasch_inner);destruct Tf as [M];spliter.
assert (Cong C A C B) by (forward_using lemma_congruenceflip).
assert (Cong A B A E) by (conclude lemma_congruencesymmetric).
assert (Cong B D A E) by (conclude lemma_congruencetransitive).
assert (Cong A E B D) by (conclude lemma_congruencesymmetric).
assert (Cong A B B A) by (conclude cn_equalityreverse).
assert (neq B C) by (forward_using lemma_betweennotequal).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert (Cong C B C A) by (conclude lemma_congruencesymmetric).
assert (Cong B E A D) by (conclude axiom_5_line).
assert (Cong B F B F) by (conclude cn_congruencereflexive).
assert (Lt B F B E) by (conclude_def Lt ).
assert (neq B E) by (forward_using lemma_betweennotequal).
assert (neq B F) by (forward_using lemma_betweennotequal).
assert (Cong A D B E) by (conclude lemma_congruencesymmetric).
let Tf:=fresh in
assert (Tf:∃ G, (BetS A G D ∧ Cong A G B F)) by (conclude proposition_03);destruct Tf as [G];spliter.
assert (Cong G D F E) by (conclude lemma_differenceofparts).
assert (Cong E F D G) by (forward_using lemma_doublereverse).
assert (Cong F B G A) by (forward_using lemma_doublereverse).
assert (Cong G A F B) by (conclude lemma_congruencesymmetric).
assert (Cong E A D B) by (forward_using lemma_congruenceflip).
assert (Cong B A A B) by (conclude cn_equalityreverse).
assert (BetS D G A) by (conclude axiom_betweennesssymmetry).
assert (Cong F A G B) by (conclude lemma_interior5).
assert (Cong A F B G) by (forward_using lemma_congruenceflip).
assert (Cong B F A G) by (forward_using lemma_congruenceflip).
assert (Cong E D D E) by (conclude cn_equalityreverse).
assert (Cong F D G E) by (conclude lemma_interior5).
assert (BetS B G E) by (conclude lemma_betweennesspreserved).
assert (neq A E) by (conclude lemma_nullsegment3).
assert (Cong A B B D) by (conclude lemma_congruencesymmetric).
assert (neq B D) by (conclude lemma_nullsegment3).
assert (BetS E G B) by (conclude axiom_betweennesssymmetry).
assert (¬ Col A D E).
 {
 intro.
 assert (Col C A E) by (conclude_def Col ).
 assert (Col A E D) by (forward_using lemma_collinearorder).
 assert (Col A E C) by (forward_using lemma_collinearorder).
 assert (neq A E) by (forward_using lemma_betweennotequal).
 assert (Col E D C) by (conclude lemma_collinear4).
 assert (Col E C D) by (forward_using lemma_collinearorder).
 assert (Col E C A) by (forward_using lemma_collinearorder).
 assert (neq C E) by (forward_using lemma_betweennotequal).
 assert (neq E C) by (conclude lemma_inequalitysymmetric).
 assert (Col C D A) by (conclude lemma_collinear4).
 assert (Col C B D) by (conclude_def Col ).
 assert (Col D C A) by (forward_using lemma_collinearorder).
 assert (Col D C B) by (forward_using lemma_collinearorder).
 assert (neq C D) by (forward_using lemma_betweennotequal).
 assert (neq D C) by (conclude lemma_inequalitysymmetric).
 assert (Col C A B) by (conclude lemma_collinear4).
 assert (Col A B C) by (forward_using lemma_collinearorder).
 contradict.
 }
assert (¬ Col A D B).
 {
 intro.
 assert (Col D B A) by (forward_using lemma_collinearorder).
 assert (Col C B D) by (conclude_def Col ).
 assert (Col D B C) by (forward_using lemma_collinearorder).
 assert (neq B D) by (forward_using lemma_betweennotequal).
 assert (neq D B) by (conclude lemma_inequalitysymmetric).
 assert (Col B A C) by (conclude lemma_collinear4).
 assert (Col A B C) by (forward_using lemma_collinearorder).
 contradict.
 }
assert (Cut A D E B G) by (conclude_def Cut ).
assert (Cut A D E B F) by (conclude_def Cut ).
assert (¬ Col D E B).
 {
 intro.
 assert (Col C B D) by (conclude_def Col ).
 assert (Col D B C) by (forward_using lemma_collinearorder).
 assert (Col D B E) by (forward_using lemma_collinearorder).
 assert (neq B D) by (forward_using lemma_betweennotequal).
 assert (neq D B) by (conclude lemma_inequalitysymmetric).
 assert (Col B C E) by (conclude lemma_collinear4).
 assert (Col C A E) by (conclude_def Col ).
 assert (Col E C A) by (forward_using lemma_collinearorder).
 assert (Col E C B) by (forward_using lemma_collinearorder).
 assert (neq C E) by (forward_using lemma_betweennotequal).
 assert (neq E C) by (conclude lemma_inequalitysymmetric).
 assert (Col C A B) by (conclude lemma_collinear4).
 assert (Col A B C) by (forward_using lemma_collinearorder).
 contradict.
 }
assert (eq G F) by (conclude lemma_twolines).
assert (Cong A F B F) by (conclude cn_equalitysub).
assert (Cong F A F B) by (forward_using lemma_congruenceflip).
assert (Cong C M C M) by (conclude cn_congruencereflexive).
assert (Cong M F M F) by (conclude cn_congruencereflexive).
assert (Cong M A M B) by (conclude lemma_interior5).
close.
Qed.

End Euclid.