Require Export GeoCoq.Elements.OriginalProofs.lemma_inequalitysymmetric.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ray4.
Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearorder.
Require Export GeoCoq.Elements.OriginalProofs.lemma_congruenceflip.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_08 : 
   forall A B C D E F, 
   Triangle A B C -> Triangle D E F -> Cong A B D E -> Cong A C D F -> Cong B C E F ->
   CongA B A C E D F /\ CongA C B A F E D /\ CongA A C B D F E.
Proof.
(* Goal: forall (A B C D E F : @Point Ax0) (_ : @Triangle Ax0 A B C) (_ : @Triangle Ax0 D E F) (_ : @Cong Ax0 A B D E) (_ : @Cong Ax0 A C D F) (_ : @Cong Ax0 B C E F), and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
intros.
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (eq E E) by (conclude cn_equalityreflexive).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (eq F F) by (conclude cn_equalityreflexive).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (nCol D E F) by (conclude_def Triangle ).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (~ eq A B).
(* Goal: not (@Col Ax0 A C B) *)
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
 {
(* Goal: not (@Col Ax0 A C B) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (~ eq B C).
(* Goal: not (@Col Ax0 A C B) *)
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
 {
(* Goal: not (@Col Ax0 A C B) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (neq C B) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (~ eq D E).
(* Goal: not (@Col Ax0 A C B) *)
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
 {
(* Goal: not (@Col Ax0 A C B) *)
 intro.
(* Goal: False *)
 assert (Col D E F) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (neq E D) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (~ eq A C).
(* Goal: not (@Col Ax0 A C B) *)
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
 {
(* Goal: not (@Col Ax0 A C B) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (neq C A) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (~ eq D F).
(* Goal: not (@Col Ax0 A C B) *)
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
 {
(* Goal: not (@Col Ax0 A C B) *)
 intro.
(* Goal: False *)
 assert (Col D E F) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (neq F D) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (~ eq E F).
(* Goal: not (@Col Ax0 A C B) *)
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
 {
(* Goal: not (@Col Ax0 A C B) *)
 intro.
(* Goal: False *)
 assert (Col D E F) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (neq F E) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Out D E E) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Out D F F) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Out A B B) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Out A C C) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (~ Col B A C).
(* Goal: not (@Col Ax0 A C B) *)
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
 {
(* Goal: not (@Col Ax0 A C B) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (CongA B A C E D F) by (conclude_def CongA ).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Cong B A E D) by (forward_using lemma_congruenceflip).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Cong C A F D) by (forward_using lemma_congruenceflip).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Out E F F) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Out E D D) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Out B C C) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Out B A A) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (~ Col C B A).
(* Goal: not (@Col Ax0 A C B) *)
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
 {
(* Goal: not (@Col Ax0 A C B) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (CongA C B A F E D) by (conclude_def CongA ).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Cong C A F D) by (forward_using lemma_congruenceflip).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Cong C B F E) by (forward_using lemma_congruenceflip).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Out F D D) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Out F E E) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Out C A A) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (Out C B B) by (conclude lemma_ray4).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (~ Col A C B).
(* Goal: not (@Col Ax0 A C B) *)
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
 {
(* Goal: not (@Col Ax0 A C B) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
assert (CongA A C B D F E) by (conclude_def CongA ).
(* Goal: and (@CongA Ax0 B A C E D F) (and (@CongA Ax0 C B A F E D) (@CongA Ax0 A C B D F E)) *)
close.
Qed.

End Euclid.


