Require Export GeoCoq.Elements.OriginalProofs.lemma_samesideflip.
Require Export GeoCoq.Elements.OriginalProofs.proposition_39A.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_39 : 
   forall A B C D, 
   Triangle A B C -> Triangle D B C -> OS A D B C -> ET A B C D B C -> neq A D ->
   Par A D B C.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @Triangle Ax0 A B C) (_ : @Triangle Ax0 D B C) (_ : @OS Ax0 A D B C) (_ : @ET Ax0 Ax1 Ax2 Ax A B C D B C) (_ : @neq Ax0 A D), @Par Ax0 A D B C *)
intros.
(* Goal: @Par Ax0 A D B C *)
assert (OS D A B C) by (forward_using lemma_samesidesymmetric).
(* Goal: False *)
assert (OS A D C B) by (conclude lemma_samesideflip).
(* Goal: @Par Ax0 A D B C *)
assert (OS D A C B) by (forward_using lemma_samesidesymmetric).
(* Goal: @Par Ax0 A D B C *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: @Par Ax0 A D B C *)
assert (nCol D B C) by (conclude_def Triangle ).
(* Goal: @Par Ax0 A D B C *)
assert (neq A B) by (forward_using lemma_NCdistinct).
(* Goal: @Par Ax0 A D B C *)
assert (neq B D) by (forward_using lemma_NCdistinct).
(* Goal: @Par Ax0 A D B C *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
assert (neq B C) by (forward_using lemma_NCdistinct).
(* Goal: @Par Ax0 A D B C *)
assert (neq C A) by (forward_using lemma_NCdistinct).
(* Goal: @Par Ax0 A D B C *)
assert (neq C B) by (forward_using lemma_NCdistinct).
(* Goal: @Par Ax0 A D B C *)
assert (neq C D) by (forward_using lemma_NCdistinct).
(* Goal: @Par Ax0 A D B C *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: @Par Ax0 A D B C *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: @Par Ax0 A D B C *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: @Par Ax0 A D B C *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @Par Ax0 A D B C *)
assert (Out B C C) by (conclude lemma_ray4).
(* Goal: @Par Ax0 A D B C *)
assert (Out B A A) by (conclude lemma_ray4).
(* Goal: @Par Ax0 A D B C *)
assert (Out B D D) by (conclude lemma_ray4).
(* Goal: @Par Ax0 A D B C *)
assert (Out C B B) by (conclude lemma_ray4).
(* Goal: @Par Ax0 A D B C *)
assert (Out C A A) by (conclude lemma_ray4).
(* Goal: @Par Ax0 A D B C *)
assert (Out C D D) by (conclude lemma_ray4).
(* Goal: @Par Ax0 A D B C *)
assert (~ ~ Par A D B C).
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
(* Goal: False *)
 {
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
 intro.
(* Goal: False *)
 assert (~ LtA C B D C B A).
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
(* Goal: False *)
  {
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
  intro.
  let Tf:=fresh in
  assert (Tf:exists M, (BetS A M C /\ Out B D M)) by (conclude lemma_crossbar2);destruct Tf as [M];spliter.
(* Goal: False *)
  assert (Par A D B C) by (conclude proposition_39A).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (~ LtA C B A C B D).
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
(* Goal: False *)
  {
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
  intro.
  let Tf:=fresh in
  assert (Tf:exists M, (BetS D M C /\ Out B A M)) by (conclude lemma_crossbar2);destruct Tf as [M];spliter.
(* Goal: False *)
  assert (ET D B C A B C) by (conclude axiom_ETsymmetric).
(* Goal: False *)
  assert (Par D A B C) by (conclude proposition_39A).
(* Goal: False *)
  assert (Par A D B C) by (forward_using lemma_parallelflip).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (~ ~ CongA C B D C B A).
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
(* Goal: False *)
  {
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
  intro.
(* Goal: False *)
  assert (nCol C B A) by (forward_using lemma_NCorder).
(* Goal: False *)
  assert (nCol C B D) by (forward_using lemma_NCorder).
(* Goal: False *)
  assert (LtA C B D C B A) by (conclude lemma_angletrichotomy2).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (nCol A C B) by (forward_using lemma_NCorder).
(* Goal: False *)
 assert (Triangle A C B) by (conclude_def Triangle ).
(* Goal: False *)
 assert (nCol D C B) by (forward_using lemma_NCorder).
(* Goal: False *)
 assert (Triangle D C B) by (conclude_def Triangle ).
(* Goal: False *)
 assert (OS A D C B) by (conclude lemma_samesideflip).
(* Goal: False *)
 assert (ET A B C D C B) by (forward_using axiom_ETpermutation).
(* Goal: False *)
 assert (ET D C B A B C) by (conclude axiom_ETsymmetric).
(* Goal: False *)
 assert (ET D C B A C B) by (forward_using axiom_ETpermutation).
(* Goal: False *)
 assert (ET A C B D C B) by (conclude axiom_ETsymmetric).
(* Goal: False *)
 assert (~ LtA B C D B C A).
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
(* Goal: False *)
  {
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
  intro.
  let Tf:=fresh in
  assert (Tf:exists M, (BetS A M B /\ Out C D M)) by (conclude lemma_crossbar2);destruct Tf as [M];spliter.
(* Goal: False *)
  assert (Par A D C B) by (conclude proposition_39A).
(* Goal: False *)
  assert (Par A D B C) by (forward_using lemma_parallelflip).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (~ LtA B C A B C D).
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
(* Goal: False *)
  {
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
  intro.
  let Tf:=fresh in
  assert (Tf:exists M, (BetS D M B /\ Out C A M)) by (conclude lemma_crossbar2);destruct Tf as [M];spliter.
(* Goal: False *)
  assert (ET D C B A C B) by (conclude axiom_ETsymmetric).
(* Goal: False *)
  assert (Par D A C B) by (conclude proposition_39A).
(* Goal: False *)
  assert (Par A D B C) by (forward_using lemma_parallelflip).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (~ ~ CongA B C D B C A).
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
(* Goal: False *)
  {
(* Goal: not (not (@CongA Ax0 B C D B C A)) *)
  intro.
(* Goal: False *)
  assert (nCol B C A) by (forward_using lemma_NCorder).
(* Goal: False *)
  assert (nCol B C D) by (forward_using lemma_NCorder).
(* Goal: False *)
  assert (LtA B C D B C A) by (conclude lemma_angletrichotomy2).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (CongA B C A B C D) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (Cong B C B C) by (conclude cn_congruencereflexive).
(* Goal: False *)
 assert (CongA D B C A B C) by (conclude lemma_equalanglesflip).
(* Goal: False *)
 assert (CongA A B C D B C) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert ((Cong A B D B /\ Cong A C D C /\ CongA B A C B D C)) by (conclude proposition_26A).
(* Goal: False *)
 assert (neq B C) by (forward_using lemma_NCdistinct).
(* Goal: False *)
 assert (eq A D) by (conclude proposition_07).
(* Goal: False *)
 contradict.
 }
(* Goal: @Par Ax0 A D B C *)
close.
Qed.

End Euclid.


