# Library GeoCoq.Elements.OriginalProofs.proposition_22

Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthannotequal.

Require Export GeoCoq.Elements.OriginalProofs.lemma_together.

Require Export GeoCoq.Elements.OriginalProofs.lemma_ray5.

Require Export GeoCoq.Elements.OriginalProofs.lemma_subtractequals.

Require Export GeoCoq.Elements.OriginalProofs.lemma_ray3.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_togethera

: ∀ A B C D F G P Q a b c : Point,

TG A a B b C c →

Cong D F A a →

Cong F G B b →

BetS D F G →

Cong P Q C c → Lt P Q D G.

Proof.

intros.

apply (lemma_together A B C D F G P Q a b c);auto.

Qed.

Lemma proposition_22 :

∀ A B C E F a b c,

TG A a B b C c → TG A a C c B b → TG B b C c A a → neq F E →

∃ X Y, Cong F X B b ∧ Cong F Y A a ∧ Cong X Y C c ∧ Out F E X ∧ Triangle F X Y.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ P, (BetS A a P ∧ Cong a P B b ∧ Lt C c A P)) by (conclude_def TG );destruct Tf as [P];spliter.

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

assert (neq a P) by (forward_using lemma_betweennotequal).

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

assert (neq C c) by (forward_using lemma_lessthannotequal).

let Tf:=fresh in

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

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

assert (neq F G) by (conclude lemma_nullsegment3).

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

rename_H H;let Tf:=fresh in

assert (Tf:∃ H, (BetS F G H ∧ Cong G H C c)) by (conclude postulate_extension);destruct Tf as [H];spliter.

let Tf:=fresh in

assert (Tf:∃ D, (BetS G F D ∧ Cong F D A a)) by (conclude postulate_extension);destruct Tf as [D];spliter.

assert (Cong D F A a) by (forward_using lemma_congruenceflip).

assert (BetS D F G) by (conclude axiom_betweennesssymmetry).

let Tf:=fresh in

assert (Tf:∃ L, CI L F A a) by (conclude circle);destruct Tf as [L];spliter.

let Tf:=fresh in

assert (Tf:∃ R, CI R G C c) by (conclude circle);destruct Tf as [R];spliter.

assert ((CI R G C c ∧ OnCirc H R)) by (conclude on).

assert (Lt D F F H) by (conclude lemma_together).

let Tf:=fresh in

assert (Tf:∃ M, (BetS F M H ∧ Cong F M D F)) by (conclude_def Lt );destruct Tf as [M];spliter.

assert (Cong F M A a) by (conclude lemma_congruencetransitive).

assert ((CI L F A a ∧ OutCirc H L)) by (conclude outside).

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

assert (Lt C c D G) by (conclude lemma_togethera).

assert (Cong D G G D) by (conclude cn_equalityreverse).

assert (Lt C c G D) by (conclude lemma_lessthancongruence).

let Tf:=fresh in

assert (Tf:∃ N, (BetS G N D ∧ Cong G N C c)) by (conclude_def Lt );destruct Tf as [N];spliter.

assert ((CI R G C c ∧ OnCirc H R)) by (conclude on).

assert (BetS D F H) by (conclude lemma_3_7b).

assert (BetS D F M) by (conclude axiom_innertransitivity).

assert (Cong F D A a) by (forward_using lemma_congruenceflip).

assert (BetS D N G) by (conclude axiom_betweennesssymmetry).

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

let Tf:=fresh in

assert (Tf:∃ J, (BetS F M J ∧ Cong M J C c)) by (conclude postulate_extension);destruct Tf as [J];spliter.

assert (BetS D F J) by (conclude lemma_3_7b).

assert ((Lt F G F J ∧ neq A a ∧ neq C c ∧ neq B b)) by (conclude lemma_together).

let Tf:=fresh in

assert (Tf:∃ Q, (BetS F Q J ∧ Cong F Q F G)) by (conclude_def Lt );destruct Tf as [Q];spliter.

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

assert (Out F J Q) by (conclude lemma_ray4).

assert (Out F G J) by (conclude_def Out ).

assert (Out F J G) by (conclude lemma_ray5).

assert (eq Q G) by (conclude lemma_layoffunique).

assert (eq G Q) by (conclude lemma_equalitysymmetric).

assert (BetS F G J) by (conclude cn_equalitysub).

assert (BetS D G J) by (conclude lemma_3_7a).

assert (Cong C c M J) by (conclude lemma_congruencesymmetric).

assert (Cong G N M J) by (conclude lemma_congruencetransitive).

assert (Cong N G M J) by (forward_using lemma_congruenceflip).

assert (BetS D M J) by (conclude lemma_3_7a).

assert (BetS D N J) by (conclude lemma_3_6b).

assert (BetS D N M) by (conclude lemma_subtractequals).

assert (Cong C c G N) by (conclude lemma_congruencesymmetric).

assert (Lt G N D G) by (conclude lemma_lessthancongruence2).

assert (neq N G) by (forward_using lemma_betweennotequal).

assert (neq G N) by (conclude lemma_inequalitysymmetric).

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

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

assert (Out G N D) by (conclude lemma_ray4).

assert (Out G F D) by (conclude lemma_ray4).

assert (Out G D N) by (conclude lemma_ray5).

assert (Out G D F) by (conclude lemma_ray5).

assert (Out G F N) by (conclude lemma_ray3).

assert (¬ (~ BetS F M G ∧ neq M G ∧ ¬ BetS F G M)).

{

intro.

assert (eq M G) by (conclude axiom_connectivity).

contradict.

}

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

assert (Out F G M) by (conclude lemma_ray4).

assert (Out F M G) by (conclude lemma_ray5).

assert (neq D M) by (forward_using lemma_betweennotequal).

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

assert ((CI L F A a ∧ InCirc N L)) by (conclude inside).

assert ((CI R G C c ∧ OnCirc N R)) by (conclude on).

let Tf:=fresh in

assert (Tf:∃ K, (OnCirc K L ∧ OnCirc K R)) by (conclude postulate_circle_circle);destruct Tf as [K];spliter.

assert (Cong F K A a) by (conclude on).

assert (Cong G K C c) by (conclude on).

assert (¬ Col F G K).

{

intro.

assert ((eq F G ∨ eq F K ∨ eq G K ∨ BetS G F K ∨ BetS F G K ∨ BetS F K G)) by (conclude_def Col ).

assert (nCol F G K).

by cases on (eq F G ∨ eq F K ∨ eq G K ∨ BetS G F K ∨ BetS F G K ∨ BetS F K G).

{

assert (¬ Col F G K).

{

intro.

contradict.

}

close.

}

{

assert (Cong A a F K) by (conclude lemma_congruencesymmetric).

assert (¬ Col F G K).

{

intro.

assert (neq F K) by (conclude lemma_nullsegment3).

contradict.

}

close.

}

{

assert (Cong C c G K) by (conclude lemma_congruencesymmetric).

assert (neq G K) by (conclude lemma_nullsegment3).

assert (¬ Col F G K).

{

intro.

assert (neq G K) by (conclude lemma_nullsegment3).

contradict.

}

close.

}

{

assert (BetS K F G) by (conclude axiom_betweennesssymmetry).

assert (Cong K F A a) by (forward_using lemma_congruenceflip).

let Tf:=fresh in

assert (Tf:∃ S, (BetS A a S ∧ Cong a S B b ∧ Lt C c A S)) by (conclude_def TG );destruct Tf as [S];spliter.

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

assert (Cong A a K F) by (conclude lemma_congruencesymmetric).

assert (Cong a S F G) by (conclude lemma_congruencetransitive).

assert (Cong A S K G) by (conclude lemma_sumofparts).

assert (Cong A S G K) by (forward_using lemma_congruenceflip).

assert (Lt C c G K) by (conclude lemma_lessthancongruence).

assert (Cong C c G K) by (conclude lemma_congruencesymmetric).

assert (Lt G K G K) by (conclude lemma_lessthancongruence2).

assert (¬ Col F G K).

{

intro.

assert (¬ Lt G K G K) by (conclude lemma_trichotomy2).

contradict.

}

close.

}

{

let Tf:=fresh in

assert (Tf:∃ S, (BetS B b S ∧ Cong b S C c ∧ Lt A a B S)) by (conclude_def TG );destruct Tf as [S];spliter.

assert (Cong C c b S) by (conclude lemma_congruencesymmetric).

assert (Cong G K b S) by (conclude lemma_congruencetransitive).

assert (Cong F K B S) by (conclude lemma_sumofparts).

assert (Cong A a F K) by (conclude lemma_congruencesymmetric).

assert (Lt F K B S) by (conclude lemma_lessthancongruence2).

assert (Cong B S F K) by (conclude lemma_congruencesymmetric).

assert (Lt F K F K) by (conclude lemma_lessthancongruence).

assert (¬ Col F G K).

{

intro.

assert (¬ Lt F K F K) by (conclude lemma_trichotomy2).

contradict.

}

close.

}

{

let Tf:=fresh in

assert (Tf:∃ S, (BetS A a S ∧ Cong a S C c ∧ Lt B b A S)) by (conclude_def TG );destruct Tf as [S];spliter.

assert (Lt F G A S) by (conclude lemma_lessthancongruence2).

assert (Cong C c a S) by (conclude lemma_congruencesymmetric).

assert (Cong G K a S) by (conclude lemma_congruencetransitive).

assert (Cong K G a S) by (forward_using lemma_congruenceflip).

assert (Cong F G A S) by (conclude lemma_sumofparts).

assert (Cong A S F G) by (conclude lemma_congruencesymmetric).

assert (Lt F G F G) by (conclude lemma_lessthancongruence).

assert (¬ Col F G K).

{

intro.

assert (¬ Lt F G F G) by (conclude lemma_trichotomy2).

contradict.

}

close.

}

contradict.

}

assert (Triangle F G K) by (conclude_def Triangle ).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_together.

Require Export GeoCoq.Elements.OriginalProofs.lemma_ray5.

Require Export GeoCoq.Elements.OriginalProofs.lemma_subtractequals.

Require Export GeoCoq.Elements.OriginalProofs.lemma_ray3.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_togethera

: ∀ A B C D F G P Q a b c : Point,

TG A a B b C c →

Cong D F A a →

Cong F G B b →

BetS D F G →

Cong P Q C c → Lt P Q D G.

Proof.

intros.

apply (lemma_together A B C D F G P Q a b c);auto.

Qed.

Lemma proposition_22 :

∀ A B C E F a b c,

TG A a B b C c → TG A a C c B b → TG B b C c A a → neq F E →

∃ X Y, Cong F X B b ∧ Cong F Y A a ∧ Cong X Y C c ∧ Out F E X ∧ Triangle F X Y.

Proof.

intros.

let Tf:=fresh in

assert (Tf:∃ P, (BetS A a P ∧ Cong a P B b ∧ Lt C c A P)) by (conclude_def TG );destruct Tf as [P];spliter.

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

assert (neq a P) by (forward_using lemma_betweennotequal).

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

assert (neq C c) by (forward_using lemma_lessthannotequal).

let Tf:=fresh in

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

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

assert (neq F G) by (conclude lemma_nullsegment3).

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

rename_H H;let Tf:=fresh in

assert (Tf:∃ H, (BetS F G H ∧ Cong G H C c)) by (conclude postulate_extension);destruct Tf as [H];spliter.

let Tf:=fresh in

assert (Tf:∃ D, (BetS G F D ∧ Cong F D A a)) by (conclude postulate_extension);destruct Tf as [D];spliter.

assert (Cong D F A a) by (forward_using lemma_congruenceflip).

assert (BetS D F G) by (conclude axiom_betweennesssymmetry).

let Tf:=fresh in

assert (Tf:∃ L, CI L F A a) by (conclude circle);destruct Tf as [L];spliter.

let Tf:=fresh in

assert (Tf:∃ R, CI R G C c) by (conclude circle);destruct Tf as [R];spliter.

assert ((CI R G C c ∧ OnCirc H R)) by (conclude on).

assert (Lt D F F H) by (conclude lemma_together).

let Tf:=fresh in

assert (Tf:∃ M, (BetS F M H ∧ Cong F M D F)) by (conclude_def Lt );destruct Tf as [M];spliter.

assert (Cong F M A a) by (conclude lemma_congruencetransitive).

assert ((CI L F A a ∧ OutCirc H L)) by (conclude outside).

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

assert (Lt C c D G) by (conclude lemma_togethera).

assert (Cong D G G D) by (conclude cn_equalityreverse).

assert (Lt C c G D) by (conclude lemma_lessthancongruence).

let Tf:=fresh in

assert (Tf:∃ N, (BetS G N D ∧ Cong G N C c)) by (conclude_def Lt );destruct Tf as [N];spliter.

assert ((CI R G C c ∧ OnCirc H R)) by (conclude on).

assert (BetS D F H) by (conclude lemma_3_7b).

assert (BetS D F M) by (conclude axiom_innertransitivity).

assert (Cong F D A a) by (forward_using lemma_congruenceflip).

assert (BetS D N G) by (conclude axiom_betweennesssymmetry).

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

let Tf:=fresh in

assert (Tf:∃ J, (BetS F M J ∧ Cong M J C c)) by (conclude postulate_extension);destruct Tf as [J];spliter.

assert (BetS D F J) by (conclude lemma_3_7b).

assert ((Lt F G F J ∧ neq A a ∧ neq C c ∧ neq B b)) by (conclude lemma_together).

let Tf:=fresh in

assert (Tf:∃ Q, (BetS F Q J ∧ Cong F Q F G)) by (conclude_def Lt );destruct Tf as [Q];spliter.

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

assert (Out F J Q) by (conclude lemma_ray4).

assert (Out F G J) by (conclude_def Out ).

assert (Out F J G) by (conclude lemma_ray5).

assert (eq Q G) by (conclude lemma_layoffunique).

assert (eq G Q) by (conclude lemma_equalitysymmetric).

assert (BetS F G J) by (conclude cn_equalitysub).

assert (BetS D G J) by (conclude lemma_3_7a).

assert (Cong C c M J) by (conclude lemma_congruencesymmetric).

assert (Cong G N M J) by (conclude lemma_congruencetransitive).

assert (Cong N G M J) by (forward_using lemma_congruenceflip).

assert (BetS D M J) by (conclude lemma_3_7a).

assert (BetS D N J) by (conclude lemma_3_6b).

assert (BetS D N M) by (conclude lemma_subtractequals).

assert (Cong C c G N) by (conclude lemma_congruencesymmetric).

assert (Lt G N D G) by (conclude lemma_lessthancongruence2).

assert (neq N G) by (forward_using lemma_betweennotequal).

assert (neq G N) by (conclude lemma_inequalitysymmetric).

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

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

assert (Out G N D) by (conclude lemma_ray4).

assert (Out G F D) by (conclude lemma_ray4).

assert (Out G D N) by (conclude lemma_ray5).

assert (Out G D F) by (conclude lemma_ray5).

assert (Out G F N) by (conclude lemma_ray3).

assert (¬ (~ BetS F M G ∧ neq M G ∧ ¬ BetS F G M)).

{

intro.

assert (eq M G) by (conclude axiom_connectivity).

contradict.

}

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

assert (Out F G M) by (conclude lemma_ray4).

assert (Out F M G) by (conclude lemma_ray5).

assert (neq D M) by (forward_using lemma_betweennotequal).

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

assert ((CI L F A a ∧ InCirc N L)) by (conclude inside).

assert ((CI R G C c ∧ OnCirc N R)) by (conclude on).

let Tf:=fresh in

assert (Tf:∃ K, (OnCirc K L ∧ OnCirc K R)) by (conclude postulate_circle_circle);destruct Tf as [K];spliter.

assert (Cong F K A a) by (conclude on).

assert (Cong G K C c) by (conclude on).

assert (¬ Col F G K).

{

intro.

assert ((eq F G ∨ eq F K ∨ eq G K ∨ BetS G F K ∨ BetS F G K ∨ BetS F K G)) by (conclude_def Col ).

assert (nCol F G K).

by cases on (eq F G ∨ eq F K ∨ eq G K ∨ BetS G F K ∨ BetS F G K ∨ BetS F K G).

{

assert (¬ Col F G K).

{

intro.

contradict.

}

close.

}

{

assert (Cong A a F K) by (conclude lemma_congruencesymmetric).

assert (¬ Col F G K).

{

intro.

assert (neq F K) by (conclude lemma_nullsegment3).

contradict.

}

close.

}

{

assert (Cong C c G K) by (conclude lemma_congruencesymmetric).

assert (neq G K) by (conclude lemma_nullsegment3).

assert (¬ Col F G K).

{

intro.

assert (neq G K) by (conclude lemma_nullsegment3).

contradict.

}

close.

}

{

assert (BetS K F G) by (conclude axiom_betweennesssymmetry).

assert (Cong K F A a) by (forward_using lemma_congruenceflip).

let Tf:=fresh in

assert (Tf:∃ S, (BetS A a S ∧ Cong a S B b ∧ Lt C c A S)) by (conclude_def TG );destruct Tf as [S];spliter.

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

assert (Cong A a K F) by (conclude lemma_congruencesymmetric).

assert (Cong a S F G) by (conclude lemma_congruencetransitive).

assert (Cong A S K G) by (conclude lemma_sumofparts).

assert (Cong A S G K) by (forward_using lemma_congruenceflip).

assert (Lt C c G K) by (conclude lemma_lessthancongruence).

assert (Cong C c G K) by (conclude lemma_congruencesymmetric).

assert (Lt G K G K) by (conclude lemma_lessthancongruence2).

assert (¬ Col F G K).

{

intro.

assert (¬ Lt G K G K) by (conclude lemma_trichotomy2).

contradict.

}

close.

}

{

let Tf:=fresh in

assert (Tf:∃ S, (BetS B b S ∧ Cong b S C c ∧ Lt A a B S)) by (conclude_def TG );destruct Tf as [S];spliter.

assert (Cong C c b S) by (conclude lemma_congruencesymmetric).

assert (Cong G K b S) by (conclude lemma_congruencetransitive).

assert (Cong F K B S) by (conclude lemma_sumofparts).

assert (Cong A a F K) by (conclude lemma_congruencesymmetric).

assert (Lt F K B S) by (conclude lemma_lessthancongruence2).

assert (Cong B S F K) by (conclude lemma_congruencesymmetric).

assert (Lt F K F K) by (conclude lemma_lessthancongruence).

assert (¬ Col F G K).

{

intro.

assert (¬ Lt F K F K) by (conclude lemma_trichotomy2).

contradict.

}

close.

}

{

let Tf:=fresh in

assert (Tf:∃ S, (BetS A a S ∧ Cong a S C c ∧ Lt B b A S)) by (conclude_def TG );destruct Tf as [S];spliter.

assert (Lt F G A S) by (conclude lemma_lessthancongruence2).

assert (Cong C c a S) by (conclude lemma_congruencesymmetric).

assert (Cong G K a S) by (conclude lemma_congruencetransitive).

assert (Cong K G a S) by (forward_using lemma_congruenceflip).

assert (Cong F G A S) by (conclude lemma_sumofparts).

assert (Cong A S F G) by (conclude lemma_congruencesymmetric).

assert (Lt F G F G) by (conclude lemma_lessthancongruence).

assert (¬ Col F G K).

{

intro.

assert (¬ Lt F G F G) by (conclude lemma_trichotomy2).

contradict.

}

close.

}

contradict.

}

assert (Triangle F G K) by (conclude_def Triangle ).

close.

Qed.

End Euclid.