Require Export GeoCoq.Elements.OriginalProofs.lemma_NCorder.
Require Export GeoCoq.Elements.OriginalProofs.lemma_oppositesidesymmetric.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_crossimpliesopposite : 
   forall A B C D, 
   CR A B C D -> nCol A C D ->
   TS A C D B /\ TS A D C B /\ TS B C D A /\ TS B D C A.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @CR Ax0 A B C D) (_ : @nCol Ax0 A C D), and (@TS Ax0 A C D B) (and (@TS Ax0 A D C B) (and (@TS Ax0 B C D A) (@TS Ax0 B D C A))) *)
intros.
let Tf:=fresh in
assert (Tf:exists M, (BetS A M B /\ BetS C M D)) by (conclude_def CR );destruct Tf as [M];spliter.
(* Goal: and (@TS Ax0 A C D B) (and (@TS Ax0 A D C B) (and (@TS Ax0 B C D A) (@TS Ax0 B D C A))) *)
assert (Col C M D) by (conclude_def Col ).
(* Goal: and (@TS Ax0 A C D B) (and (@TS Ax0 A D C B) (and (@TS Ax0 B C D A) (@TS Ax0 B D C A))) *)
assert (Col C D M) by (forward_using lemma_collinearorder).
(* Goal: and (@TS Ax0 A C D B) (and (@TS Ax0 A D C B) (and (@TS Ax0 B C D A) (@TS Ax0 B D C A))) *)
assert (nCol C D A) by (forward_using lemma_NCorder).
(* Goal: and (@TS Ax0 A C D B) (and (@TS Ax0 A D C B) (and (@TS Ax0 B C D A) (@TS Ax0 B D C A))) *)
assert (nCol D C A) by (forward_using lemma_NCorder).
(* Goal: and (@TS Ax0 A C D B) (and (@TS Ax0 A D C B) (and (@TS Ax0 B C D A) (@TS Ax0 B D C A))) *)
assert (TS A C D B) by (conclude_def TS ).
(* Goal: and (@TS Ax0 A C D B) (and (@TS Ax0 A D C B) (and (@TS Ax0 B C D A) (@TS Ax0 B D C A))) *)
assert (Col D C M) by (forward_using lemma_collinearorder).
(* Goal: and (@TS Ax0 A C D B) (and (@TS Ax0 A D C B) (and (@TS Ax0 B C D A) (@TS Ax0 B D C A))) *)
assert (TS A D C B) by (conclude_def TS ).
(* Goal: and (@TS Ax0 A C D B) (and (@TS Ax0 A D C B) (and (@TS Ax0 B C D A) (@TS Ax0 B D C A))) *)
assert (TS B C D A) by (conclude lemma_oppositesidesymmetric).
(* Goal: and (@TS Ax0 A C D B) (and (@TS Ax0 A D C B) (and (@TS Ax0 B C D A) (@TS Ax0 B D C A))) *)
assert (TS B D C A) by (conclude lemma_oppositesidesymmetric).
(* Goal: and (@TS Ax0 A C D B) (and (@TS Ax0 A D C B) (and (@TS Ax0 B C D A) (@TS Ax0 B D C A))) *)
close.
Qed.

End Euclid.


