# Library GeoCoq.Elements.OriginalProofs.proposition_09

Require Export GeoCoq.Elements.OriginalProofs.proposition_10.

Require Export GeoCoq.Elements.OriginalProofs.lemma_ABCequalsCBA.

Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglestransitive.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_09 :

∀ A B C,

nCol B A C →

∃ X, CongA B A X X A C ∧ InAngle B A C X.

Proof.

intros.

assert (¬ eq A B).

{

intro.

assert (eq B A) by (conclude lemma_equalitysymmetric).

assert (Col B A C) by (conclude_def Col ).

contradict.

}

assert (¬ eq A C).

{

intro.

assert (Col B A C) by (conclude_def Col ).

contradict.

}

let Tf:=fresh in

assert (Tf:∃ E, (Out A C E ∧ Cong A E A B)) by (conclude lemma_layoff);destruct Tf as [E];spliter.

assert (¬ eq B E).

{

intro.

assert (Col A B E) by (conclude_def Col ).

assert (Col A C E) by (conclude lemma_rayimpliescollinear).

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

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

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

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

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

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ F, (BetS B F E ∧ Cong F B F E)) by (conclude proposition_10);destruct Tf as [F];spliter.

assert (eq B B) by (conclude cn_equalityreflexive).

assert (eq F F) by (conclude cn_equalityreflexive).

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

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

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

assert (Cong B F E F) by (conclude lemma_congruencesymmetric).

assert (¬ Col B A F).

{

intro.

assert (Col B F E) by (conclude_def Col ).

assert (Col F B E) by (forward_using lemma_collinearorder).

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

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

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

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

assert (Col A C E) by (conclude lemma_rayimpliescollinear).

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

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

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

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

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

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

contradict.

}

assert (Out A B B) by (conclude lemma_ray4).

assert (¬ eq A F).

{

intro.

assert (Col B A F) by (conclude_def Col ).

contradict.

}

assert (Out A F F) by (conclude lemma_ray4).

assert (CongA B A F C A F) by (conclude_def CongA ).

assert (CongA C A F B A F) by (conclude lemma_equalanglessymmetric).

assert (nCol C A F) by (conclude_def CongA ).

assert (CongA C A F F A C) by (conclude lemma_ABCequalsCBA).

assert (CongA B A F F A C) by (conclude lemma_equalanglestransitive).

assert (InAngle B A C F) by (conclude_def InAngle ).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_ABCequalsCBA.

Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglestransitive.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_09 :

∀ A B C,

nCol B A C →

∃ X, CongA B A X X A C ∧ InAngle B A C X.

Proof.

intros.

assert (¬ eq A B).

{

intro.

assert (eq B A) by (conclude lemma_equalitysymmetric).

assert (Col B A C) by (conclude_def Col ).

contradict.

}

assert (¬ eq A C).

{

intro.

assert (Col B A C) by (conclude_def Col ).

contradict.

}

let Tf:=fresh in

assert (Tf:∃ E, (Out A C E ∧ Cong A E A B)) by (conclude lemma_layoff);destruct Tf as [E];spliter.

assert (¬ eq B E).

{

intro.

assert (Col A B E) by (conclude_def Col ).

assert (Col A C E) by (conclude lemma_rayimpliescollinear).

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

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

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

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

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

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ F, (BetS B F E ∧ Cong F B F E)) by (conclude proposition_10);destruct Tf as [F];spliter.

assert (eq B B) by (conclude cn_equalityreflexive).

assert (eq F F) by (conclude cn_equalityreflexive).

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

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

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

assert (Cong B F E F) by (conclude lemma_congruencesymmetric).

assert (¬ Col B A F).

{

intro.

assert (Col B F E) by (conclude_def Col ).

assert (Col F B E) by (forward_using lemma_collinearorder).

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

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

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

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

assert (Col A C E) by (conclude lemma_rayimpliescollinear).

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

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

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

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

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

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

contradict.

}

assert (Out A B B) by (conclude lemma_ray4).

assert (¬ eq A F).

{

intro.

assert (Col B A F) by (conclude_def Col ).

contradict.

}

assert (Out A F F) by (conclude lemma_ray4).

assert (CongA B A F C A F) by (conclude_def CongA ).

assert (CongA C A F B A F) by (conclude lemma_equalanglessymmetric).

assert (nCol C A F) by (conclude_def CongA ).

assert (CongA C A F F A C) by (conclude lemma_ABCequalsCBA).

assert (CongA B A F F A C) by (conclude lemma_equalanglestransitive).

assert (InAngle B A C F) by (conclude_def InAngle ).

close.

Qed.

End Euclid.