# Library GeoCoq.Elements.OriginalProofs.lemma_10_12

Require Export GeoCoq.Elements.OriginalProofs.lemma_linereflectionisometry.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_10_12 :

∀ A B C H,

Per A B C → Per A B H → Cong B C B H →

Cong A C A H.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ D, (BetS A B D ∧ Cong A B D B ∧ Cong A C D C ∧ neq B C)) by (conclude_def Per );destruct Tf as [D];spliter.

assert (neq B H) by (conclude_def Per ).

let Tf:=fresh in

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

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

assert (Cong D B A B) by (conclude lemma_congruencesymmetric).

assert (Cong D B F B) by (conclude lemma_congruencetransitive).

assert (Cong B F B D) by (forward_using lemma_doublereverse).

assert (eq F D) by (conclude lemma_extensionunique).

assert (Cong A H D H) by (conclude cn_equalitysub).

assert (Cong A C A H).

by cases on (eq C H ∨ neq C H).

{

assert (Cong A C A C) by (conclude cn_congruencereflexive).

assert (Cong A C A H) by (conclude cn_equalitysub).

close.

}

{

let Tf:=fresh in

assert (Tf:∃ M, (BetS C M H ∧ Cong M C M H)) by (conclude proposition_10);destruct Tf as [M];spliter.

assert (Cong C B H B) by (forward_using lemma_doublereverse).

assert (Cong A C A H).

by cases on (eq B M ∨ neq B M).

{

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

assert (BetS C B H) by (conclude cn_equalitysub).

assert (Cong B C B H) by (conclude cn_equalitysub).

assert (Cong C B B H) by (forward_using lemma_congruenceflip).

assert (Cong C A H A) by (conclude lemma_rightreverse).

assert (Cong A C A H) by (forward_using lemma_congruenceflip).

close.

}

{

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

assert (Cong C M H M) by (forward_using lemma_congruenceflip).

assert (Per C M B) by (conclude_def Per ).

assert (Per B M C) by (conclude lemma_8_2).

assert (Cong C A C D) by (forward_using lemma_congruenceflip).

assert (Cong H A H D) by (forward_using lemma_congruenceflip).

assert (Cong C M C M) by (conclude cn_congruencereflexive).

assert (Cong M H M H) by (conclude cn_congruencereflexive).

assert (Cong M A M D) by (conclude lemma_interior5).

assert (Cong A M D M) by (forward_using lemma_congruenceflip).

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

assert (Per A B M) by (conclude_def Per ).

assert (Cong B A B D) by (forward_using lemma_congruenceflip).

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

assert (Cong C A H D) by (conclude lemma_linereflectionisometry).

assert (Cong A C D H) by (forward_using lemma_congruenceflip).

assert (BetS D B A) by (conclude axiom_betweennesssymmetry).

assert (Cong B D B A) by (forward_using lemma_congruenceflip).

assert (Cong A B B D) by (forward_using lemma_congruenceflip).

assert (Cong A H D H) by (conclude lemma_rightreverse).

assert (Cong D H A H) by (conclude lemma_congruencesymmetric).

assert (Cong C A H D) by (forward_using lemma_congruenceflip).

assert (Cong H D H A) by (forward_using lemma_congruenceflip).

assert (Cong C A H A) by (conclude lemma_congruencetransitive).

assert (Cong A C A H) by (forward_using lemma_congruenceflip).

close.

}

close.

}

close.

Qed.

End Euclid.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_10_12 :

∀ A B C H,

Per A B C → Per A B H → Cong B C B H →

Cong A C A H.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ D, (BetS A B D ∧ Cong A B D B ∧ Cong A C D C ∧ neq B C)) by (conclude_def Per );destruct Tf as [D];spliter.

assert (neq B H) by (conclude_def Per ).

let Tf:=fresh in

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

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

assert (Cong D B A B) by (conclude lemma_congruencesymmetric).

assert (Cong D B F B) by (conclude lemma_congruencetransitive).

assert (Cong B F B D) by (forward_using lemma_doublereverse).

assert (eq F D) by (conclude lemma_extensionunique).

assert (Cong A H D H) by (conclude cn_equalitysub).

assert (Cong A C A H).

by cases on (eq C H ∨ neq C H).

{

assert (Cong A C A C) by (conclude cn_congruencereflexive).

assert (Cong A C A H) by (conclude cn_equalitysub).

close.

}

{

let Tf:=fresh in

assert (Tf:∃ M, (BetS C M H ∧ Cong M C M H)) by (conclude proposition_10);destruct Tf as [M];spliter.

assert (Cong C B H B) by (forward_using lemma_doublereverse).

assert (Cong A C A H).

by cases on (eq B M ∨ neq B M).

{

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

assert (BetS C B H) by (conclude cn_equalitysub).

assert (Cong B C B H) by (conclude cn_equalitysub).

assert (Cong C B B H) by (forward_using lemma_congruenceflip).

assert (Cong C A H A) by (conclude lemma_rightreverse).

assert (Cong A C A H) by (forward_using lemma_congruenceflip).

close.

}

{

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

assert (Cong C M H M) by (forward_using lemma_congruenceflip).

assert (Per C M B) by (conclude_def Per ).

assert (Per B M C) by (conclude lemma_8_2).

assert (Cong C A C D) by (forward_using lemma_congruenceflip).

assert (Cong H A H D) by (forward_using lemma_congruenceflip).

assert (Cong C M C M) by (conclude cn_congruencereflexive).

assert (Cong M H M H) by (conclude cn_congruencereflexive).

assert (Cong M A M D) by (conclude lemma_interior5).

assert (Cong A M D M) by (forward_using lemma_congruenceflip).

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

assert (Per A B M) by (conclude_def Per ).

assert (Cong B A B D) by (forward_using lemma_congruenceflip).

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

assert (Cong C A H D) by (conclude lemma_linereflectionisometry).

assert (Cong A C D H) by (forward_using lemma_congruenceflip).

assert (BetS D B A) by (conclude axiom_betweennesssymmetry).

assert (Cong B D B A) by (forward_using lemma_congruenceflip).

assert (Cong A B B D) by (forward_using lemma_congruenceflip).

assert (Cong A H D H) by (conclude lemma_rightreverse).

assert (Cong D H A H) by (conclude lemma_congruencesymmetric).

assert (Cong C A H D) by (forward_using lemma_congruenceflip).

assert (Cong H D H A) by (forward_using lemma_congruenceflip).

assert (Cong C A H A) by (conclude lemma_congruencetransitive).

assert (Cong A C A H) by (forward_using lemma_congruenceflip).

close.

}

close.

}

close.

Qed.

End Euclid.