# Library GeoCoq.Elements.OriginalProofs.lemma_equaltorightisright

Require Export GeoCoq.Elements.OriginalProofs.lemma_8_3.

Require Export GeoCoq.Elements.OriginalProofs.lemma_8_2.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_equaltorightisright :

∀ A B C a b c,

Per A B C → CongA a b c A B C →

Per a b c.

Proof.

intros.

assert (neq B C) by (forward_using lemma_angledistinct).

assert (neq A B) by (forward_using lemma_angledistinct).

assert (CongA A B C a b c) by (conclude lemma_equalanglessymmetric).

let Tf:=fresh in

assert (Tf:∃ E F e f, (Out B A E ∧ Out B C F ∧ Out b a e ∧ Out b c f ∧ Cong B E b e ∧ Cong B F b f ∧ Cong E F e f ∧ nCol A B C)) by (conclude_def CongA );destruct Tf as [E[F[e[f]]]];spliter.

assert (Per A B F) by (conclude lemma_8_3).

assert (Per F B A) by (conclude lemma_8_2).

assert (Per F B E) by (conclude lemma_8_3).

assert (Per E B F) by (conclude lemma_8_2).

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

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

let Tf:=fresh in

assert (Tf:∃ W, (BetS E B W ∧ Cong E B W B ∧ Cong E F W F ∧ neq B F)) by (conclude_def Per );destruct Tf as [W];spliter.

assert (neq b e) by (conclude lemma_nullsegment3).

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

let Tf:=fresh in

assert (Tf:∃ w, (BetS e b w ∧ Cong b w e b)) by (conclude postulate_extension);destruct Tf as [w];spliter.

assert (Cong e b E B) by (forward_using lemma_doublereverse).

assert (Cong b w E B) by (conclude lemma_congruencetransitive).

assert (Cong E B B W) by (forward_using lemma_congruenceflip).

assert (Cong b w B W) by (conclude lemma_congruencetransitive).

assert (Cong b f B F) by (conclude lemma_congruencesymmetric).

assert (Cong e f E F) by (conclude lemma_congruencesymmetric).

assert (Cong e w E W) by (conclude lemma_sumofparts).

assert (neq E B) by (conclude lemma_nullsegment3).

assert (Cong E B e b) by (forward_using lemma_congruenceflip).

assert (neq e b) by (conclude lemma_nullsegment3).

assert (Cong f w F W) by (conclude axiom_5_line).

assert (Cong e b B W) by (conclude lemma_congruencetransitive).

assert (Cong B W b w) by (conclude lemma_congruencesymmetric).

assert (Cong e b b w) by (conclude lemma_congruencetransitive).

assert (Cong e b w b) by (forward_using lemma_congruenceflip).

assert (Cong e f W F) by (conclude lemma_congruencetransitive).

assert (Cong W F w f) by (forward_using lemma_doublereverse).

assert (Cong e f w f) by (conclude lemma_congruencetransitive).

assert (neq b f) by (conclude lemma_raystrict).

assert (Per e b f) by (conclude_def Per ).

assert (Out b f c) by (conclude lemma_ray5).

assert (Per e b c) by (conclude lemma_8_3).

assert (Per c b e) by (conclude lemma_8_2).

assert (Out b e a) by (conclude lemma_ray5).

assert (Per c b a) by (conclude lemma_8_3).

assert (Per a b c) by (conclude lemma_8_2).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_8_2.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_equaltorightisright :

∀ A B C a b c,

Per A B C → CongA a b c A B C →

Per a b c.

Proof.

intros.

assert (neq B C) by (forward_using lemma_angledistinct).

assert (neq A B) by (forward_using lemma_angledistinct).

assert (CongA A B C a b c) by (conclude lemma_equalanglessymmetric).

let Tf:=fresh in

assert (Tf:∃ E F e f, (Out B A E ∧ Out B C F ∧ Out b a e ∧ Out b c f ∧ Cong B E b e ∧ Cong B F b f ∧ Cong E F e f ∧ nCol A B C)) by (conclude_def CongA );destruct Tf as [E[F[e[f]]]];spliter.

assert (Per A B F) by (conclude lemma_8_3).

assert (Per F B A) by (conclude lemma_8_2).

assert (Per F B E) by (conclude lemma_8_3).

assert (Per E B F) by (conclude lemma_8_2).

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

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

let Tf:=fresh in

assert (Tf:∃ W, (BetS E B W ∧ Cong E B W B ∧ Cong E F W F ∧ neq B F)) by (conclude_def Per );destruct Tf as [W];spliter.

assert (neq b e) by (conclude lemma_nullsegment3).

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

let Tf:=fresh in

assert (Tf:∃ w, (BetS e b w ∧ Cong b w e b)) by (conclude postulate_extension);destruct Tf as [w];spliter.

assert (Cong e b E B) by (forward_using lemma_doublereverse).

assert (Cong b w E B) by (conclude lemma_congruencetransitive).

assert (Cong E B B W) by (forward_using lemma_congruenceflip).

assert (Cong b w B W) by (conclude lemma_congruencetransitive).

assert (Cong b f B F) by (conclude lemma_congruencesymmetric).

assert (Cong e f E F) by (conclude lemma_congruencesymmetric).

assert (Cong e w E W) by (conclude lemma_sumofparts).

assert (neq E B) by (conclude lemma_nullsegment3).

assert (Cong E B e b) by (forward_using lemma_congruenceflip).

assert (neq e b) by (conclude lemma_nullsegment3).

assert (Cong f w F W) by (conclude axiom_5_line).

assert (Cong e b B W) by (conclude lemma_congruencetransitive).

assert (Cong B W b w) by (conclude lemma_congruencesymmetric).

assert (Cong e b b w) by (conclude lemma_congruencetransitive).

assert (Cong e b w b) by (forward_using lemma_congruenceflip).

assert (Cong e f W F) by (conclude lemma_congruencetransitive).

assert (Cong W F w f) by (forward_using lemma_doublereverse).

assert (Cong e f w f) by (conclude lemma_congruencetransitive).

assert (neq b f) by (conclude lemma_raystrict).

assert (Per e b f) by (conclude_def Per ).

assert (Out b f c) by (conclude lemma_ray5).

assert (Per e b c) by (conclude lemma_8_3).

assert (Per c b e) by (conclude lemma_8_2).

assert (Out b e a) by (conclude lemma_ray5).

assert (Per c b a) by (conclude lemma_8_3).

assert (Per a b c) by (conclude lemma_8_2).

close.

Qed.

End Euclid.