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

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_equalanglesreflexive : 
   forall A B C, 
   nCol A B C ->
   CongA A B C A B C.
Proof.
(* Goal: forall (A B C : @Point Ax0) (_ : @nCol Ax0 A B C), @CongA Ax0 A B C A B C *)
intros.
(* Goal: @CongA Ax0 A B C A B C *)
assert (CongA A B C C B A) by (conclude lemma_ABCequalsCBA).
(* Goal: @CongA Ax0 A B C A B C *)
assert (nCol C B A) by (conclude lemma_equalanglesNC).
(* Goal: @CongA Ax0 A B C A B C *)
assert (CongA C B A A B C) by (conclude lemma_ABCequalsCBA).
(* Goal: @CongA Ax0 A B C A B C *)
assert (CongA A B C A B C) by (conclude lemma_equalanglestransitive).
(* Goal: @CongA Ax0 A B C A B C *)
close.
Qed.

End Euclid.


