Require Export GeoCoq.Elements.OriginalProofs.lemma_ABCequalsCBA.
Require Export GeoCoq.Elements.OriginalProofs.lemma_supplements.
Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglestransitive.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_15 : 
   forall A B C D E, 
   BetS A E B -> BetS C E D -> nCol A E C ->
   CongA A E C D E B /\ CongA C E B A E D.
Proof.
(* Goal: forall (A B C D E : @Point Ax0) (_ : @BetS Ax0 A E B) (_ : @BetS Ax0 C E D) (_ : @nCol Ax0 A E C), @CongA Ax0 C E B A E D *)
intros.
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (neq E D) by (forward_using lemma_betweennotequal).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (neq D E) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (neq E B) by (forward_using lemma_betweennotequal).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (neq B E) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (~ Col B E D).
(* Goal: not (@Col Ax0 B E D) *)
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
 {
(* Goal: not (@Col Ax0 B E D) *)
 intro.
(* Goal: False *)
 assert (Col A E B) by (conclude_def Col ).
(* Goal: False *)
 assert (Col B E A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col E A D) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col C E D) by (conclude_def Col ).
(* Goal: False *)
 assert (Col D E C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col D E A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col E C A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A E C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (Out E D D) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (Out E B B) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (BetS B E A) by (conclude axiom_betweennesssymmetry).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (Supp B E D D A) by (conclude_def Supp ).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (BetS D E C) by (conclude axiom_betweennesssymmetry).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (Supp D E B B C) by (conclude_def Supp ).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (~ Col A E D).
(* Goal: not (@Col Ax0 B E D) *)
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
 {
(* Goal: not (@Col Ax0 B E D) *)
 intro.
(* Goal: False *)
 assert (Col C E D) by (conclude_def Col ).
(* Goal: False *)
 assert (Col D E C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col D E A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col E C A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A E C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (CongA B E D D E B) by (conclude lemma_ABCequalsCBA).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (CongA D E A B E C) by (conclude lemma_supplements).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (~ Col B E C).
(* Goal: not (@Col Ax0 B E D) *)
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
 {
(* Goal: not (@Col Ax0 B E D) *)
 intro.
(* Goal: False *)
 assert (Col A E B) by (conclude_def Col ).
(* Goal: False *)
 assert (Col B E A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col E A C) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A E C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (CongA B E C C E B) by (conclude lemma_ABCequalsCBA).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (CongA D E A C E B) by (conclude lemma_equalanglestransitive).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (CongA A E D D E A) by (conclude lemma_ABCequalsCBA).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (CongA A E D C E B) by (conclude lemma_equalanglestransitive).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (CongA C E B A E D) by (conclude lemma_equalanglessymmetric).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (~ eq E C).
(* Goal: not (@Col Ax0 B E D) *)
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
 {
(* Goal: not (@Col Ax0 B E D) *)
 intro.
(* Goal: False *)
 assert (Col B E C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (Out E C C) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (Supp B E C C A) by (conclude_def Supp ).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (BetS C E D) by (conclude axiom_betweennesssymmetry).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (Supp C E B B D) by (conclude_def Supp ).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (~ Col A E C).
(* Goal: not (@Col Ax0 B E D) *)
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
 {
(* Goal: not (@Col Ax0 B E D) *)
 intro.
(* Goal: False *)
 assert (Col D E C) by (conclude_def Col ).
(* Goal: False *)
 assert (Col C E D) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col C E A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq C E) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col E D A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A E D) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (CongA B E C C E B) by (conclude lemma_ABCequalsCBA).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (CongA C E A B E D) by (conclude lemma_supplements).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (~ Col B E D).
(* Goal: not (@Col Ax0 B E D) *)
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
 {
(* Goal: not (@Col Ax0 B E D) *)
 intro.
(* Goal: False *)
 assert (Col A E B) by (conclude_def Col ).
(* Goal: False *)
 assert (Col B E A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col E A D) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A E D) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (CongA B E D D E B) by (conclude lemma_ABCequalsCBA).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (CongA C E A D E B) by (conclude lemma_equalanglestransitive).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (CongA A E C C E A) by (conclude lemma_ABCequalsCBA).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
assert (CongA A E C D E B) by (conclude lemma_equalanglestransitive).
(* Goal: and (@CongA Ax0 A E C D E B) (@CongA Ax0 C E B A E D) *)
close.
Qed.

Lemma proposition_15a :
 forall A B C D E : Point,
       BetS A E B ->
       BetS C E D -> nCol A E C -> CongA A E C D E B.
Proof.
(* Goal: forall (A B C D E : @Point Ax0) (_ : @BetS Ax0 A E B) (_ : @BetS Ax0 C E D) (_ : @nCol Ax0 A E C), @CongA Ax0 C E B A E D *)
intros.
(* Goal: @CongA Ax0 C E B A E D *)
apply (proposition_15 A B C D E);assumption.
Qed.

Lemma proposition_15b :
 forall A B C D E : Point,
       BetS A E B ->
       BetS C E D -> nCol A E C ->
       CongA C E B A E D.
Proof.
(* Goal: forall (A B C D E : @Point Ax0) (_ : @BetS Ax0 A E B) (_ : @BetS Ax0 C E D) (_ : @nCol Ax0 A E C), @CongA Ax0 C E B A E D *)
intros.
(* Goal: @CongA Ax0 C E B A E D *)
apply (proposition_15 A B C D E);assumption.
Qed.

End Euclid.


