Require Export GeoCoq.Elements.OriginalProofs.lemma_26helper.
Require Export GeoCoq.Elements.OriginalProofs.lemma_trichotomy1.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_26B : 
   forall A B C D E F, 
   Triangle A B C -> Triangle D E F -> CongA A B C D E F -> CongA B C A E F D -> Cong A B D E ->
   Cong B C E F /\ Cong A C D F /\ CongA B A C E D F.
Proof.
(* Goal: forall (A B C D E F : @Point Ax0) (_ : @Triangle Ax0 A B C) (_ : @Triangle Ax0 D E F) (_ : @CongA Ax0 A B C D E F) (_ : @CongA Ax0 B C A E F D) (_ : @Cong Ax0 A B D E), and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
intros.
(* Goal: and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (~ Lt E F B C) by (conclude lemma_26helper).
(* Goal: and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (CongA D E F A B C) by (conclude lemma_equalanglessymmetric).
(* Goal: and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (CongA E F D B C A) by (conclude lemma_equalanglessymmetric).
(* Goal: and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (Cong D E A B) by (conclude lemma_congruencesymmetric).
(* Goal: and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (~ Lt B C E F) by (conclude lemma_26helper).
(* Goal: and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (~ eq B C).
(* Goal: not (@eq Ax0 E F) *)
(* Goal: and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
 {
(* Goal: not (@eq Ax0 E F) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (~ eq E F).
(* Goal: not (@eq Ax0 E F) *)
(* Goal: and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
 {
(* Goal: not (@eq Ax0 E F) *)
 intro.
(* Goal: False *)
 assert (Col D E F) by (conclude_def Col ).
(* Goal: False *)
 assert (nCol D E F) by (conclude_def Triangle ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (Cong B C E F) by (conclude lemma_trichotomy1).
(* Goal: and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert (Cong B A E D) by (forward_using lemma_congruenceflip).
(* Goal: and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
assert ((Cong A C D F /\ CongA B A C E D F /\ CongA B C A E F D)) by (conclude proposition_04).
(* Goal: and (@Cong Ax0 B C E F) (and (@Cong Ax0 A C D F) (@CongA Ax0 B A C E D F)) *)
close.
Qed.

End Euclid.


