Library GeoCoq.Elements.OriginalProofs.proposition_07

Require Export GeoCoq.Elements.OriginalProofs.proposition_12.
Require Export GeoCoq.Elements.OriginalProofs.lemma_samesidesymmetric.
Require Export GeoCoq.Elements.OriginalProofs.lemma_planeseparation.
Require Export GeoCoq.Elements.OriginalProofs.lemma_droppedperpendicularunique.
Require Export GeoCoq.Elements.OriginalProofs.lemma_fiveline.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_07 :
   ∀ A B C D,
   neq A B → Cong C A D A → Cong C B D B → OS C D A B →
   eq C D.
Proof.
intros.
assert (nCol A B C) by (conclude_def OS ).
let Tf:=fresh in
assert (Tf:∃ F, Perp_at C F A B F) by (conclude proposition_12);destruct Tf as [F];spliter.
rename_H H;
let Tf:=fresh in
assert (Tf:∃ H, (Col C F F ∧ Col A B F ∧ Col A B H ∧ Per H F C)) by (conclude_def Perp_at );destruct Tf as [H];spliter.
assert (¬ eq C F).
 {
 intro.
 assert (Col A B C) by (conclude cn_equalitysub).
 contradict.
 }
assert (neq F C) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ E, (BetS C F E ∧ Cong F E F C)) by (conclude postulate_extension);destruct Tf as [E];spliter.
assert (Cong A C A E).
by cases on (eq A F ∨ neq A F).
{
 assert (Cong A E A C) by (conclude cn_equalitysub).
 assert (Cong A C A E) by (conclude lemma_congruencesymmetric).
 close.
 }
{
 assert (neq B A) by (conclude lemma_inequalitysymmetric).
 assert (Col B A F) by (forward_using lemma_collinearorder).
 assert (Col B A H) by (forward_using lemma_collinearorder).
 assert (Col A F H) by (conclude lemma_collinear4).
 assert (Col H F A) by (forward_using lemma_collinearorder).
 assert (Per A F C) by (conclude lemma_collinearright).
 assert (Per C F A) by (conclude lemma_8_2).
 let Tf:=fresh in
 assert (Tf:∃ P, (BetS C F P ∧ Cong C F P F ∧ Cong C A P A ∧ neq F A)) by (conclude_def Per );destruct Tf as [P];spliter.
 assert (Cong F E C F) by (forward_using lemma_congruenceflip).
 assert (Cong F E P F) by (conclude lemma_congruencetransitive).
 assert (Cong F E F P) by (forward_using lemma_congruenceflip).
 assert (eq E P) by (conclude lemma_extensionunique).
 assert (Cong C A E A) by (conclude cn_equalitysub).
 assert (Cong A C A E) by (forward_using lemma_congruenceflip).
 close.
 }

assert (Cong B C B E).
by cases on (eq B F ∨ neq B F).
{
 assert (Cong B E B C) by (conclude cn_equalitysub).
 assert (Cong B C B E) by (conclude lemma_congruencesymmetric).
 close.
 }
{
 assert (Col B A F) by (forward_using lemma_collinearorder).
 assert (Col B A H) by (forward_using lemma_collinearorder).
 assert (Col A B F) by (forward_using lemma_collinearorder).
 assert (Col A B H) by (forward_using lemma_collinearorder).
 assert (Col B F H) by (conclude lemma_collinear4).
 assert (Col H F B) by (forward_using lemma_collinearorder).
 assert (Per B F C) by (conclude lemma_collinearright).
 assert (Per C F B) by (conclude lemma_8_2).
 let Tf:=fresh in
 assert (Tf:∃ P, (BetS C F P ∧ Cong C F P F ∧ Cong C B P B ∧ neq F B)) by (conclude_def Per );destruct Tf as [P];spliter.
 assert (Cong F E C F) by (forward_using lemma_congruenceflip).
 assert (Cong F E P F) by (conclude lemma_congruencetransitive).
 assert (Cong F E F P) by (forward_using lemma_congruenceflip).
 assert (eq E P) by (conclude lemma_extensionunique).
 assert (Cong C B E B) by (conclude cn_equalitysub).
 assert (Cong B C B E) by (forward_using lemma_congruenceflip).
 close.
 }

assert (TS C A B E) by (conclude_def TS ).
assert (OS D C A B) by (forward_using lemma_samesidesymmetric).
assert (TS D A B E) by (conclude lemma_planeseparation).
let Tf:=fresh in
assert (Tf:∃ G, (BetS D G E ∧ Col A B G ∧ nCol A B D)) by (conclude_def TS );destruct Tf as [G];spliter.
assert (Cong E A C A) by (forward_using lemma_doublereverse).
assert (Cong A E C A) by (forward_using lemma_congruenceflip).
assert (Cong A E D A) by (conclude lemma_congruencetransitive).
assert (Cong A E A D) by (forward_using lemma_congruenceflip).
assert (Cong A D A E) by (conclude lemma_congruencesymmetric).
assert (Cong B D B C) by (forward_using lemma_doublereverse).
assert (Cong B D B E) by (conclude lemma_congruencetransitive).
assert (Cong A G A G) by (conclude cn_congruencereflexive).
assert (Cong G B G B) by (conclude cn_congruencereflexive).
assert ((eq A B ∨ eq A G ∨ eq B G ∨ BetS B A G ∨ BetS A B G ∨ BetS A G B)) by (conclude_def Col ).
assert (Cong G D G E).
by cases on (eq A B ∨ eq A G ∨ eq B G ∨ BetS B A G ∨ BetS A B G ∨ BetS A G B).
{
 assert (¬ ¬ Cong G D G E).
  {
  intro.
  contradict.
  }
 close.
 }
{
 assert (Cong A D A E) by (conclude lemma_congruencesymmetric).
 assert (Cong G D G E) by (conclude cn_equalitysub).
 close.
 }
{
 assert (Cong G D G E) by (conclude cn_equalitysub).
 close.
 }
{
 assert (Cong B A B A) by (conclude cn_congruencereflexive).
 assert (Cong A G A G) by (conclude cn_congruencereflexive).
 assert (Cong A D A E) by (conclude lemma_congruencesymmetric).
 assert (neq B A) by (conclude lemma_inequalitysymmetric).
 assert (Cong D G E G) by (conclude axiom_5_line).
 assert (Cong G D G E) by (forward_using lemma_congruenceflip).
 close.
 }
{
 assert (Cong A B A B) by (conclude cn_congruencereflexive).
 assert (Cong B G B G) by (conclude cn_congruencereflexive).
 assert (Cong D G E G) by (conclude axiom_5_line).
 assert (Cong G D G E) by (forward_using lemma_congruenceflip).
 close.
 }
{
 assert (Cong A G A G) by (conclude cn_congruencereflexive).
 assert (Cong G B G B) by (conclude cn_congruencereflexive).
 assert (Cong G D G E) by (conclude lemma_interior5).
 close.
 }

assert (Cong D A E A) by (forward_using lemma_congruenceflip).
assert (eq F G).
by cases on (eq A G ∨ neq A G).
{
 assert (neq G E) by (forward_using lemma_betweennotequal).
 assert (neq E G) by (conclude lemma_inequalitysymmetric).
 assert (BetS E G D) by (conclude axiom_betweennesssymmetry).
 assert (Cong E G D G) by (forward_using lemma_doublereverse).
 assert (Cong E B D B) by (forward_using lemma_doublereverse).
 assert (¬ eq G B).
  {
  intro.
  assert (eq A B) by (conclude cn_equalitysub).
  contradict.
  }
 assert (Per E G B) by (conclude_def Per ).
 assert (neq F E) by (forward_using lemma_betweennotequal).
 assert (neq E F) by (conclude lemma_inequalitysymmetric).
 assert (BetS E F C) by (conclude axiom_betweennesssymmetry).
 assert (Cong E F C F) by (forward_using lemma_doublereverse).
 assert (Cong E B C B) by (forward_using lemma_doublereverse).
 assert (¬ eq F B).
  {
  intro.
  assert (Cong B E B C) by (forward_using lemma_congruenceflip).
  assert (Cong B C B D) by (forward_using lemma_congruenceflip).
  assert (Cong B E B E) by (conclude lemma_congruencetransitive).
  assert (Cong A E A D) by (forward_using lemma_congruenceflip).
  assert (neq B A) by (conclude lemma_inequalitysymmetric).
  assert (BetS E A D) by (conclude cn_equalitysub).
  assert (Cong E A D A) by (forward_using lemma_congruenceflip).
  assert (Per E A B) by (conclude_def Per ).
  assert (Per B A E) by (conclude lemma_8_2).
  assert (BetS E B C) by (conclude cn_equalitysub).
  assert (Per E B A) by (conclude_def Per ).
  assert (Per A B E) by (conclude lemma_8_2).
  let Tf:=fresh in
  assert (Tf:∃ J, (BetS B A J ∧ Cong A J A B)) by (conclude postulate_extension);destruct Tf as [J];spliter.
  assert (Out B A J) by (conclude lemma_ray4).
  assert (Per E B J) by (conclude lemma_8_3).
  assert (Per J B E) by (conclude lemma_8_2).
  assert (Col A B J) by (conclude_def Col ).
  assert (Col B A J) by (forward_using lemma_collinearorder).
  assert (Per B A E) by (conclude lemma_8_2).
  assert (neq A J) by (forward_using lemma_betweennotequal).
  assert (neq J A) by (conclude lemma_inequalitysymmetric).
  assert (Per J A E) by (conclude lemma_collinearright).
  assert (Col B A J) by (conclude_def Col ).
  assert (Col J A B) by (forward_using lemma_collinearorder).
  assert (eq A B) by (conclude lemma_droppedperpendicularunique).
  contradict.
  }
 assert (Per E F B) by (conclude_def Per ).
 assert (Per B G E) by (conclude lemma_8_2).
 assert (Per B F E) by (conclude lemma_8_2).
 assert (Col B G F) by (conclude lemma_collinear4).
 assert (eq G F) by (conclude lemma_droppedperpendicularunique).
 assert (eq F G) by (conclude lemma_equalitysymmetric).
 close.
 }
{
 assert (eq F G).
 by cases on (eq A F ∨ neq A F).
 {
  assert (neq F B) by (conclude cn_equalitysub).
  assert (Cong E F C F) by (forward_using lemma_congruenceflip).
  assert (Cong E B C B) by (forward_using lemma_doublereverse).
  assert (BetS E F C) by (conclude axiom_betweennesssymmetry).
  assert (Per E F B) by (conclude_def Per ).
  assert (Per B F E) by (conclude lemma_8_2).
  assert (¬ eq B G).
   {
   intro.
   assert (eq F A) by (conclude lemma_equalitysymmetric).
   assert (Cong A E A C) by (forward_using lemma_congruenceflip).
   assert (Cong A C A D) by (forward_using lemma_congruenceflip).
   assert (Cong A E A D) by (conclude lemma_congruencetransitive).
   assert (Cong B E B D) by (conclude lemma_congruencesymmetric).
   assert (BetS E G D) by (conclude axiom_betweennesssymmetry).
   assert (BetS E B D) by (conclude cn_equalitysub).
   assert (Cong E B D B) by (forward_using lemma_congruenceflip).
   assert (Cong E A D A) by (conclude lemma_congruencesymmetric).
   assert (neq B A) by (conclude lemma_inequalitysymmetric).
   assert (Per E B A) by (conclude_def Per ).
   assert (Per A B E) by (conclude lemma_8_2).
   assert (BetS E A C) by (conclude cn_equalitysub).
   assert (Per E A B) by (conclude_def Per ).
   assert (Per B A E) by (conclude lemma_8_2).
   let Tf:=fresh in
   assert (Tf:∃ K, (BetS A B K ∧ Cong B K B A)) by (conclude postulate_extension);destruct Tf as [K];spliter.
   assert (Out A B K) by (conclude lemma_ray4).
   assert (Per E A K) by (conclude lemma_8_3).
   assert (Per K A E) by (conclude lemma_8_2).
   assert (Col B A K) by (conclude_def Col ).
   assert (Col A B K) by (forward_using lemma_collinearorder).
   assert (Per A B E) by (conclude lemma_8_2).
   assert (neq B K) by (forward_using lemma_betweennotequal).
   assert (neq K B) by (conclude lemma_inequalitysymmetric).
   assert (Per K B E) by (conclude lemma_collinearright).
   assert (Col A B K) by (conclude_def Col ).
   assert (Col K B A) by (forward_using lemma_collinearorder).
   assert (eq B A) by (conclude lemma_droppedperpendicularunique).
   assert (neq B A) by (conclude lemma_inequalitysymmetric).
   contradict.
   }
  assert (neq G B) by (conclude lemma_inequalitysymmetric).
  assert (Cong E G D G) by (forward_using lemma_doublereverse).
  assert (Cong E B D B) by (forward_using lemma_doublereverse).
  assert (BetS E G D) by (conclude axiom_betweennesssymmetry).
  assert (Per E G B) by (conclude_def Per ).
  assert (Per B G E) by (conclude lemma_8_2).
  assert (Col F B G) by (conclude cn_equalitysub).
  assert (Col B G F) by (forward_using lemma_collinearorder).
  assert (eq G F) by (conclude lemma_droppedperpendicularunique).
  assert (eq F G) by (conclude lemma_equalitysymmetric).
  close.
  }
 {
  assert (neq F A) by (conclude lemma_inequalitysymmetric).
  assert (Cong E F C F) by (forward_using lemma_doublereverse).
  assert (BetS E F C) by (conclude axiom_betweennesssymmetry).
  assert (Per E F A) by (conclude_def Per ).
  assert (Per A F E) by (conclude lemma_8_2).
  assert (BetS E G D) by (conclude axiom_betweennesssymmetry).
  assert (Cong E G D G) by (forward_using lemma_doublereverse).
  assert (Cong E A D A) by (conclude lemma_congruencesymmetric).
  assert (neq G A) by (conclude lemma_inequalitysymmetric).
  assert (Per E G A) by (conclude_def Per ).
  assert (Per A G E) by (conclude lemma_8_2).
  assert (Col B A F) by (forward_using lemma_collinearorder).
  assert (Col B A G) by (forward_using lemma_collinearorder).
  assert (neq B A) by (conclude lemma_inequalitysymmetric).
  assert (Col A F G) by (conclude lemma_collinear4).
  assert (eq F G) by (conclude lemma_droppedperpendicularunique).
  close.
  }

 close.
 }

assert (Cong A F A F) by (conclude cn_congruencereflexive).
assert (Cong B F B F) by (conclude cn_congruencereflexive).
assert (Cong A F A G) by (conclude cn_equalitysub).
assert (Cong B F B G) by (conclude cn_equalitysub).
assert (Cong A B A B) by (conclude cn_congruencereflexive).
assert (Col A F B) by (forward_using lemma_collinearorder).
assert (Cong F B F B) by (conclude cn_congruencereflexive).
assert (Cong F B G B) by (conclude cn_equalitysub).
assert (Cong A C A D) by (forward_using lemma_congruenceflip).
assert (Cong B C B D) by (forward_using lemma_congruenceflip).
assert (Cong A B A B) by (conclude cn_congruencereflexive).
assert (Cong F C G D) by (conclude lemma_fiveline).
assert (Cong F C F D) by (conclude cn_equalitysub).
assert (BetS E F C) by (conclude axiom_betweennesssymmetry).
assert (BetS E G D) by (conclude axiom_betweennesssymmetry).
assert (BetS E F D) by (conclude cn_equalitysub).
assert (Out F D C) by (conclude_def Out ).
assert (eq D D) by (conclude cn_equalityreflexive).
assert (¬ eq F D).
 {
 intro.
 assert (Col A B F) by (forward_using lemma_collinearorder).
 assert (Col A B D) by (conclude cn_equalitysub).
 contradict.
 }
assert (Out F D D) by (conclude lemma_ray4).
assert (eq C D) by (conclude lemma_layoffunique).
close.
Qed.

End Euclid.