Require Export GeoCoq.Elements.OriginalProofs.proposition_24.
Require Export GeoCoq.Elements.OriginalProofs.lemma_angletrichotomy2.

Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma proposition_25 : 
   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 -> Lt E F B C ->
   LtA E D F B A C.
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) (_ : @Lt Ax0 E F B C), @LtA Ax0 E D F B A C *)
intros.
(* Goal: @LtA Ax0 E D F B A C *)
assert (Cong D E A B) by (conclude lemma_congruencesymmetric).
(* Goal: @LtA Ax0 E D F B A C *)
assert (Cong D F A C) by (conclude lemma_congruencesymmetric).
(* Goal: @LtA Ax0 E D F B A C *)
assert (~ LtA B A C E D F).
(* Goal: not (@CongA Ax0 E D F B A C) *)
(* Goal: @LtA Ax0 E D F B A C *)
 {
(* Goal: not (@CongA Ax0 E D F B A C) *)
 intro.
(* Goal: False *)
 assert (Lt B C E F) by (conclude proposition_24).
(* Goal: False *)
 assert (~ Lt E F B C) by (conclude lemma_trichotomy2).
(* Goal: False *)
 contradict.
 }
(* Goal: @LtA Ax0 E D F B A C *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: @LtA Ax0 E D F B A C *)
assert (~ Col B A C).
(* Goal: not (@CongA Ax0 E D F B A C) *)
(* Goal: @LtA Ax0 E D F B A C *)
 {
(* Goal: not (@CongA Ax0 E D F B A C) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @LtA Ax0 E D F B A C *)
assert (nCol D E F) by (conclude_def Triangle ).
(* Goal: @LtA Ax0 E D F B A C *)
assert (~ Col E D F).
(* Goal: not (@CongA Ax0 E D F B A C) *)
(* Goal: @LtA Ax0 E D F B A C *)
 {
(* Goal: not (@CongA Ax0 E D F B A C) *)
 intro.
(* Goal: False *)
 assert (Col D E F) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @LtA Ax0 E D F B A C *)
assert (~ CongA E D F B A C).
(* Goal: not (@CongA Ax0 E D F B A C) *)
(* Goal: @LtA Ax0 E D F B A C *)
 {
(* Goal: not (@CongA Ax0 E D F B A C) *)
 intro.
(* Goal: False *)
 assert (CongA B A C E D F) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (Cong B C E F) by (conclude proposition_04).
(* Goal: False *)
 assert (Cong E F B C) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 assert (Lt B C B C) by (conclude lemma_lessthancongruence2).
(* Goal: False *)
 assert (~ Lt B C B C) by (conclude lemma_trichotomy2).
(* Goal: False *)
 contradict.
 }
(* Goal: @LtA Ax0 E D F B A C *)
assert (LtA E D F B A C) by (conclude lemma_angletrichotomy2).
(* Goal: @LtA Ax0 E D F B A C *)
close.
Qed.

End Euclid.
