Require Export GeoCoq.Elements.OriginalProofs.lemma_congruenceflip.
Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthancongruence.
Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthancongruence2.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_TGflip : 
   forall A B C a b c, 
   TG A a B b C c ->
   TG a A B b C c /\ TG A a B b c C.
Proof.
(* Goal: forall (A B C a b c : @Point Ax0) (_ : @TG Ax0 A a B b C c), and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
intros.
rename_H H;let Tf:=fresh in
assert (Tf:exists H, (BetS A a H /\ Cong a H B b /\ Lt C c A H)) by (conclude_def TG );destruct Tf as [H];spliter.
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (neq A a) by (forward_using lemma_betweennotequal).
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (neq a A) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (neq a H) by (forward_using lemma_betweennotequal).
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (neq B b) by (conclude axiom_nocollapse).
let Tf:=fresh in
assert (Tf:exists h, (BetS a A h /\ Cong A h B b)) by (conclude lemma_extension);destruct Tf as [h];spliter.
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (Cong A a a A) by (conclude cn_equalityreverse).
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (Cong B b A h) by (conclude lemma_congruencesymmetric).
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (Cong a H A h) by (conclude lemma_congruencetransitive).
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (Cong A H a h) by (conclude cn_sumofparts).
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (Lt C c a h) by (conclude lemma_lessthancongruence).
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (TG a A B b C c) by (conclude_def TG ).
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (Cong C c c C) by (conclude cn_equalityreverse).
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (Lt c C A H) by (conclude lemma_lessthancongruence2).
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (TG A a B b c C) by (conclude_def TG ).
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
assert (Lt C c a h) by (conclude lemma_lessthancongruence).
(* Goal: and (@TG Ax0 a A B b C c) (@TG Ax0 A a B b c C) *)
close.
Qed.

End Euclid.


