Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthanbetween.
Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthanadditive.

Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma lemma_21helper : 
   forall A B C E, 
   TG B A A E B E -> BetS A E C ->
   TT B A A C B E E C.
Proof.
(* Goal: forall (A B C E : @Point Ax0) (_ : @TG Ax0 B A A E B E) (_ : @BetS Ax0 A E C), @TT Ax0 B A A C B E E C *)
intros.
rename_H H;let Tf:=fresh in
assert (Tf:exists H, (BetS B A H /\ Cong A H A E /\ Lt B E B H)) by (conclude_def TG );destruct Tf as [H];spliter.
(* Goal: @TT Ax0 B A A C B E E C *)
assert (neq B A) by (forward_using lemma_betweennotequal).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (~ eq B E).
(* Goal: not (@neq Ax0 B K) *)
(* Goal: False *)
 {
(* Goal: not (@neq Ax0 B K) *)
 intro.
(* Goal: False *)
 assert (Lt B B B H) by (conclude cn_equalitysub).
 let Tf:=fresh in
 assert (Tf:exists K, (BetS B K H /\ Cong B K B B)) by (conclude_def Lt );destruct Tf as [K];spliter.
(* Goal: False *)
 assert (~ neq B K).
(* Goal: not (@neq Ax0 B K) *)
(* Goal: False *)
  {
(* Goal: not (@neq Ax0 B K) *)
  intro.
(* Goal: False *)
  assert (neq B B) by (conclude axiom_nocollapse).
(* Goal: False *)
  assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (BetS B B H) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (neq B B) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: False *)
 contradict.
 }
(* Goal: @TT Ax0 B A A C B E E C *)
assert (neq A C) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists F, (BetS B A F /\ Cong A F A C)) by (conclude lemma_extension);destruct Tf as [F];spliter.
(* Goal: @TT Ax0 B A A C B E E C *)
assert (neq E C) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists G, (BetS B E G /\ Cong E G E C)) by (conclude lemma_extension);destruct Tf as [G];spliter.
(* Goal: @TT Ax0 B A A C B E E C *)
assert (Cong A C A F) by (conclude lemma_congruencesymmetric).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (Cong A E A H) by (conclude lemma_congruencesymmetric).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (Cong A E A E) by (conclude cn_congruencereflexive).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (Lt A E A C) by (conclude_def Lt ).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (Lt A E A F) by (conclude lemma_lessthancongruence).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (Lt A H A F) by (conclude lemma_lessthancongruence2).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (Out A H F) by (conclude_def Out ).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (BetS A H F) by (conclude lemma_lessthanbetween).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (Cong E C H F) by (conclude lemma_differenceofparts).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (Cong E G H F) by (conclude lemma_congruencetransitive).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (BetS B H F) by (conclude lemma_3_7a).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (Lt B G B F) by (conclude lemma_lessthanadditive).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (TG B A A C B G) by (conclude_def TG ).
(* Goal: @TT Ax0 B A A C B E E C *)
assert (TT B A A C B E E C) by (conclude_def TT ).
(* Goal: @TT Ax0 B A A C B E E C *)
close.
Qed.

End Euclid.
