Library GeoCoq.Elements.OriginalProofs.proposition_24
Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglesflip.
Require Export GeoCoq.Elements.OriginalProofs.proposition_19.
Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthancongruence2.
Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma proposition_24 :
∀ A B C D E F,
Triangle A B C → Triangle D E F → Cong A B D E → Cong A C D F → LtA E D F B A C →
Lt E F B C.
Proof.
intros.
assert (nCol D E F) by (conclude_def Triangle ).
assert (¬ eq D E).
{
intro.
assert (Col D E F) by (conclude_def Col ).
contradict.
}
assert (nCol A B C) by (conclude_def Triangle ).
assert (¬ Col B A C).
{
intro.
assert (Col A B C) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ eq A B).
{
intro.
assert (Col A B C) by (conclude_def Col ).
contradict.
}
assert (¬ eq A C).
{
intro.
assert (Col A B C) by (conclude_def Col ).
contradict.
}
assert (neq C A) by (conclude lemma_inequalitysymmetric).
assert (¬ eq B C).
{
intro.
assert (Col A B C) by (conclude_def Col ).
contradict.
}
assert (neq C B) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ P Q T, (BetS P T Q ∧ Out A B P ∧ Out A C Q ∧ CongA E D F B A T)) by (conclude_def LtA );destruct Tf as [P[Q[T]]];spliter.
assert (nCol B A T) by (conclude lemma_equalanglesNC).
assert (¬ eq A T).
{
intro.
assert (Col B A T) by (conclude_def Col ).
contradict.
}
assert (nCol A B C) by (conclude_def Triangle ).
assert (¬ eq A C).
{
intro.
assert (Col A B C) by (conclude_def Col ).
contradict.
}
rename_H H;let Tf:=fresh in
assert (Tf:∃ H, (Out A T H ∧ Cong A H A C)) by (conclude lemma_layoff);destruct Tf as [H];spliter.
assert (Cong A H D F) by (conclude lemma_congruencetransitive).
assert (nCol B A T) by (conclude lemma_equalanglesNC).
assert (¬ Col H A B).
{
intro.
assert (Col A T H) by (conclude lemma_rayimpliescollinear).
assert (Col H A T) by (forward_using lemma_collinearorder).
assert (neq A H) by (conclude lemma_raystrict).
assert (neq H A) by (conclude lemma_inequalitysymmetric).
assert (Col A B T) by (conclude lemma_collinear4).
assert (Col B A T) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ eq H B).
{
intro.
assert (Col H A B) by (conclude_def Col ).
contradict.
}
assert (Triangle H A B) by (conclude_def Triangle ).
assert (CongA B A T E D F) by (conclude lemma_equalanglessymmetric).
assert (nCol E D F) by (conclude lemma_equalanglesNC).
assert (¬ Col F D E).
{
intro.
assert (Col E D F) by (forward_using lemma_collinearorder).
contradict.
}
assert (Triangle F D E) by (conclude_def Triangle ).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Out A B B) by (conclude lemma_ray4).
assert (CongA E D F B A H) by (conclude lemma_equalangleshelper).
assert (CongA B A H E D F) by (conclude lemma_equalanglessymmetric).
assert (CongA H A B F D E) by (conclude lemma_equalanglesflip).
assert ((Cong H B F E ∧ CongA A H B D F E ∧ CongA A B H D E F)) by (conclude proposition_04).
assert (Out A Q C) by (conclude lemma_ray5).
assert (Out A P B) by (conclude lemma_ray5).
assert (Col A Q C) by (conclude lemma_rayimpliescollinear).
assert (Col A P B) by (conclude lemma_rayimpliescollinear).
assert (¬ Col Q A P).
{
intro.
assert (Col A P Q) by (forward_using lemma_collinearorder).
assert (Col Q A C) by (forward_using lemma_collinearorder).
assert (Col Q A P) by (forward_using lemma_collinearorder).
assert (neq A Q) by (conclude lemma_ray2).
assert (neq Q A) by (conclude lemma_inequalitysymmetric).
assert (Col A C P) by (conclude lemma_collinear4).
assert (Col P A B) by (forward_using lemma_collinearorder).
assert (Col P A C) by (forward_using lemma_collinearorder).
assert (neq A P) by (conclude lemma_raystrict).
assert (neq P A) by (conclude lemma_inequalitysymmetric).
assert (Col A B C) by (conclude lemma_collinear4).
contradict.
}
assert (Triangle Q A P) by (conclude_def Triangle ).
assert (BetS Q T P) by (conclude axiom_betweennesssymmetry).
let Tf:=fresh in
assert (Tf:∃ J, (Out A T J ∧ BetS C J B)) by (conclude lemma_crossbar);destruct Tf as [J];spliter.
assert (Out A J H) by (conclude lemma_ray3).
assert (Cong A C A H) by (conclude lemma_congruencesymmetric).
assert (¬ Col A C H).
{
intro.
assert (Col A T H) by (conclude lemma_rayimpliescollinear).
assert (Col H A T) by (forward_using lemma_collinearorder).
assert (Col H A C) by (forward_using lemma_collinearorder).
assert (neq A H) by (conclude lemma_raystrict).
assert (neq H A) by (conclude lemma_inequalitysymmetric).
assert (Col A T C) by (conclude lemma_collinear4).
assert (Col A J H) by (conclude lemma_rayimpliescollinear).
assert (Col H A J) by (forward_using lemma_collinearorder).
assert (Col A C J) by (conclude lemma_collinear4).
assert (Col C J B) by (conclude_def Col ).
assert (Col C J A) by (forward_using lemma_collinearorder).
assert (neq C J) by (forward_using lemma_betweennotequal).
assert (Col J B A) by (conclude lemma_collinear4).
assert (Col A T J) by (conclude lemma_rayimpliescollinear).
assert (Col J A T) by (forward_using lemma_collinearorder).
assert (Col J A B) by (forward_using lemma_collinearorder).
assert (neq A J) by (conclude lemma_raystrict).
assert (neq J A) by (conclude lemma_inequalitysymmetric).
assert (Col A T B) by (conclude lemma_collinear4).
assert (Col B A T) by (forward_using lemma_collinearorder).
contradict.
}
assert (Triangle A C H) by (conclude_def Triangle ).
assert (isosceles A C H) by (conclude_def isosceles ).
assert (CongA A C H A H C) by (conclude proposition_05).
assert ((BetS A H J ∨ eq J H ∨ BetS A J H)) by (conclude lemma_ray1).
assert (Lt H B C B).
by cases on (BetS A H J ∨ eq J H ∨ BetS A J H).
{
assert (¬ Col C J H).
{
intro.
assert (Col A H J) by (conclude_def Col ).
assert (Col J H A) by (forward_using lemma_collinearorder).
assert (Col J H C) by (forward_using lemma_collinearorder).
assert (neq H J) by (forward_using lemma_betweennotequal).
assert (neq J H) by (conclude lemma_inequalitysymmetric).
assert (Col H A C) by (conclude lemma_collinear4).
assert (Col A C H) by (forward_using lemma_collinearorder).
contradict.
}
assert (Triangle C J H) by (conclude_def Triangle ).
assert (BetS J H A) by (conclude axiom_betweennesssymmetry).
assert (LtA J C H C H A) by (conclude proposition_16).
assert (¬ Col H C J).
{
intro.
assert (Col C J H) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA H C J J C H) by (conclude lemma_ABCequalsCBA).
assert (LtA H C J C H A) by (conclude lemma_angleorderrespectscongruence2).
assert (¬ Col A H C).
{
intro.
assert (Col A C H) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA A H C C H A) by (conclude lemma_ABCequalsCBA).
assert (neq C H) by (forward_using lemma_angledistinct).
assert (neq H C) by (conclude lemma_inequalitysymmetric).
assert (LtA H C J A H C) by (conclude lemma_angleorderrespectscongruence).
assert (Out H B B) by (conclude lemma_ray4).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (¬ Col C H J).
{
intro.
assert (Col C J H) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ eq C H).
{
intro.
assert (Col C H J) by (conclude_def Col ).
contradict.
}
assert (neq H C) by (conclude lemma_inequalitysymmetric).
assert (Out H C C) by (conclude lemma_ray4).
assert (CongA C H J C H J) by (conclude lemma_equalanglesreflexive).
assert (neq C J) by (forward_using lemma_angledistinct).
assert (neq C H) by (forward_using lemma_angledistinct).
assert (LtA C H J C H B) by (conclude_def LtA ).
assert (¬ Col C A H).
{
intro.
assert (Col A C H) by (forward_using lemma_collinearorder).
contradict.
}
assert (Triangle C A H) by (conclude_def Triangle ).
assert (LtA A C H C H J) by (conclude proposition_16).
assert (LtA H C J A C H) by (conclude lemma_angleorderrespectscongruence).
assert (LtA H C J C H J) by (conclude lemma_angleordertransitive).
assert (LtA H C J C H B) by (conclude lemma_angleordertransitive).
assert (eq H H) by (conclude cn_equalityreflexive).
assert (Out C H H) by (conclude lemma_ray4).
assert (Out C J B) by (conclude lemma_ray4).
assert (CongA H C J H C J) by (conclude lemma_equalanglesreflexive).
assert (CongA H C J H C B) by (conclude lemma_equalangleshelper).
assert (CongA H C B H C J) by (conclude lemma_equalanglessymmetric).
assert (LtA H C B C H B) by (conclude lemma_angleorderrespectscongruence2).
assert (¬ Col B H C).
{
intro.
assert (Col C J B) by (conclude_def Col ).
assert (Col B C H) by (forward_using lemma_collinearorder).
assert (Col B C J) by (forward_using lemma_collinearorder).
assert (neq C B) by (forward_using lemma_betweennotequal).
assert (neq B C) by (conclude lemma_inequalitysymmetric).
assert (Col C H J) by (conclude lemma_collinear4).
contradict.
}
assert (Triangle B H C) by (conclude_def Triangle ).
assert (CongA B H C C H B) by (conclude lemma_ABCequalsCBA).
assert (LtA H C B B H C) by (conclude lemma_angleorderrespectscongruence).
assert (Lt B H B C) by (conclude proposition_19).
assert (Cong B H H B) by (conclude cn_equalityreverse).
assert (Lt H B B C) by (conclude lemma_lessthancongruence2).
assert (Cong B C C B) by (conclude cn_equalityreverse).
assert (Lt H B C B) by (conclude lemma_lessthancongruence).
close.
}
{
assert (BetS C H B) by (conclude cn_equalitysub).
assert (BetS B H C) by (conclude axiom_betweennesssymmetry).
assert (Cong B H H B) by (conclude cn_equalityreverse).
assert (Lt H B B C) by (conclude_def Lt ).
assert (Cong B C C B) by (conclude cn_equalityreverse).
assert (Lt H B C B) by (conclude lemma_lessthancongruence).
close.
}
{
assert (BetS H J A) by (conclude axiom_betweennesssymmetry).
assert (Cong C A C A) by (conclude cn_congruencereflexive).
assert (Cong C H C H) by (conclude cn_congruencereflexive).
assert (¬ Col C J H).
{
intro.
assert (Col A H J) by (conclude_def Col ).
assert (Col J H A) by (forward_using lemma_collinearorder).
assert (Col J H C) by (forward_using lemma_collinearorder).
assert (neq H J) by (forward_using lemma_betweennotequal).
assert (neq J H) by (conclude lemma_inequalitysymmetric).
assert (Col H A C) by (conclude lemma_collinear4).
assert (Col A C H) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ Col H C B).
{
intro.
assert (Col C J B) by (conclude_def Col ).
assert (Col B C J) by (forward_using lemma_collinearorder).
assert (Col B C H) by (forward_using lemma_collinearorder).
assert (neq C B) by (forward_using lemma_betweennotequal).
assert (neq B C) by (conclude lemma_inequalitysymmetric).
assert (Col C H J) by (conclude lemma_collinear4).
assert (Col C J H) by (forward_using lemma_collinearorder).
contradict.
}
assert (eq H H) by (conclude cn_equalityreflexive).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (¬ eq C H).
{
intro.
assert (Col C H B) by (conclude_def Col ).
assert (Col H C B) by (forward_using lemma_collinearorder).
contradict.
}
assert (Out C H H) by (conclude lemma_ray4).
assert (Out C A A) by (conclude lemma_ray4).
assert (CongA H C B H C B) by (conclude lemma_equalanglesreflexive).
assert (Out C B J) by (conclude lemma_ray4).
assert (Out C H H) by (conclude lemma_ray4).
assert (CongA H C B H C J) by (conclude lemma_equalangleshelper).
assert (BetS H J A) by (conclude axiom_betweennesssymmetry).
assert (LtA H C B H C A) by (conclude_def LtA ).
assert (¬ Col B C H).
{
intro.
assert (Col H C B) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA B C H H C B) by (conclude lemma_ABCequalsCBA).
assert (LtA B C H H C A) by (conclude lemma_angleorderrespectscongruence2).
assert (CongA A C H H C A) by (conclude lemma_ABCequalsCBA).
assert (LtA B C H A C H) by (conclude lemma_angleorderrespectscongruence).
assert (CongA A H C A C H) by (conclude lemma_equalanglessymmetric).
assert (LtA B C H A H C) by (conclude lemma_angleorderrespectscongruence).
assert (¬ Col A H C).
{
intro.
assert (Col A C H) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA A H C C H A) by (conclude lemma_ABCequalsCBA).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (neq H B) by (forward_using lemma_angledistinct).
assert (neq H C) by (forward_using lemma_angledistinct).
assert (neq H A) by (forward_using lemma_angledistinct).
assert (Out H C C) by (conclude lemma_ray4).
assert (Out H B B) by (conclude lemma_ray4).
assert (Out H A J) by (conclude lemma_ray4).
assert (CongA A H C C H J) by (conclude lemma_equalangleshelper).
assert (LtA A H C C H B) by (conclude_def LtA ).
assert (¬ Col B H C).
{
intro.
assert (Col H C B) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA B H C C H B) by (conclude lemma_ABCequalsCBA).
assert (LtA A H C B H C) by (conclude lemma_angleorderrespectscongruence).
assert (LtA B C H B H C) by (conclude lemma_angleordertransitive).
assert (¬ Col H C B).
{
intro.
assert (Col B H C) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA H C B B C H) by (conclude lemma_ABCequalsCBA).
assert (LtA H C B B H C) by (conclude lemma_angleorderrespectscongruence2).
assert (Triangle B H C) by (conclude_def Triangle ).
assert (Lt B H B C) by (conclude proposition_19).
assert (Cong B H H B) by (conclude cn_equalityreverse).
assert (Lt H B B C) by (conclude lemma_lessthancongruence2).
assert (Cong B C C B) by (conclude cn_equalityreverse).
assert (Lt H B C B) by (conclude lemma_lessthancongruence).
close.
}
assert (Cong F E E F) by (conclude cn_equalityreverse).
assert (Cong H B E F) by (conclude lemma_congruencetransitive).
assert (Lt E F C B) by (conclude lemma_lessthancongruence2).
assert (Cong C B B C) by (conclude cn_equalityreverse).
assert (Lt E F B C) by (conclude lemma_lessthancongruence).
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.proposition_19.
Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthancongruence2.
Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma proposition_24 :
∀ A B C D E F,
Triangle A B C → Triangle D E F → Cong A B D E → Cong A C D F → LtA E D F B A C →
Lt E F B C.
Proof.
intros.
assert (nCol D E F) by (conclude_def Triangle ).
assert (¬ eq D E).
{
intro.
assert (Col D E F) by (conclude_def Col ).
contradict.
}
assert (nCol A B C) by (conclude_def Triangle ).
assert (¬ Col B A C).
{
intro.
assert (Col A B C) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ eq A B).
{
intro.
assert (Col A B C) by (conclude_def Col ).
contradict.
}
assert (¬ eq A C).
{
intro.
assert (Col A B C) by (conclude_def Col ).
contradict.
}
assert (neq C A) by (conclude lemma_inequalitysymmetric).
assert (¬ eq B C).
{
intro.
assert (Col A B C) by (conclude_def Col ).
contradict.
}
assert (neq C B) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ P Q T, (BetS P T Q ∧ Out A B P ∧ Out A C Q ∧ CongA E D F B A T)) by (conclude_def LtA );destruct Tf as [P[Q[T]]];spliter.
assert (nCol B A T) by (conclude lemma_equalanglesNC).
assert (¬ eq A T).
{
intro.
assert (Col B A T) by (conclude_def Col ).
contradict.
}
assert (nCol A B C) by (conclude_def Triangle ).
assert (¬ eq A C).
{
intro.
assert (Col A B C) by (conclude_def Col ).
contradict.
}
rename_H H;let Tf:=fresh in
assert (Tf:∃ H, (Out A T H ∧ Cong A H A C)) by (conclude lemma_layoff);destruct Tf as [H];spliter.
assert (Cong A H D F) by (conclude lemma_congruencetransitive).
assert (nCol B A T) by (conclude lemma_equalanglesNC).
assert (¬ Col H A B).
{
intro.
assert (Col A T H) by (conclude lemma_rayimpliescollinear).
assert (Col H A T) by (forward_using lemma_collinearorder).
assert (neq A H) by (conclude lemma_raystrict).
assert (neq H A) by (conclude lemma_inequalitysymmetric).
assert (Col A B T) by (conclude lemma_collinear4).
assert (Col B A T) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ eq H B).
{
intro.
assert (Col H A B) by (conclude_def Col ).
contradict.
}
assert (Triangle H A B) by (conclude_def Triangle ).
assert (CongA B A T E D F) by (conclude lemma_equalanglessymmetric).
assert (nCol E D F) by (conclude lemma_equalanglesNC).
assert (¬ Col F D E).
{
intro.
assert (Col E D F) by (forward_using lemma_collinearorder).
contradict.
}
assert (Triangle F D E) by (conclude_def Triangle ).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Out A B B) by (conclude lemma_ray4).
assert (CongA E D F B A H) by (conclude lemma_equalangleshelper).
assert (CongA B A H E D F) by (conclude lemma_equalanglessymmetric).
assert (CongA H A B F D E) by (conclude lemma_equalanglesflip).
assert ((Cong H B F E ∧ CongA A H B D F E ∧ CongA A B H D E F)) by (conclude proposition_04).
assert (Out A Q C) by (conclude lemma_ray5).
assert (Out A P B) by (conclude lemma_ray5).
assert (Col A Q C) by (conclude lemma_rayimpliescollinear).
assert (Col A P B) by (conclude lemma_rayimpliescollinear).
assert (¬ Col Q A P).
{
intro.
assert (Col A P Q) by (forward_using lemma_collinearorder).
assert (Col Q A C) by (forward_using lemma_collinearorder).
assert (Col Q A P) by (forward_using lemma_collinearorder).
assert (neq A Q) by (conclude lemma_ray2).
assert (neq Q A) by (conclude lemma_inequalitysymmetric).
assert (Col A C P) by (conclude lemma_collinear4).
assert (Col P A B) by (forward_using lemma_collinearorder).
assert (Col P A C) by (forward_using lemma_collinearorder).
assert (neq A P) by (conclude lemma_raystrict).
assert (neq P A) by (conclude lemma_inequalitysymmetric).
assert (Col A B C) by (conclude lemma_collinear4).
contradict.
}
assert (Triangle Q A P) by (conclude_def Triangle ).
assert (BetS Q T P) by (conclude axiom_betweennesssymmetry).
let Tf:=fresh in
assert (Tf:∃ J, (Out A T J ∧ BetS C J B)) by (conclude lemma_crossbar);destruct Tf as [J];spliter.
assert (Out A J H) by (conclude lemma_ray3).
assert (Cong A C A H) by (conclude lemma_congruencesymmetric).
assert (¬ Col A C H).
{
intro.
assert (Col A T H) by (conclude lemma_rayimpliescollinear).
assert (Col H A T) by (forward_using lemma_collinearorder).
assert (Col H A C) by (forward_using lemma_collinearorder).
assert (neq A H) by (conclude lemma_raystrict).
assert (neq H A) by (conclude lemma_inequalitysymmetric).
assert (Col A T C) by (conclude lemma_collinear4).
assert (Col A J H) by (conclude lemma_rayimpliescollinear).
assert (Col H A J) by (forward_using lemma_collinearorder).
assert (Col A C J) by (conclude lemma_collinear4).
assert (Col C J B) by (conclude_def Col ).
assert (Col C J A) by (forward_using lemma_collinearorder).
assert (neq C J) by (forward_using lemma_betweennotequal).
assert (Col J B A) by (conclude lemma_collinear4).
assert (Col A T J) by (conclude lemma_rayimpliescollinear).
assert (Col J A T) by (forward_using lemma_collinearorder).
assert (Col J A B) by (forward_using lemma_collinearorder).
assert (neq A J) by (conclude lemma_raystrict).
assert (neq J A) by (conclude lemma_inequalitysymmetric).
assert (Col A T B) by (conclude lemma_collinear4).
assert (Col B A T) by (forward_using lemma_collinearorder).
contradict.
}
assert (Triangle A C H) by (conclude_def Triangle ).
assert (isosceles A C H) by (conclude_def isosceles ).
assert (CongA A C H A H C) by (conclude proposition_05).
assert ((BetS A H J ∨ eq J H ∨ BetS A J H)) by (conclude lemma_ray1).
assert (Lt H B C B).
by cases on (BetS A H J ∨ eq J H ∨ BetS A J H).
{
assert (¬ Col C J H).
{
intro.
assert (Col A H J) by (conclude_def Col ).
assert (Col J H A) by (forward_using lemma_collinearorder).
assert (Col J H C) by (forward_using lemma_collinearorder).
assert (neq H J) by (forward_using lemma_betweennotequal).
assert (neq J H) by (conclude lemma_inequalitysymmetric).
assert (Col H A C) by (conclude lemma_collinear4).
assert (Col A C H) by (forward_using lemma_collinearorder).
contradict.
}
assert (Triangle C J H) by (conclude_def Triangle ).
assert (BetS J H A) by (conclude axiom_betweennesssymmetry).
assert (LtA J C H C H A) by (conclude proposition_16).
assert (¬ Col H C J).
{
intro.
assert (Col C J H) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA H C J J C H) by (conclude lemma_ABCequalsCBA).
assert (LtA H C J C H A) by (conclude lemma_angleorderrespectscongruence2).
assert (¬ Col A H C).
{
intro.
assert (Col A C H) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA A H C C H A) by (conclude lemma_ABCequalsCBA).
assert (neq C H) by (forward_using lemma_angledistinct).
assert (neq H C) by (conclude lemma_inequalitysymmetric).
assert (LtA H C J A H C) by (conclude lemma_angleorderrespectscongruence).
assert (Out H B B) by (conclude lemma_ray4).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (¬ Col C H J).
{
intro.
assert (Col C J H) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ eq C H).
{
intro.
assert (Col C H J) by (conclude_def Col ).
contradict.
}
assert (neq H C) by (conclude lemma_inequalitysymmetric).
assert (Out H C C) by (conclude lemma_ray4).
assert (CongA C H J C H J) by (conclude lemma_equalanglesreflexive).
assert (neq C J) by (forward_using lemma_angledistinct).
assert (neq C H) by (forward_using lemma_angledistinct).
assert (LtA C H J C H B) by (conclude_def LtA ).
assert (¬ Col C A H).
{
intro.
assert (Col A C H) by (forward_using lemma_collinearorder).
contradict.
}
assert (Triangle C A H) by (conclude_def Triangle ).
assert (LtA A C H C H J) by (conclude proposition_16).
assert (LtA H C J A C H) by (conclude lemma_angleorderrespectscongruence).
assert (LtA H C J C H J) by (conclude lemma_angleordertransitive).
assert (LtA H C J C H B) by (conclude lemma_angleordertransitive).
assert (eq H H) by (conclude cn_equalityreflexive).
assert (Out C H H) by (conclude lemma_ray4).
assert (Out C J B) by (conclude lemma_ray4).
assert (CongA H C J H C J) by (conclude lemma_equalanglesreflexive).
assert (CongA H C J H C B) by (conclude lemma_equalangleshelper).
assert (CongA H C B H C J) by (conclude lemma_equalanglessymmetric).
assert (LtA H C B C H B) by (conclude lemma_angleorderrespectscongruence2).
assert (¬ Col B H C).
{
intro.
assert (Col C J B) by (conclude_def Col ).
assert (Col B C H) by (forward_using lemma_collinearorder).
assert (Col B C J) by (forward_using lemma_collinearorder).
assert (neq C B) by (forward_using lemma_betweennotequal).
assert (neq B C) by (conclude lemma_inequalitysymmetric).
assert (Col C H J) by (conclude lemma_collinear4).
contradict.
}
assert (Triangle B H C) by (conclude_def Triangle ).
assert (CongA B H C C H B) by (conclude lemma_ABCequalsCBA).
assert (LtA H C B B H C) by (conclude lemma_angleorderrespectscongruence).
assert (Lt B H B C) by (conclude proposition_19).
assert (Cong B H H B) by (conclude cn_equalityreverse).
assert (Lt H B B C) by (conclude lemma_lessthancongruence2).
assert (Cong B C C B) by (conclude cn_equalityreverse).
assert (Lt H B C B) by (conclude lemma_lessthancongruence).
close.
}
{
assert (BetS C H B) by (conclude cn_equalitysub).
assert (BetS B H C) by (conclude axiom_betweennesssymmetry).
assert (Cong B H H B) by (conclude cn_equalityreverse).
assert (Lt H B B C) by (conclude_def Lt ).
assert (Cong B C C B) by (conclude cn_equalityreverse).
assert (Lt H B C B) by (conclude lemma_lessthancongruence).
close.
}
{
assert (BetS H J A) by (conclude axiom_betweennesssymmetry).
assert (Cong C A C A) by (conclude cn_congruencereflexive).
assert (Cong C H C H) by (conclude cn_congruencereflexive).
assert (¬ Col C J H).
{
intro.
assert (Col A H J) by (conclude_def Col ).
assert (Col J H A) by (forward_using lemma_collinearorder).
assert (Col J H C) by (forward_using lemma_collinearorder).
assert (neq H J) by (forward_using lemma_betweennotequal).
assert (neq J H) by (conclude lemma_inequalitysymmetric).
assert (Col H A C) by (conclude lemma_collinear4).
assert (Col A C H) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ Col H C B).
{
intro.
assert (Col C J B) by (conclude_def Col ).
assert (Col B C J) by (forward_using lemma_collinearorder).
assert (Col B C H) by (forward_using lemma_collinearorder).
assert (neq C B) by (forward_using lemma_betweennotequal).
assert (neq B C) by (conclude lemma_inequalitysymmetric).
assert (Col C H J) by (conclude lemma_collinear4).
assert (Col C J H) by (forward_using lemma_collinearorder).
contradict.
}
assert (eq H H) by (conclude cn_equalityreflexive).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (¬ eq C H).
{
intro.
assert (Col C H B) by (conclude_def Col ).
assert (Col H C B) by (forward_using lemma_collinearorder).
contradict.
}
assert (Out C H H) by (conclude lemma_ray4).
assert (Out C A A) by (conclude lemma_ray4).
assert (CongA H C B H C B) by (conclude lemma_equalanglesreflexive).
assert (Out C B J) by (conclude lemma_ray4).
assert (Out C H H) by (conclude lemma_ray4).
assert (CongA H C B H C J) by (conclude lemma_equalangleshelper).
assert (BetS H J A) by (conclude axiom_betweennesssymmetry).
assert (LtA H C B H C A) by (conclude_def LtA ).
assert (¬ Col B C H).
{
intro.
assert (Col H C B) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA B C H H C B) by (conclude lemma_ABCequalsCBA).
assert (LtA B C H H C A) by (conclude lemma_angleorderrespectscongruence2).
assert (CongA A C H H C A) by (conclude lemma_ABCequalsCBA).
assert (LtA B C H A C H) by (conclude lemma_angleorderrespectscongruence).
assert (CongA A H C A C H) by (conclude lemma_equalanglessymmetric).
assert (LtA B C H A H C) by (conclude lemma_angleorderrespectscongruence).
assert (¬ Col A H C).
{
intro.
assert (Col A C H) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA A H C C H A) by (conclude lemma_ABCequalsCBA).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (neq H B) by (forward_using lemma_angledistinct).
assert (neq H C) by (forward_using lemma_angledistinct).
assert (neq H A) by (forward_using lemma_angledistinct).
assert (Out H C C) by (conclude lemma_ray4).
assert (Out H B B) by (conclude lemma_ray4).
assert (Out H A J) by (conclude lemma_ray4).
assert (CongA A H C C H J) by (conclude lemma_equalangleshelper).
assert (LtA A H C C H B) by (conclude_def LtA ).
assert (¬ Col B H C).
{
intro.
assert (Col H C B) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA B H C C H B) by (conclude lemma_ABCequalsCBA).
assert (LtA A H C B H C) by (conclude lemma_angleorderrespectscongruence).
assert (LtA B C H B H C) by (conclude lemma_angleordertransitive).
assert (¬ Col H C B).
{
intro.
assert (Col B H C) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA H C B B C H) by (conclude lemma_ABCequalsCBA).
assert (LtA H C B B H C) by (conclude lemma_angleorderrespectscongruence2).
assert (Triangle B H C) by (conclude_def Triangle ).
assert (Lt B H B C) by (conclude proposition_19).
assert (Cong B H H B) by (conclude cn_equalityreverse).
assert (Lt H B B C) by (conclude lemma_lessthancongruence2).
assert (Cong B C C B) by (conclude cn_equalityreverse).
assert (Lt H B C B) by (conclude lemma_lessthancongruence).
close.
}
assert (Cong F E E F) by (conclude cn_equalityreverse).
assert (Cong H B E F) by (conclude lemma_congruencetransitive).
assert (Lt E F C B) by (conclude lemma_lessthancongruence2).
assert (Cong C B B C) by (conclude cn_equalityreverse).
assert (Lt E F B C) by (conclude lemma_lessthancongruence).
close.
Qed.
End Euclid.