Require Export GeoCoq.Elements.OriginalProofs.lemma_NChelper.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NCorder.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_parallelcollinear2 : 
   forall A B C c d, 
   TP A B c d -> BetS c C d ->
   TP A B C d.
Proof.
(* Goal: forall (A B C c d : @Point Ax0) (_ : @TP Ax0 A B c d) (_ : @BetS Ax0 c C d), @TP Ax0 A B C d *)
intros.
(* Goal: @TP Ax0 A B C d *)
assert (BetS d C c) by (conclude axiom_betweennesssymmetry).
(* Goal: @TP Ax0 A B C d *)
assert ((neq A B /\ neq c d /\ ~ Meet A B c d /\ OS c d A B)) by (conclude_def TP ).
let Tf:=fresh in
assert (Tf:exists p q r, (Col A B p /\ Col A B r /\ BetS c p q /\ BetS d r q /\ nCol A B c /\ nCol A B d)) by (conclude_def OS );destruct Tf as [p[q[r]]];spliter.
(* Goal: False *)
assert (neq C d) by (forward_using lemma_betweennotequal).
(* Goal: @TP Ax0 A B C d *)
assert (BetS q p c) by (conclude axiom_betweennesssymmetry).
(* Goal: @TP Ax0 A B C d *)
assert (BetS q r d) by (conclude axiom_betweennesssymmetry).
(* Goal: @TP Ax0 A B C d *)
assert (BetS d C c) by (conclude axiom_betweennesssymmetry).
(* Goal: @TP Ax0 A B C d *)
assert (BetS q p c) by (conclude axiom_betweennesssymmetry).
(* Goal: @TP Ax0 A B C d *)
assert (Col q p c) by (conclude_def Col ).
(* Goal: @TP Ax0 A B C d *)
assert (~ eq p r).
(* Goal: not (@Meet Ax0 A B C d) *)
(* Goal: @TP Ax0 A B C d *)
 {
(* Goal: not (@Meet Ax0 A B C d) *)
 intro.
(* Goal: @TP Ax0 A B C d *)
 assert (Col q r d) by (conclude_def Col ).
(* Goal: @TP Ax0 A B C d *)
 assert (Col q p c) by (conclude_def Col ).
(* Goal: False *)
 assert (Col q p d) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (neq q p) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col p c d) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col c d p) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Meet A B c d) by (conclude_def Meet ).
(* Goal: False *)
 contradict.
 }
(* Goal: @TP Ax0 A B C d *)
assert (nCol p r c) by (conclude lemma_NChelper).
(* Goal: @TP Ax0 A B C d *)
assert (nCol p r d) by (conclude lemma_NChelper).
(* Goal: @TP Ax0 A B C d *)
assert (nCol r d p) by (forward_using lemma_NCorder).
(* Goal: @TP Ax0 A B C d *)
assert (Col q r d) by (conclude_def Col ).
(* Goal: @TP Ax0 A B C d *)
assert (Col r d q) by (forward_using lemma_collinearorder).
(* Goal: @TP Ax0 A B C d *)
assert (eq d d) by (conclude cn_equalityreflexive).
(* Goal: @TP Ax0 A B C d *)
assert (Col r d d) by (conclude_def Col ).
(* Goal: @TP Ax0 A B C d *)
assert (neq q d) by (forward_using lemma_betweennotequal).
(* Goal: @TP Ax0 A B C d *)
assert (nCol q d p) by (conclude lemma_NChelper).
(* Goal: @TP Ax0 A B C d *)
assert (nCol q p d) by (forward_using lemma_NCorder).
(* Goal: @TP Ax0 A B C d *)
assert (Col q p c) by (conclude_def Col ).
(* Goal: @TP Ax0 A B C d *)
assert (eq c c) by (conclude cn_equalityreflexive).
(* Goal: @TP Ax0 A B C d *)
assert (~ eq c p).
(* Goal: not (@Meet Ax0 A B C d) *)
(* Goal: @TP Ax0 A B C d *)
 {
(* Goal: not (@Meet Ax0 A B C d) *)
 intro.
(* Goal: False *)
 assert (eq p c) by (conclude lemma_equalitysymmetric).
(* Goal: False *)
 assert (Col p r c) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @TP Ax0 A B C d *)
assert (eq p p) by (conclude cn_equalityreflexive).
(* Goal: @TP Ax0 A B C d *)
assert (Col q p p) by (conclude_def Col ).
(* Goal: @TP Ax0 A B C d *)
assert (nCol c p d) by (conclude lemma_NChelper).
(* Goal: @TP Ax0 A B C d *)
assert (Col c p q) by (forward_using lemma_collinearorder).
(* Goal: @TP Ax0 A B C d *)
assert (eq c c) by (conclude cn_equalityreflexive).
(* Goal: @TP Ax0 A B C d *)
assert (Col c p c) by (conclude_def Col ).
(* Goal: @TP Ax0 A B C d *)
assert (neq q c) by (forward_using lemma_betweennotequal).
(* Goal: @TP Ax0 A B C d *)
assert (nCol q c d) by (conclude lemma_NChelper).
(* Goal: @TP Ax0 A B C d *)
assert (BetS q p c) by (conclude axiom_betweennesssymmetry).
let Tf:=fresh in
assert (Tf:exists E, (BetS q E C /\ BetS d E p)) by (conclude postulate_Pasch_inner);destruct Tf as [E];spliter.
(* Goal: @TP Ax0 A B C d *)
assert (BetS p E d) by (conclude axiom_betweennesssymmetry).
(* Goal: @TP Ax0 A B C d *)
assert (BetS q r d) by (conclude axiom_betweennesssymmetry).
let Tf:=fresh in
assert (Tf:exists F, (BetS q F E /\ BetS p F r)) by (conclude postulate_Pasch_inner);destruct Tf as [F];spliter.
(* Goal: @TP Ax0 A B C d *)
assert (Col p r F) by (conclude_def Col ).
(* Goal: @TP Ax0 A B C d *)
assert (Col B r p) by (conclude lemma_collinear4).
(* Goal: False *)
assert (Col B A p) by (forward_using lemma_collinearorder).
(* Goal: False *)
assert (Col B A r) by (forward_using lemma_collinearorder).
(* Goal: @TP Ax0 A B C d *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
(* Goal: @TP Ax0 A B C d *)
assert (Col B p r) by (forward_using lemma_collinearorder).
(* Goal: @TP Ax0 A B C d *)
assert (Col B p A) by (forward_using lemma_collinearorder).
(* Goal: @TP Ax0 A B C d *)
assert (~ Col A B C).
(* Goal: not (@Meet Ax0 A B C d) *)
(* Goal: @TP Ax0 A B C d *)
 {
(* Goal: not (@Meet Ax0 A B C d) *)
 intro.
(* Goal: False *)
 assert (Col c C d) by (conclude_def Col ).
(* Goal: False *)
 assert (Col c d C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Meet A B c d) by (conclude_def Meet ).
(* Goal: False *)
 contradict.
 }
(* Goal: @TP Ax0 A B C d *)
assert (BetS q F C) by (conclude lemma_3_6b).
(* Goal: @TP Ax0 A B C d *)
assert (BetS C F q) by (conclude axiom_betweennesssymmetry).
(* Goal: @TP Ax0 A B C d *)
assert (~ ~ OS C d A B).
(* Goal: not (@Meet Ax0 A B C d) *)
(* Goal: @TP Ax0 A B C d *)
 {
(* Goal: not (@Meet Ax0 A B C d) *)
 intro.
(* Goal: False *)
 assert (~ neq B p).
(* Goal: not (@Meet Ax0 A B C d) *)
(* Goal: @TP Ax0 A B C d *)
  {
(* Goal: not (@Meet Ax0 A B C d) *)
  intro.
(* Goal: False *)
  assert (Col p r A) by (conclude lemma_collinear4).
(* Goal: False *)
  assert (Col A p r) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (Col A p B) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (~ neq A p).
(* Goal: not (@Meet Ax0 A B C d) *)
(* Goal: @TP Ax0 A B C d *)
   {
(* Goal: not (@Meet Ax0 A B C d) *)
   intro.
(* Goal: False *)
   assert (Col p r B) by (conclude lemma_collinear4).
(* Goal: False *)
   assert (Col A B F) by (conclude lemma_collinear5).
(* Goal: False *)
   assert (OS C d A B) by (conclude_def OS ).
(* Goal: False *)
   contradict.
   }
(* Goal: False *)
  assert (Col A r F) by (conclude cn_equalitysub).
(* Goal: False *)
  assert (Col r A F) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (Col r A B) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (~ eq r A).
(* Goal: not (@Meet Ax0 A B C d) *)
(* Goal: @TP Ax0 A B C d *)
   {
(* Goal: not (@Meet Ax0 A B C d) *)
   intro.
(* Goal: False *)
   assert (eq r p) by (conclude cn_equalitysub).
(* Goal: False *)
   assert (neq p r) by (forward_using lemma_betweennotequal).
(* Goal: False *)
   assert (neq r p) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
   contradict.
   }
(* Goal: False *)
  assert (Col A F B) by (conclude lemma_collinear4).
(* Goal: False *)
  assert (Col A B F) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (OS C d A B) by (conclude_def OS ).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (neq A p) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (Col A p B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: False *)
 assert (Col B A A) by (conclude_def Col ).
(* Goal: False *)
 assert (Col B A p) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col B A r) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col A p r) by (conclude lemma_collinear5).
(* Goal: False *)
 assert (Col p B r) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col p r B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col p r A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col A B F) by (conclude lemma_collinear5).
(* Goal: False *)
 assert (OS C d A B) by (conclude_def OS ).
(* Goal: False *)
 contradict.
 }
(* Goal: @TP Ax0 A B C d *)
assert (~ Meet A B C d).
(* Goal: not (@Meet Ax0 A B C d) *)
(* Goal: @TP Ax0 A B C d *)
 {
(* Goal: not (@Meet Ax0 A B C d) *)
 intro.
 let Tf:=fresh in
 assert (Tf:exists R, (neq A B /\ neq C d /\ Col A B R /\ Col C d R)) by (conclude_def Meet );destruct Tf as [R];spliter.
(* Goal: False *)
 assert (Col c C d) by (conclude_def Col ).
(* Goal: False *)
 assert (Col C d c) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq C d) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col d c R) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col c d R) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Meet A B c d) by (conclude_def Meet ).
(* Goal: False *)
 contradict.
 }
(* Goal: @TP Ax0 A B C d *)
assert (TP A B C d) by (conclude_def TP ).
(* Goal: @TP Ax0 A B C d *)
close.
Qed.

End Euclid.


