Require Export GeoCoq.Elements.OriginalProofs.euclidean_tactics.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_TCreflexive :
   forall A B C,
   Triangle A B C ->
   Cong_3 A B C A B C.
Proof.
(* Goal: forall (A B C : @Point Ax) (_ : @Triangle Ax A B C), @Cong_3 Ax A B C A B C *)
intros.
(* Goal: @Cong_3 Ax A B C A B C *)
assert (Cong A B A B) by (conclude cn_congruencereflexive).
(* Goal: @Cong_3 Ax A B C A B C *)
assert (Cong B C B C) by (conclude cn_congruencereflexive).
(* Goal: @Cong_3 Ax A B C A B C *)
assert (Cong A C A C) by (conclude cn_congruencereflexive).
(* Goal: @Cong_3 Ax A B C A B C *)
assert (Cong_3 A B C A B C) by (conclude_def Cong_3 ).
(* Goal: @Cong_3 Ax A B C A B C *)
close.
Qed.

End Euclid.