# Library GeoCoq.Elements.OriginalProofs.lemma_equalanglesNC

Require Export GeoCoq.Elements.OriginalProofs.lemma_ray2.

Require Export GeoCoq.Elements.OriginalProofs.lemma_rayimpliescollinear.

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearitypreserved.

Require Export GeoCoq.Elements.OriginalProofs.lemma_raystrict.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_equalanglesNC :

∀ A B C a b c,

CongA A B C a b c →

nCol a b c.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ 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.

assert (neq b a) by (conclude lemma_ray2).

assert (neq a b) by (conclude lemma_inequalitysymmetric).

assert (Cong b u B U) by (conclude lemma_congruencesymmetric).

assert (Cong b v B V) by (conclude lemma_congruencesymmetric).

assert (Col B A U) by (conclude lemma_rayimpliescollinear).

assert (Col B C V) by (conclude lemma_rayimpliescollinear).

assert (Col b a u) by (conclude lemma_rayimpliescollinear).

assert (Col b c v) by (conclude lemma_rayimpliescollinear).

assert (Col a b u) by (forward_using lemma_collinearorder).

assert (¬ Col a b c).

{

intro.

assert (Col b u c) by (conclude lemma_collinear4).

assert (Col c b u) by (forward_using lemma_collinearorder).

assert (Col c b v) by (forward_using lemma_collinearorder).

assert (neq b c) by (conclude lemma_ray2).

assert (neq c b) by (conclude lemma_inequalitysymmetric).

assert (Col b u v) by (conclude lemma_collinear4).

assert (Cong u v U V) by (conclude lemma_congruencesymmetric).

assert (Col B U V) by (conclude lemma_collinearitypreserved).

assert (Col B U A) by (forward_using lemma_collinearorder).

assert (neq B U) by (conclude lemma_raystrict).

assert (Col U V A) by (conclude lemma_collinear4).

assert (Col U V B) by (forward_using lemma_collinearorder).

assert (Col V A B).

by cases on (eq U V ∨ neq U V).

{

assert (Col B A V) by (conclude cn_equalitysub).

assert (Col V A B) by (forward_using lemma_collinearorder).

close.

}

{

assert (Col V A B) by (conclude lemma_collinear4).

close.

}

assert (Col V B A) by (forward_using lemma_collinearorder).

assert (Col V B C) by (forward_using lemma_collinearorder).

assert (neq B V) by (conclude lemma_raystrict).

assert (neq V B) by (conclude lemma_inequalitysymmetric).

assert (Col B A C) by (conclude lemma_collinear4).

assert (Col A B C) by (forward_using lemma_collinearorder).

contradict.

}

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_rayimpliescollinear.

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearitypreserved.

Require Export GeoCoq.Elements.OriginalProofs.lemma_raystrict.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_equalanglesNC :

∀ A B C a b c,

CongA A B C a b c →

nCol a b c.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ 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.

assert (neq b a) by (conclude lemma_ray2).

assert (neq a b) by (conclude lemma_inequalitysymmetric).

assert (Cong b u B U) by (conclude lemma_congruencesymmetric).

assert (Cong b v B V) by (conclude lemma_congruencesymmetric).

assert (Col B A U) by (conclude lemma_rayimpliescollinear).

assert (Col B C V) by (conclude lemma_rayimpliescollinear).

assert (Col b a u) by (conclude lemma_rayimpliescollinear).

assert (Col b c v) by (conclude lemma_rayimpliescollinear).

assert (Col a b u) by (forward_using lemma_collinearorder).

assert (¬ Col a b c).

{

intro.

assert (Col b u c) by (conclude lemma_collinear4).

assert (Col c b u) by (forward_using lemma_collinearorder).

assert (Col c b v) by (forward_using lemma_collinearorder).

assert (neq b c) by (conclude lemma_ray2).

assert (neq c b) by (conclude lemma_inequalitysymmetric).

assert (Col b u v) by (conclude lemma_collinear4).

assert (Cong u v U V) by (conclude lemma_congruencesymmetric).

assert (Col B U V) by (conclude lemma_collinearitypreserved).

assert (Col B U A) by (forward_using lemma_collinearorder).

assert (neq B U) by (conclude lemma_raystrict).

assert (Col U V A) by (conclude lemma_collinear4).

assert (Col U V B) by (forward_using lemma_collinearorder).

assert (Col V A B).

by cases on (eq U V ∨ neq U V).

{

assert (Col B A V) by (conclude cn_equalitysub).

assert (Col V A B) by (forward_using lemma_collinearorder).

close.

}

{

assert (Col V A B) by (conclude lemma_collinear4).

close.

}

assert (Col V B A) by (forward_using lemma_collinearorder).

assert (Col V B C) by (forward_using lemma_collinearorder).

assert (neq B V) by (conclude lemma_raystrict).

assert (neq V B) by (conclude lemma_inequalitysymmetric).

assert (Col B A C) by (conclude lemma_collinear4).

assert (Col A B C) by (forward_using lemma_collinearorder).

contradict.

}

close.

Qed.

End Euclid.