Library GeoCoq.Elements.OriginalProofs.proposition_31

Require Export GeoCoq.Elements.OriginalProofs.lemma_NChelper.
Require Export GeoCoq.Elements.OriginalProofs.lemma_pointreflectionisometry.
Require Export GeoCoq.Elements.OriginalProofs.lemma_oppositesidesymmetric.
Require Export GeoCoq.Elements.OriginalProofs.proposition_27.
Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelflip.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_31 :
   ∀ A B C D,
   BetS B D C → nCol B C A →
   ∃ X Y Z, BetS X A Y ∧ CongA Y A D A D B ∧ CongA Y A D B D A ∧ CongA D A Y B D A ∧ CongA X A D A D C ∧ CongA X A D C D A ∧ CongA D A X C D A ∧ Par X Y B C ∧ Cong X A D C ∧ Cong A Y B D ∧ Cong A Z Z D ∧ Cong X Z Z C ∧ Cong B Z Z Y ∧ BetS X Z C ∧ BetS B Z Y ∧ BetS A Z D.
Proof.
intros.
assert (Col B D C) by (conclude_def Col ).
assert (¬ eq A D).
 {
 intro.
 assert (Col B A C) by (conclude cn_equalitysub).
 assert (Col B C A) by (forward_using lemma_collinearorder).
 contradict.
 }
let Tf:=fresh in
assert (Tf:∃ M, (BetS A M D ∧ Cong M A M D)) by (conclude proposition_10);destruct Tf as [M];spliter.
assert (Cong A M M D) by (forward_using lemma_congruenceflip).
assert (Col A M D) by (conclude_def Col ).
assert (Col A D M) by (forward_using lemma_collinearorder).
assert (nCol A B C) by (forward_using lemma_NCorder).
assert (Col C B D) by (forward_using lemma_collinearorder).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col C B B) by (conclude_def Col ).
assert (nCol C B A) by (forward_using lemma_NCorder).
assert (neq B D) by (forward_using lemma_betweennotequal).
assert (nCol B D A) by (conclude lemma_NChelper).
assert (neq M D) by (forward_using lemma_betweennotequal).
assert (Col B D C) by (conclude_def Col ).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (Col B D D) by (conclude_def Col ).
assert (neq D C) by (forward_using lemma_betweennotequal).
assert (neq C D) by (conclude lemma_inequalitysymmetric).
assert (nCol C D A) by (conclude lemma_NChelper).
assert (nCol A D C) by (forward_using lemma_NCorder).
assert (Col A M D) by (conclude_def Col ).
assert (Col A D M) by (forward_using lemma_collinearorder).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A D A) by (conclude_def Col ).
assert (neq A M) by (forward_using lemma_betweennotequal).
assert (nCol A M C) by (conclude lemma_NChelper).
assert (¬ eq C M).
 {
 intro.
 assert (Col A C M) by (conclude_def Col ).
 assert (Col A M C) by (forward_using lemma_collinearorder).
 contradict.
 }
assert (neq M C) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ E, (BetS C M E ∧ Cong M E M C)) by (conclude postulate_extension);destruct Tf as [E];spliter.
assert (Cong M C M E) by (conclude lemma_congruencesymmetric).
assert (Cong C M M E) by (forward_using lemma_congruenceflip).
assert (Midpoint C M E) by (conclude_def Midpoint ).
assert (neq A M) by (forward_using lemma_betweennotequal).
assert (nCol A D B) by (forward_using lemma_NCorder).
assert (nCol A M B) by (conclude lemma_NChelper).
assert (¬ eq B M).
 {
 intro.
 assert (Col A B M) by (conclude_def Col ).
 assert (Col A M B) by (forward_using lemma_collinearorder).
 contradict.
 }
assert (neq M B) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ F, (BetS B M F ∧ Cong M F M B)) by (conclude postulate_extension);destruct Tf as [F];spliter.
assert (Cong M F B M) by (forward_using lemma_congruenceflip).
assert (Cong B M M F) by (conclude lemma_congruencesymmetric).
assert (Midpoint B M F) by (conclude_def Midpoint ).
assert (Cong M D M A) by (conclude lemma_congruencesymmetric).
assert (BetS D M A) by (conclude axiom_betweennesssymmetry).
assert (Cong D M M A) by (forward_using lemma_congruenceflip).
assert (Midpoint D M A) by (conclude_def Midpoint ).
assert (Cong B D F A) by (conclude lemma_pointreflectionisometry).
assert (Cong D C A E) by (conclude lemma_pointreflectionisometry).
assert (Cong B C F E) by (conclude lemma_pointreflectionisometry).
assert (BetS F A E) by (conclude lemma_betweennesspreserved).
assert (BetS E A F) by (conclude axiom_betweennesssymmetry).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (neq A F) by (forward_using lemma_betweennotequal).
assert (Out A F F) by (conclude lemma_ray4).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (neq B D) by (forward_using lemma_betweennotequal).
assert (neq D B) by (conclude lemma_inequalitysymmetric).
assert (Out D B B) by (conclude lemma_ray4).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (neq D A) by (forward_using lemma_betweennotequal).
assert (Out D A A) by (conclude lemma_ray4).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (neq A D) by (conclude lemma_inequalitysymmetric).
assert (Out A D D) by (conclude lemma_ray4).
assert (nCol B M A) by (forward_using lemma_NCorder).
assert (Col B M F) by (conclude_def Col ).
assert (eq M M) by (conclude cn_equalityreflexive).
assert (Col B M M) by (conclude_def Col ).
assert (neq M F) by (forward_using lemma_betweennotequal).
assert (neq F M) by (conclude lemma_inequalitysymmetric).
assert (nCol F M A) by (conclude lemma_NChelper).
assert (nCol A M F) by (forward_using lemma_NCorder).
assert (Col A M A) by (conclude_def Col ).
assert (Col A M D) by (conclude_def Col ).
assert (nCol A D F) by (conclude lemma_NChelper).
assert (nCol F A D) by (forward_using lemma_NCorder).
assert (Cong D B A F) by (forward_using lemma_congruenceflip).
assert (Midpoint A M D) by (conclude_def Midpoint ).
assert (Cong B A F D) by (conclude lemma_pointreflectionisometry).
assert (Cong F D B A) by (conclude lemma_congruencesymmetric).
assert (Cong A F D B) by (conclude lemma_congruencesymmetric).
assert (Cong A D D A) by (conclude cn_equalityreverse).
assert (CongA F A D B D A) by (conclude_def CongA ).
assert (Col B D C) by (conclude_def Col ).
assert (Col B C D) by (forward_using lemma_collinearorder).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col B C B) by (conclude_def Col ).
assert (nCol B D A) by (conclude lemma_NChelper).
assert (CongA B D A A D B) by (conclude lemma_ABCequalsCBA).
assert (CongA F A D A D B) by (conclude lemma_equalanglestransitive).
assert (CongA A D B F A D) by (conclude lemma_equalanglessymmetric).
assert (Col A M D) by (conclude_def Col ).
assert (Col D A M) by (forward_using lemma_collinearorder).
assert (nCol D A B) by (forward_using lemma_NCorder).
assert (Col D A A) by (conclude_def Col ).
assert (neq A M) by (forward_using lemma_betweennotequal).
assert (neq M A) by (conclude lemma_inequalitysymmetric).
assert (nCol M A B) by (conclude lemma_NChelper).
assert (nCol B M A) by (forward_using lemma_NCorder).
assert (Col B M F) by (conclude_def Col ).
assert (nCol F M A) by (conclude lemma_NChelper).
assert (nCol M A F) by (forward_using lemma_NCorder).
assert (Col M A D) by (forward_using lemma_collinearorder).
assert (nCol D A F) by (conclude lemma_NChelper).
assert (nCol F A D) by (forward_using lemma_NCorder).
assert (CongA F A D D A F) by (conclude lemma_ABCequalsCBA).
assert (CongA A D B D A F) by (conclude lemma_equalanglestransitive).
assert (CongA D A F A D B) by (conclude lemma_equalanglessymmetric).
assert (nCol A D B) by (forward_using lemma_NCorder).
assert (CongA A D B B D A) by (conclude lemma_ABCequalsCBA).
assert (CongA D A F B D A) by (conclude lemma_equalanglestransitive).
assert (TS B A D F) by (conclude_def TS ).
assert (TS F A D B) by (conclude lemma_oppositesidesymmetric).
assert (BetS C D B) by (conclude axiom_betweennesssymmetry).
assert (Par F E C B) by (conclude proposition_27).
assert (Par E F B C) by (forward_using lemma_parallelflip).
assert (Cong D C E A) by (forward_using lemma_congruenceflip).
assert (Cong E A D C) by (conclude lemma_congruencesymmetric).
assert (Cong B D A F) by (forward_using lemma_congruenceflip).
assert (Cong A F B D) by (conclude lemma_congruencesymmetric).
assert (Cong M C E M) by (forward_using lemma_congruenceflip).
assert (Cong E M M C) by (conclude lemma_congruencesymmetric).
assert (neq E A) by (forward_using lemma_betweennotequal).
assert (neq A E) by (conclude lemma_inequalitysymmetric).
assert (eq E E) by (conclude cn_equalityreflexive).
assert (Out A E E) by (conclude lemma_ray4).
assert (neq D C) by (forward_using lemma_betweennotequal).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Out D C C) by (conclude lemma_ray4).
assert (Cong E M M C) by (forward_using lemma_congruenceflip).
assert (Cong A M M D) by (forward_using lemma_congruenceflip).
assert (Cong D M M A) by (forward_using lemma_doublereverse).
assert (BetS E M C) by (conclude axiom_betweennesssymmetry).
assert (Midpoint E M C) by (conclude_def Midpoint ).
assert (Cong E D C A) by (conclude lemma_pointreflectionisometry).
assert (Cong A E D C) by (conclude lemma_pointreflectionisometry).
assert (Cong A D D A) by (conclude lemma_pointreflectionisometry).
assert (Col E A F) by (conclude_def Col ).
assert (Col F A E) by (forward_using lemma_collinearorder).
assert (Col F A A) by (conclude_def Col ).
assert (nCol E A D) by (conclude lemma_NChelper).
assert (CongA E A D C D A) by (conclude_def CongA ).
assert (nCol C D A) by (forward_using lemma_NCorder).
assert (CongA C D A A D C) by (conclude lemma_ABCequalsCBA).
assert (CongA E A D A D C) by (conclude lemma_equalanglestransitive).
assert (nCol D A E) by (forward_using lemma_NCorder).
assert (CongA D A E E A D) by (conclude lemma_ABCequalsCBA).
assert (CongA D A E C D A) by (conclude lemma_equalanglestransitive).
remove_exists;eauto 20.
Qed.

End Euclid.