Require Export GeoCoq.Elements.OriginalProofs.lemma_ABCequalsCBA.
Require Export GeoCoq.Elements.OriginalProofs.proposition_04.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_05 : 
   forall A B C, 
   isosceles A B C ->
   CongA A B C A C B.
Proof.
(* Goal: forall (A B C : @Point Ax0) (_ : @isosceles Ax0 A B C), @CongA Ax0 A B C A C B *)
intros.
(* Goal: @CongA Ax0 A B C A C B *)
assert ((Triangle A B C /\ Cong A B A C)) by (conclude_def isosceles ).
(* Goal: @CongA Ax0 A B C A C B *)
assert (Cong A C A B) by (conclude lemma_congruencesymmetric).
(* Goal: @CongA Ax0 A B C A C B *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: @CongA Ax0 A B C A C B *)
assert (~ Col C A B).
(* Goal: not (@Col Ax0 C A B) *)
(* Goal: @CongA Ax0 A B C A C B *)
 {
(* Goal: not (@Col Ax0 C A B) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @CongA Ax0 A B C A C B *)
assert (CongA C A B B A C) by (conclude lemma_ABCequalsCBA).
(* Goal: @CongA Ax0 A B C A C B *)
assert ((Cong C B B C /\ CongA A C B A B C /\ CongA A B C A C B)) by (conclude proposition_04).
(* Goal: @CongA Ax0 A B C A C B *)
close.
Qed.

End Euclid.


