Require Export GeoCoq.Elements.OriginalProofs.lemma_NCorder.
Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear4.
Require Export GeoCoq.Elements.OriginalProofs.lemma_TCreflexive.

Section Euclid.

Context `{Ax:area}.

Lemma lemma_EFreflexive : 
   forall a b c d p, 
   BetS a p c -> BetS b p d -> nCol a b c ->
   EF a b c d a b c d.
Proof.
(* Goal: forall (a b c d p : @Point Ax0) (_ : @BetS Ax0 a p c) (_ : @BetS Ax0 b p d) (_ : @nCol Ax0 a b c), @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
intros.
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
assert (nCol a c b) by (forward_using lemma_NCorder).
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
assert (~ Col a c d).
(* Goal: not (@Col Ax0 a c d) *)
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
 {
(* Goal: not (@Col Ax0 a c d) *)
 intro.
(* Goal: False *)
 assert (Col b p d) by (conclude_def Col ).
(* Goal: False *)
 assert (Col a p c) by (conclude_def Col ).
(* Goal: False *)
 assert (Col a c p) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq a c) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col c d p) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col d p c) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col d p b) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq p d) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq d p) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col p c b) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col a p c) by (conclude_def Col ).
(* Goal: False *)
 assert (Col p c a) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq p c) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col c b a) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col a b c) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
assert (Triangle a c d) by (conclude_def Triangle ).
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
assert (Triangle a c b) by (conclude_def Triangle ).
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
assert (Cong_3 a c d a c d) by (conclude lemma_TCreflexive).
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
assert (Cong_3 a c b a c b) by (conclude lemma_TCreflexive).
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
assert (ET a c d a c d) by (conclude axiom_congruentequal).
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
assert (ET a c b a c b) by (conclude axiom_congruentequal).
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
assert (Col a c p) by (conclude_def Col ).
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
assert (nCol a c b) by (forward_using lemma_NCorder).
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
assert (TS b a c d) by (conclude_def TS ).
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
assert (EF a b c d a b c d) by (conclude axiom_paste3).
(* Goal: @EF Ax0 Ax1 Ax2 Ax a b c d a b c d *)
close.
Qed.

End Euclid.
