Library GeoCoq.Elements.OriginalProofs.lemma_35helper
Require Export GeoCoq.Elements.OriginalProofs.proposition_34.
Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelNC.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NCdistinct.
Section Euclid.
Context `{Ax1:euclidean_euclidean}.
Lemma lemma_35helper :
∀ A B C D E F,
PG A B C D → PG E B C F → BetS A D F → Col A E F →
BetS A E F.
Proof.
intros.
assert ((Par A B C D ∧ Par A D B C)) by (conclude_def PG ).
assert ((Par E B C F ∧ Par E F B C)) by (conclude_def PG ).
assert (Par A B D C) by (forward_using lemma_parallelflip).
assert (Par E B F C) by (forward_using lemma_parallelflip).
assert (Cong A D B C) by (forward_using proposition_34).
assert (Cong E F B C) by (forward_using proposition_34).
assert (Cong B C E F) by (conclude lemma_congruencesymmetric).
assert (Cong A D E F) by (conclude lemma_congruencetransitive).
assert (Col A D F) by (conclude_def Col ).
assert (Col F A E) by (forward_using lemma_collinearorder).
assert (Col F A D) by (forward_using lemma_collinearorder).
assert (neq A F) by (forward_using lemma_betweennotequal).
assert (neq F A) by (conclude lemma_inequalitysymmetric).
assert (Col A E D) by (conclude lemma_collinear4).
let Tf:=fresh in
assert (Tf:∃ M, (BetS A M C ∧ BetS B M D)) by (conclude lemma_diagonalsmeet);destruct Tf as [M];spliter.
assert (BetS D M B) by (conclude axiom_betweennesssymmetry).
assert (BetS C M A) by (conclude axiom_betweennesssymmetry).
assert (BetS B M D) by (conclude axiom_betweennesssymmetry).
let Tf:=fresh in
assert (Tf:∃ m, (BetS E m C ∧ BetS B m F)) by (conclude lemma_diagonalsmeet);destruct Tf as [m];spliter.
assert (BetS F m B) by (conclude axiom_betweennesssymmetry).
assert (BetS B m F) by (conclude axiom_betweennesssymmetry).
assert (nCol A D B) by (forward_using lemma_parallelNC).
assert (Col A D F) by (conclude_def Col ).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A D A) by (conclude_def Col ).
assert (nCol A F B) by (conclude lemma_NChelper).
let Tf:=fresh in
assert (Tf:∃ Q, (BetS B Q F ∧ BetS A M Q)) by (conclude postulate_Pasch_outer);destruct Tf as [Q];spliter.
assert (Col A M Q) by (conclude_def Col ).
assert (Col A M C) by (conclude_def Col ).
assert (Col M A Q) by (forward_using lemma_collinearorder).
assert (Col M A C) by (forward_using lemma_collinearorder).
assert (neq A M) by (forward_using lemma_betweennotequal).
assert (neq M A) by (conclude lemma_inequalitysymmetric).
assert (Col A Q C) by (conclude lemma_collinear4).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col F A A) by (conclude_def Col ).
assert (Col C C B) by (conclude_def Col ).
assert (neq A F) by (forward_using lemma_betweennotequal).
assert (neq F A) by (conclude lemma_inequalitysymmetric).
assert (neq B C) by (conclude_def Par ).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert (¬ Meet F A C B).
{
intro.
let Tf:=fresh in
assert (Tf:∃ p, (neq F A ∧ neq C B ∧ Col F A p ∧ Col C B p)) by (conclude_def Meet );destruct Tf as [p];spliter.
assert (Col A D F) by (conclude_def Col ).
assert (Col F A D) by (forward_using lemma_collinearorder).
assert (neq A D) by (forward_using lemma_betweennotequal).
assert (Col A D p) by (conclude lemma_collinear4).
assert (Col B C p) by (forward_using lemma_collinearorder).
assert (Meet A D B C) by (conclude_def Meet ).
assert (¬ Meet A D B C) by (conclude_def Par ).
contradict.
}
assert (BetS F Q B) by (conclude axiom_betweennesssymmetry).
assert (¬ Meet A D B C) by (conclude_def Par ).
assert (Col A C Q) by (forward_using lemma_collinearorder).
assert (BetS A Q C) by (conclude lemma_collinearbetween).
assert (BetS C Q A) by (conclude axiom_betweennesssymmetry).
assert (¬ eq A E).
{
intro.
assert (Cong A F A F) by (conclude cn_congruencereflexive).
assert (Cong A F E F) by (conclude cn_equalitysub).
assert (Cong E F A D) by (conclude lemma_congruencesymmetric).
assert (Cong A F A D) by (conclude lemma_congruencetransitive).
assert (Cong A D A F) by (conclude lemma_congruencesymmetric).
assert (Cong A D A D) by (conclude cn_congruencereflexive).
assert (Lt A D A F) by (conclude_def Lt ).
assert (Lt A F A F) by (conclude lemma_lessthancongruence2).
assert (¬ Lt A F A F) by (conclude lemma_trichotomy2).
contradict.
}
assert (¬ BetS A F E).
{
intro.
assert (BetS E F A) by (conclude axiom_betweennesssymmetry).
assert (nCol A D C) by (forward_using lemma_parallelNC).
assert (Col A D E) by (forward_using lemma_collinearorder).
assert (nCol A E C) by (conclude lemma_NChelper).
assert (nCol C A E) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ r, (BetS C r F ∧ BetS E r Q)) by (conclude postulate_Pasch_inner);destruct Tf as [r];spliter.
assert (BetS Q r E) by (conclude axiom_betweennesssymmetry).
assert (nCol E B F) by (forward_using lemma_parallelNC).
assert (nCol F B E) by (forward_using lemma_NCorder).
rename_H H;let Tf:=fresh in
assert (Tf:∃ H, (BetS E H B ∧ BetS F r H)) by (conclude postulate_Pasch_outer);destruct Tf as [H];spliter.
assert (Col E H B) by (conclude_def Col ).
assert (Col F r H) by (conclude_def Col ).
assert (Col E B H) by (forward_using lemma_collinearorder).
assert (Col C r F) by (conclude_def Col ).
assert (Col r F C) by (forward_using lemma_collinearorder).
assert (Col r F H) by (forward_using lemma_collinearorder).
assert (neq r F) by (forward_using lemma_betweennotequal).
assert (Col F C H) by (conclude lemma_collinear4).
assert (neq B E) by (forward_using lemma_NCdistinct).
assert (neq E B) by (conclude lemma_inequalitysymmetric).
assert (neq F C) by (conclude_def Par ).
assert (Meet E B F C) by (conclude_def Meet ).
assert (¬ Meet E B F C) by (conclude_def Par ).
contradict.
}
assert (Col A F E) by (forward_using lemma_collinearorder).
assert ((eq A F ∨ eq A E ∨ eq F E ∨ BetS F A E ∨ BetS A F E ∨ BetS A E F)) by (conclude_def Col ).
assert (BetS A E F).
by cases on (eq A F ∨ eq A E ∨ eq F E ∨ BetS F A E ∨ BetS A F E ∨ BetS A E F).
{
assert (¬ ¬ BetS A E F).
{
intro.
assert (BetS A D A) by (conclude cn_equalitysub).
assert (¬ BetS A D A) by (conclude axiom_betweennessidentity).
contradict.
}
close.
}
{
assert (¬ ¬ BetS A E F).
{
intro.
contradict.
}
close.
}
{
assert (¬ ¬ BetS A E F).
{
intro.
assert (eq E F) by (conclude lemma_equalitysymmetric).
assert (Col B E F) by (conclude_def Col ).
assert (Col E B F) by (forward_using lemma_collinearorder).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (Col F C F) by (conclude_def Col ).
assert (neq E B) by (conclude_def Par ).
assert (neq F C) by (conclude_def Par ).
assert (Meet E B F C) by (conclude_def Meet ).
assert (¬ Meet E B F C) by (conclude_def Par ).
contradict.
}
close.
}
{
assert (¬ ¬ BetS A E F).
{
intro.
assert (BetS F D A) by (conclude axiom_betweennesssymmetry).
assert (BetS D A E) by (conclude lemma_3_6a).
assert (Cong D A D A) by (conclude cn_congruencereflexive).
assert (Lt D A D E) by (conclude_def Lt ).
assert (Cong D A A D) by (conclude cn_equalityreverse).
assert (Lt A D D E) by (conclude lemma_lessthancongruence2).
assert (Cong D E E D) by (conclude cn_equalityreverse).
assert (Lt A D E D) by (conclude lemma_lessthancongruence).
assert (Cong A D A D) by (conclude cn_congruencereflexive).
assert (Lt A D A F) by (conclude_def Lt ).
assert (Cong A D D A) by (conclude cn_equalityreverse).
assert (Lt D A A F) by (conclude lemma_lessthancongruence2).
assert (Cong A F F A) by (conclude cn_equalityreverse).
assert (Lt D A F A) by (conclude lemma_lessthancongruence).
assert (Cong F A F A) by (conclude cn_congruencereflexive).
assert (Lt F A F E) by (conclude_def Lt ).
assert (Lt D A F E) by (conclude lemma_lessthantransitive).
assert (Cong D A F E) by (forward_using lemma_congruenceflip).
assert (Lt F E F E) by (conclude lemma_lessthancongruence2).
assert (¬ Lt F E F E) by (conclude lemma_trichotomy2).
contradict.
}
close.
}
{
assert (¬ ¬ BetS A E F).
{
intro.
contradict.
}
close.
}
{
close.
}
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelNC.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NCdistinct.
Section Euclid.
Context `{Ax1:euclidean_euclidean}.
Lemma lemma_35helper :
∀ A B C D E F,
PG A B C D → PG E B C F → BetS A D F → Col A E F →
BetS A E F.
Proof.
intros.
assert ((Par A B C D ∧ Par A D B C)) by (conclude_def PG ).
assert ((Par E B C F ∧ Par E F B C)) by (conclude_def PG ).
assert (Par A B D C) by (forward_using lemma_parallelflip).
assert (Par E B F C) by (forward_using lemma_parallelflip).
assert (Cong A D B C) by (forward_using proposition_34).
assert (Cong E F B C) by (forward_using proposition_34).
assert (Cong B C E F) by (conclude lemma_congruencesymmetric).
assert (Cong A D E F) by (conclude lemma_congruencetransitive).
assert (Col A D F) by (conclude_def Col ).
assert (Col F A E) by (forward_using lemma_collinearorder).
assert (Col F A D) by (forward_using lemma_collinearorder).
assert (neq A F) by (forward_using lemma_betweennotequal).
assert (neq F A) by (conclude lemma_inequalitysymmetric).
assert (Col A E D) by (conclude lemma_collinear4).
let Tf:=fresh in
assert (Tf:∃ M, (BetS A M C ∧ BetS B M D)) by (conclude lemma_diagonalsmeet);destruct Tf as [M];spliter.
assert (BetS D M B) by (conclude axiom_betweennesssymmetry).
assert (BetS C M A) by (conclude axiom_betweennesssymmetry).
assert (BetS B M D) by (conclude axiom_betweennesssymmetry).
let Tf:=fresh in
assert (Tf:∃ m, (BetS E m C ∧ BetS B m F)) by (conclude lemma_diagonalsmeet);destruct Tf as [m];spliter.
assert (BetS F m B) by (conclude axiom_betweennesssymmetry).
assert (BetS B m F) by (conclude axiom_betweennesssymmetry).
assert (nCol A D B) by (forward_using lemma_parallelNC).
assert (Col A D F) by (conclude_def Col ).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A D A) by (conclude_def Col ).
assert (nCol A F B) by (conclude lemma_NChelper).
let Tf:=fresh in
assert (Tf:∃ Q, (BetS B Q F ∧ BetS A M Q)) by (conclude postulate_Pasch_outer);destruct Tf as [Q];spliter.
assert (Col A M Q) by (conclude_def Col ).
assert (Col A M C) by (conclude_def Col ).
assert (Col M A Q) by (forward_using lemma_collinearorder).
assert (Col M A C) by (forward_using lemma_collinearorder).
assert (neq A M) by (forward_using lemma_betweennotequal).
assert (neq M A) by (conclude lemma_inequalitysymmetric).
assert (Col A Q C) by (conclude lemma_collinear4).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col F A A) by (conclude_def Col ).
assert (Col C C B) by (conclude_def Col ).
assert (neq A F) by (forward_using lemma_betweennotequal).
assert (neq F A) by (conclude lemma_inequalitysymmetric).
assert (neq B C) by (conclude_def Par ).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert (¬ Meet F A C B).
{
intro.
let Tf:=fresh in
assert (Tf:∃ p, (neq F A ∧ neq C B ∧ Col F A p ∧ Col C B p)) by (conclude_def Meet );destruct Tf as [p];spliter.
assert (Col A D F) by (conclude_def Col ).
assert (Col F A D) by (forward_using lemma_collinearorder).
assert (neq A D) by (forward_using lemma_betweennotequal).
assert (Col A D p) by (conclude lemma_collinear4).
assert (Col B C p) by (forward_using lemma_collinearorder).
assert (Meet A D B C) by (conclude_def Meet ).
assert (¬ Meet A D B C) by (conclude_def Par ).
contradict.
}
assert (BetS F Q B) by (conclude axiom_betweennesssymmetry).
assert (¬ Meet A D B C) by (conclude_def Par ).
assert (Col A C Q) by (forward_using lemma_collinearorder).
assert (BetS A Q C) by (conclude lemma_collinearbetween).
assert (BetS C Q A) by (conclude axiom_betweennesssymmetry).
assert (¬ eq A E).
{
intro.
assert (Cong A F A F) by (conclude cn_congruencereflexive).
assert (Cong A F E F) by (conclude cn_equalitysub).
assert (Cong E F A D) by (conclude lemma_congruencesymmetric).
assert (Cong A F A D) by (conclude lemma_congruencetransitive).
assert (Cong A D A F) by (conclude lemma_congruencesymmetric).
assert (Cong A D A D) by (conclude cn_congruencereflexive).
assert (Lt A D A F) by (conclude_def Lt ).
assert (Lt A F A F) by (conclude lemma_lessthancongruence2).
assert (¬ Lt A F A F) by (conclude lemma_trichotomy2).
contradict.
}
assert (¬ BetS A F E).
{
intro.
assert (BetS E F A) by (conclude axiom_betweennesssymmetry).
assert (nCol A D C) by (forward_using lemma_parallelNC).
assert (Col A D E) by (forward_using lemma_collinearorder).
assert (nCol A E C) by (conclude lemma_NChelper).
assert (nCol C A E) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:∃ r, (BetS C r F ∧ BetS E r Q)) by (conclude postulate_Pasch_inner);destruct Tf as [r];spliter.
assert (BetS Q r E) by (conclude axiom_betweennesssymmetry).
assert (nCol E B F) by (forward_using lemma_parallelNC).
assert (nCol F B E) by (forward_using lemma_NCorder).
rename_H H;let Tf:=fresh in
assert (Tf:∃ H, (BetS E H B ∧ BetS F r H)) by (conclude postulate_Pasch_outer);destruct Tf as [H];spliter.
assert (Col E H B) by (conclude_def Col ).
assert (Col F r H) by (conclude_def Col ).
assert (Col E B H) by (forward_using lemma_collinearorder).
assert (Col C r F) by (conclude_def Col ).
assert (Col r F C) by (forward_using lemma_collinearorder).
assert (Col r F H) by (forward_using lemma_collinearorder).
assert (neq r F) by (forward_using lemma_betweennotequal).
assert (Col F C H) by (conclude lemma_collinear4).
assert (neq B E) by (forward_using lemma_NCdistinct).
assert (neq E B) by (conclude lemma_inequalitysymmetric).
assert (neq F C) by (conclude_def Par ).
assert (Meet E B F C) by (conclude_def Meet ).
assert (¬ Meet E B F C) by (conclude_def Par ).
contradict.
}
assert (Col A F E) by (forward_using lemma_collinearorder).
assert ((eq A F ∨ eq A E ∨ eq F E ∨ BetS F A E ∨ BetS A F E ∨ BetS A E F)) by (conclude_def Col ).
assert (BetS A E F).
by cases on (eq A F ∨ eq A E ∨ eq F E ∨ BetS F A E ∨ BetS A F E ∨ BetS A E F).
{
assert (¬ ¬ BetS A E F).
{
intro.
assert (BetS A D A) by (conclude cn_equalitysub).
assert (¬ BetS A D A) by (conclude axiom_betweennessidentity).
contradict.
}
close.
}
{
assert (¬ ¬ BetS A E F).
{
intro.
contradict.
}
close.
}
{
assert (¬ ¬ BetS A E F).
{
intro.
assert (eq E F) by (conclude lemma_equalitysymmetric).
assert (Col B E F) by (conclude_def Col ).
assert (Col E B F) by (forward_using lemma_collinearorder).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (Col F C F) by (conclude_def Col ).
assert (neq E B) by (conclude_def Par ).
assert (neq F C) by (conclude_def Par ).
assert (Meet E B F C) by (conclude_def Meet ).
assert (¬ Meet E B F C) by (conclude_def Par ).
contradict.
}
close.
}
{
assert (¬ ¬ BetS A E F).
{
intro.
assert (BetS F D A) by (conclude axiom_betweennesssymmetry).
assert (BetS D A E) by (conclude lemma_3_6a).
assert (Cong D A D A) by (conclude cn_congruencereflexive).
assert (Lt D A D E) by (conclude_def Lt ).
assert (Cong D A A D) by (conclude cn_equalityreverse).
assert (Lt A D D E) by (conclude lemma_lessthancongruence2).
assert (Cong D E E D) by (conclude cn_equalityreverse).
assert (Lt A D E D) by (conclude lemma_lessthancongruence).
assert (Cong A D A D) by (conclude cn_congruencereflexive).
assert (Lt A D A F) by (conclude_def Lt ).
assert (Cong A D D A) by (conclude cn_equalityreverse).
assert (Lt D A A F) by (conclude lemma_lessthancongruence2).
assert (Cong A F F A) by (conclude cn_equalityreverse).
assert (Lt D A F A) by (conclude lemma_lessthancongruence).
assert (Cong F A F A) by (conclude cn_congruencereflexive).
assert (Lt F A F E) by (conclude_def Lt ).
assert (Lt D A F E) by (conclude lemma_lessthantransitive).
assert (Cong D A F E) by (forward_using lemma_congruenceflip).
assert (Lt F E F E) by (conclude lemma_lessthancongruence2).
assert (¬ Lt F E F E) by (conclude lemma_trichotomy2).
contradict.
}
close.
}
{
assert (¬ ¬ BetS A E F).
{
intro.
contradict.
}
close.
}
{
close.
}
close.
Qed.
End Euclid.