proposition: Lemma lemma_TTflip : forall A B C D E F G H, TT A B C D E F G H -> TT B A D C E F G H.
proof: Proof. intros. let Tf:=fresh in assert (Tf:exists J, (BetS E F J /\ Cong F J G H /\ TG A B C D E J)) by (conclude_def TT );destruct Tf as [J];spliter. assert (TG B A C D E J) by (forward_using lemma_TGflip). assert (TG C D B A E J) by (conclude lemma_TGsymmetric). assert (TG D C B A E J) by (forward_using lemma_TGflip). assert (TG B A D C E J) by (conclude lemma_TGsymmetric). assert (TT B A D C E F G H) by (conclude_def TT ). close. Qed.
imports: GeoCoq.Elements.OriginalProofs.lemma_TGflip GeoCoq.Elements.OriginalProofs.lemma_TGsymmetric