Require Export GeoCoq.Elements.OriginalProofs.lemma_crisscross.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_30helper : 
   forall A B E F G H, 
   Par A B E F -> BetS A G B -> BetS E H F -> ~ CR A F G H ->
   CR A E G H.
Proof.
(* Goal: forall (A B E F G H : @Point Ax) (_ : @Par Ax A B E F) (_ : @BetS Ax A G B) (_ : @BetS Ax E H F) (_ : not (@CR Ax A F G H)), @CR Ax A E G H *)
intros.
(* Goal: @CR Ax A E G H *)
assert (Col A G B) by (conclude_def Col ).
(* Goal: @CR Ax A E G H *)
assert (Col E H F) by (conclude_def Col ).
(* Goal: @CR Ax A E G H *)
assert (Col B A G) by (forward_using lemma_collinearorder).
(* Goal: @CR Ax A E G H *)
assert (Col E F H) by (forward_using lemma_collinearorder).
(* Goal: @CR Ax A E G H *)
assert (neq H F) by (forward_using lemma_betweennotequal).
(* Goal: @CR Ax A E G H *)
assert (neq E H) by (forward_using lemma_betweennotequal).
(* Goal: @CR Ax A E G H *)
assert (neq H E) by (conclude lemma_inequalitysymmetric).
(* Goal: @CR Ax A E G H *)
assert (neq F H) by (conclude lemma_inequalitysymmetric).
(* Goal: @CR Ax A E G H *)
assert (neq A G) by (forward_using lemma_betweennotequal).
(* Goal: @CR Ax A E G H *)
assert (neq G A) by (conclude lemma_inequalitysymmetric).
(* Goal: @CR Ax A E G H *)
assert (Par A B F E) by (forward_using lemma_parallelflip).
(* Goal: @CR Ax A E G H *)
assert (Col F E H) by (forward_using lemma_collinearorder).
(* Goal: @CR Ax A E G H *)
assert (Par A B H E) by (conclude lemma_collinearparallel).
(* Goal: @CR Ax A E G H *)
assert (Par A B H F) by (conclude lemma_collinearparallel).
(* Goal: @CR Ax A E G H *)
assert (Par H F A B) by (conclude lemma_parallelsymmetric).
(* Goal: @CR Ax A E G H *)
assert (Par H F B A) by (forward_using lemma_parallelflip).
(* Goal: @CR Ax A E G H *)
assert (Par H F G A) by (conclude lemma_collinearparallel).
(* Goal: @CR Ax A E G H *)
assert (Par H F A G) by (forward_using lemma_parallelflip).
(* Goal: @CR Ax A E G H *)
assert (Par A G H F) by (conclude lemma_parallelsymmetric).
(* Goal: @CR Ax A E G H *)
assert (Par A G F H) by (forward_using lemma_parallelflip).
(* Goal: @CR Ax A E G H *)
assert (CR A H F G) by (conclude lemma_crisscross).
let Tf:=fresh in
assert (Tf:exists M, (BetS A M H /\ BetS F M G)) by (conclude_def CR );destruct Tf as [M];spliter.
(* Goal: @CR Ax A E G H *)
assert (neq A H) by (forward_using lemma_betweennotequal).
(* Goal: @CR Ax A E G H *)
assert (neq F G) by (forward_using lemma_betweennotequal).
(* Goal: @CR Ax A E G H *)
assert (BetS G M F) by (conclude axiom_betweennesssymmetry).
(* Goal: @CR Ax A E G H *)
assert (nCol A E F) by (forward_using lemma_parallelNC).
(* Goal: @CR Ax A E G H *)
assert (nCol F E A) by (forward_using lemma_NCorder).
(* Goal: @CR Ax A E G H *)
assert (BetS F H E) by (conclude axiom_betweennesssymmetry).
let Tf:=fresh in
assert (Tf:exists p, (BetS A p E /\ BetS F M p)) by (conclude postulate_Pasch_outer);destruct Tf as [p];spliter.
(* Goal: @CR Ax A E G H *)
assert (nCol A G H) by (forward_using lemma_parallelNC).
(* Goal: @CR Ax A E G H *)
assert (nCol A H G) by (forward_using lemma_NCorder).
(* Goal: @CR Ax A E G H *)
assert (Col F M G) by (conclude_def Col ).
(* Goal: @CR Ax A E G H *)
assert (Col F M p) by (conclude_def Col ).
(* Goal: @CR Ax A E G H *)
assert (neq F M) by (forward_using lemma_betweennotequal).
(* Goal: @CR Ax A E G H *)
assert (Col M G p) by (conclude lemma_collinear4).
(* Goal: @CR Ax A E G H *)
assert (Col M p G) by (forward_using lemma_collinearorder).
(* Goal: @CR Ax A E G H *)
assert (Col M p F) by (forward_using lemma_collinearorder).
(* Goal: @CR Ax A E G H *)
assert (neq M p) by (forward_using lemma_betweennotequal).
(* Goal: @CR Ax A E G H *)
assert (Col p G F) by (conclude lemma_collinear4).
(* Goal: @CR Ax A E G H *)
assert (Col G F p) by (forward_using lemma_collinearorder).
(* Goal: @CR Ax A E G H *)
assert (Col H F E) by (forward_using lemma_collinearorder).
(* Goal: @CR Ax A E G H *)
assert (neq A B) by (forward_using lemma_betweennotequal).
(* Goal: @CR Ax A E G H *)
assert (neq A G) by (forward_using lemma_betweennotequal).
(* Goal: @CR Ax A E G H *)
assert (neq E F) by (forward_using lemma_betweennotequal).
(* Goal: @CR Ax A E G H *)
assert (neq F E) by (conclude lemma_inequalitysymmetric).
(* Goal: @CR Ax A E G H *)
assert (~ Meet A B H E) by (conclude_def Par ).
(* Goal: @CR Ax A E G H *)
assert (BetS G p F) by (conclude lemma_collinearbetween).
(* Goal: @CR Ax A E G H *)
assert (BetS F p G) by (conclude axiom_betweennesssymmetry).
(* Goal: @CR Ax A E G H *)
assert (BetS M p G) by (conclude lemma_3_6a).
(* Goal: @CR Ax A E G H *)
assert (BetS G p M) by (conclude axiom_betweennesssymmetry).
(* Goal: @CR Ax A E G H *)
assert (nCol A G H) by (forward_using lemma_parallelNC).
(* Goal: @CR Ax A E G H *)
assert (nCol A H G) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:exists m, (BetS G m H /\ BetS A p m)) by (conclude postulate_Pasch_outer);destruct Tf as [m];spliter.
(* Goal: @CR Ax A E G H *)
assert (Col A p m) by (conclude_def Col ).
(* Goal: @CR Ax A E G H *)
assert (Col A p E) by (conclude_def Col ).
(* Goal: @CR Ax A E G H *)
assert (neq A p) by (forward_using lemma_betweennotequal).
(* Goal: @CR Ax A E G H *)
assert (Col p m E) by (conclude lemma_collinear4).
(* Goal: @CR Ax A E G H *)
assert (Col p m A) by (forward_using lemma_collinearorder).
(* Goal: @CR Ax A E G H *)
assert (neq p m) by (forward_using lemma_betweennotequal).
(* Goal: @CR Ax A E G H *)
assert (Col m E A) by (conclude lemma_collinear4).
(* Goal: @CR Ax A E G H *)
assert (Col A E m) by (forward_using lemma_collinearorder).
(* Goal: @CR Ax A E G H *)
assert (neq A E) by (forward_using lemma_NCdistinct).
(* Goal: @CR Ax A E G H *)
assert (neq G H) by (forward_using lemma_NCdistinct).
(* Goal: @CR Ax A E G H *)
assert (neq G B) by (forward_using lemma_betweennotequal).
(* Goal: @CR Ax A E G H *)
assert (neq B G) by (conclude lemma_inequalitysymmetric).
(* Goal: @CR Ax A E G H *)
assert (Par H F B G) by (conclude lemma_collinearparallel).
(* Goal: @CR Ax A E G H *)
assert (Par B G H F) by (conclude lemma_parallelsymmetric).
(* Goal: @CR Ax A E G H *)
assert (Par G B F H) by (forward_using lemma_parallelflip).
(* Goal: @CR Ax A E G H *)
assert (~ Meet G B F H) by (conclude_def Par ).
(* Goal: @CR Ax A E G H *)
assert (Col G A B) by (forward_using lemma_collinearorder).
(* Goal: @CR Ax A E G H *)
assert (BetS A m E) by (conclude lemma_collinearbetween).
(* Goal: @CR Ax A E G H *)
assert (CR A E G H) by (conclude_def CR ).
(* Goal: @CR Ax A E G H *)
close.
Qed.

End Euclid.


