Require Export GeoCoq.Elements.OriginalProofs.lemma_supplementsymmetric.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ABCequalsCBA.
Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglestransitive.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_RTsymmetric : 
   forall A B C D E F, 
   RT A B C D E F ->
   RT D E F A B C.
Proof.
(* Goal: forall (A B C D E F : @Point Ax0) (_ : @RT Ax0 A B C D E F), @RT Ax0 D E F A B C *)
intros.
let Tf:=fresh in
assert (Tf:exists a b c d e, (Supp a b c d e /\ CongA A B C a b c /\ CongA D E F d b e)) by (conclude_def RT );destruct Tf as [a[b[c[d[e]]]]];spliter.
(* Goal: @RT Ax0 D E F A B C *)
assert (Supp e b d c a) by (conclude lemma_supplementsymmetric).
(* Goal: @RT Ax0 D E F A B C *)
assert (nCol d b e) by (conclude lemma_equalanglesNC).
(* Goal: @RT Ax0 D E F A B C *)
assert (CongA d b e e b d) by (conclude lemma_ABCequalsCBA).
(* Goal: @RT Ax0 D E F A B C *)
assert (nCol a b c) by (conclude lemma_equalanglesNC).
(* Goal: @RT Ax0 D E F A B C *)
assert (CongA a b c c b a) by (conclude lemma_ABCequalsCBA).
(* Goal: @RT Ax0 D E F A B C *)
assert (CongA D E F e b d) by (conclude lemma_equalanglestransitive).
(* Goal: @RT Ax0 D E F A B C *)
assert (CongA A B C c b a) by (conclude lemma_equalanglestransitive).
(* Goal: @RT Ax0 D E F A B C *)
assert (RT D E F A B C) by (conclude_def RT ).
(* Goal: @RT Ax0 D E F A B C *)
close.
Qed.

End Euclid.


