Require Export GeoCoq.Elements.OriginalProofs.lemma_rayimpliescollinear.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ray2.
Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearitypreserved.
Require Export GeoCoq.Elements.OriginalProofs.lemma_raystrict.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_equalanglessymmetric : 
   forall A B C a b c, 
   CongA A B C a b c ->
   CongA a b c A B C.
Proof.
(* Goal: forall (A B C a b c : @Point Ax0) (_ : @CongA Ax0 A B C a b c), @CongA Ax0 a b c A B C *)
intros.
let Tf:=fresh in
assert (Tf:exists U V u v, (Out B A U /\ Out B C V /\ Out b a u /\ Out b c v /\ Cong B U b u /\ Cong B V b v /\ Cong U V u v /\ nCol A B C)) by (conclude_def CongA );destruct Tf as [U[V[u[v]]]];spliter.
(* Goal: @CongA Ax0 a b c A B C *)
assert (Cong b u B U) by (conclude lemma_congruencesymmetric).
(* Goal: @CongA Ax0 a b c A B C *)
assert (Cong b v B V) by (conclude lemma_congruencesymmetric).
(* Goal: @CongA Ax0 a b c A B C *)
assert (Cong v u V U) by (forward_using lemma_doublereverse).
(* Goal: @CongA Ax0 a b c A B C *)
assert (~ Col a b c).
(* Goal: not (@Col Ax0 a b c) *)
(* Goal: @CongA Ax0 a b c A B C *)
 {
(* Goal: not (@Col Ax0 a b c) *)
 intro.
(* Goal: False *)
 assert (Col b a u) by (conclude lemma_rayimpliescollinear).
(* Goal: False *)
 assert (Col b c v) by (conclude lemma_rayimpliescollinear).
(* Goal: False *)
 assert (Col B A U) by (conclude lemma_rayimpliescollinear).
(* Goal: False *)
 assert (Col B C V) by (conclude lemma_rayimpliescollinear).
(* Goal: False *)
 assert (Col a b u) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq b a) by (conclude lemma_ray2).
(* Goal: False *)
 assert (neq a b) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col b u c) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col c b u) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col c b v) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq b c) by (conclude lemma_ray2).
(* Goal: False *)
 assert (neq c b) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col b u v) by (conclude lemma_collinear4).
(* Goal: @CongA Ax0 a b c A B C *)
 assert (Cong u v U V) by (conclude lemma_congruencesymmetric).
(* Goal: False *)
 assert (Col B U V) by (conclude lemma_collinearitypreserved).
(* Goal: False *)
 assert (Col U B V) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col U B A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq B U) by (conclude lemma_raystrict).
(* Goal: False *)
 assert (neq U B) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col B V A) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col V B A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col V B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq B V) by (conclude lemma_raystrict).
(* Goal: False *)
 assert (neq V B) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col B A C) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @CongA Ax0 a b c A B C *)
assert (Cong u v U V) by (conclude lemma_congruencesymmetric).
(* Goal: @CongA Ax0 a b c A B C *)
assert (CongA a b c A B C) by (conclude_def CongA ).
(* Goal: @CongA Ax0 a b c A B C *)
close.
Qed.

End Euclid.


