Require Export GeoCoq.Elements.OriginalProofs.proposition_16.
Require Export GeoCoq.Elements.OriginalProofs.lemma_angletrichotomy.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_26helper : 
   forall A B C D E F, 
   Triangle A B C -> CongA A B C D E F -> CongA B C A E F D -> Cong A B D E ->
   ~ Lt E F B C.
Proof.
(* Goal: forall (A B C D E F : @Point Ax) (_ : @Triangle Ax A B C) (_ : @CongA Ax A B C D E F) (_ : @CongA Ax B C A E F D) (_ : @Cong Ax A B D E), not (@Lt Ax E F B C) *)
intros.
(* Goal: not (@Lt Ax E F B C) *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: False *)
assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).
(* Goal: not (@Lt Ax E F B C) *)
assert (neq A B) by (forward_using lemma_angledistinct).
(* Goal: not (@Lt Ax E F B C) *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
(* Goal: not (@Lt Ax E F B C) *)
assert (neq B C) by (forward_using lemma_angledistinct).
(* Goal: not (@Lt Ax E F B C) *)
assert (neq C B) by (conclude lemma_inequalitysymmetric).
(* Goal: not (@Lt Ax E F B C) *)
assert (neq A C) by (forward_using lemma_angledistinct).
(* Goal: not (@Lt Ax E F B C) *)
assert (neq C A) by (conclude lemma_inequalitysymmetric).
(* Goal: not (@Lt Ax E F B C) *)
assert (~ Lt E F B C).
(* Goal: not (@Col Ax A H B) *)
(* Goal: False *)
 {
(* Goal: not (@Col Ax A H B) *)
 intro.
 rename_H H;let Tf:=fresh in
 assert (Tf:exists H, (BetS B H C /\ Cong B H E F)) by (conclude_def Lt );destruct Tf as [H];spliter.
(* Goal: False *)
 assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).
(* Goal: False *)
 assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: False *)
 assert (Out B A A) by (conclude lemma_ray4).
(* Goal: False *)
 assert (Out B C H) by (conclude lemma_ray4).
(* Goal: False *)
 assert (CongA A B C A B H) by (conclude lemma_equalangleshelper).
(* Goal: False *)
 assert (CongA A B H A B C) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (CongA A B H D E F) by (conclude lemma_equalanglestransitive).
(* Goal: False *)
 assert (Cong B A E D) by (forward_using lemma_congruenceflip).
(* Goal: False *)
 assert ((Cong A H D F /\ CongA B A H E D F /\ CongA B H A E F D)) by (conclude proposition_04).
(* Goal: False *)
 assert (CongA E F D B C A) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (~ Col A C H).
(* Goal: not (@Col Ax A H B) *)
(* Goal: False *)
  {
(* Goal: not (@Col Ax A H B) *)
  intro.
(* Goal: False *)
  assert (Col H C A) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (Col B H C) by (conclude_def Col ).
(* Goal: False *)
  assert (Col H C B) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (neq H C) by (forward_using lemma_betweennotequal).
(* Goal: False *)
  assert (Col C A B) by (conclude lemma_collinear4).
(* Goal: False *)
  assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (Triangle A C H) by (conclude_def Triangle ).
(* Goal: False *)
 assert (BetS C H B) by (conclude axiom_betweennesssymmetry).
(* Goal: False *)
 assert (LtA H C A A H B) by (conclude proposition_16).
(* Goal: False *)
 assert (Out C B H) by (conclude lemma_ray4).
(* Goal: False *)
 assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: False *)
 assert (Out C A A) by (conclude lemma_ray4).
(* Goal: False *)
 assert (~ Col B C A).
(* Goal: not (@Col Ax A H B) *)
(* Goal: False *)
  {
(* Goal: not (@Col Ax A H B) *)
  intro.
(* Goal: False *)
  assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (CongA B C A B C A) by (conclude lemma_equalanglesreflexive).
(* Goal: False *)
 assert (CongA B C A H C A) by (conclude lemma_equalangleshelper).
(* Goal: False *)
 assert (CongA H C A B C A) by (conclude lemma_equalanglessymmetric).
(* Goal: False *)
 assert (LtA B C A A H B) by (conclude lemma_angleorderrespectscongruence2).
(* Goal: False *)
 assert (LtA E F D A H B) by (conclude lemma_angleorderrespectscongruence2).
(* Goal: False *)
 assert (~ Col A H B).
(* Goal: not (@Col Ax A H B) *)
(* Goal: False *)
  {
(* Goal: not (@Col Ax A H B) *)
  intro.
(* Goal: False *)
  assert (Col H B A) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (Col B H C) by (conclude_def Col ).
(* Goal: False *)
  assert (Col H B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (neq B H) by (forward_using lemma_betweennotequal).
(* Goal: False *)
  assert (neq H B) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
  assert (Col B A C) by (conclude lemma_collinear4).
(* Goal: False *)
  assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (CongA A H B B H A) by (conclude lemma_ABCequalsCBA).
(* Goal: False *)
 assert (CongA A H B E F D) by (conclude lemma_equalanglestransitive).
(* Goal: False *)
 assert (LtA A H B A H B) by (conclude lemma_angleorderrespectscongruence2).
(* Goal: False *)
 assert (~ LtA A H B A H B) by (conclude lemma_angletrichotomy).
(* Goal: False *)
 contradict.
 }
(* Goal: not (@Lt Ax E F B C) *)
close.
Qed.

End Euclid.


