Library GeoCoq.Elements.OriginalProofs.proposition_14
Require Export GeoCoq.Elements.OriginalProofs.lemma_NCdistinct.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NChelper.
Require Export GeoCoq.Elements.OriginalProofs.lemma_oppositesidesymmetric.
Require Export GeoCoq.Elements.OriginalProofs.proposition_07.
Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma proposition_14 :
∀ A B C D E,
RT A B C D B E → Out B C D → TS E D B A →
Supp A B C D E ∧ BetS A B E.
Proof.
intros.
let Tf:=fresh in
assert (Tf:∃ a b c d e, (Supp a b c d e ∧ CongA A B C a b c ∧ CongA D B E d b e)) by (conclude_def RT );destruct Tf as [a[b[c[d[e]]]]];spliter.
assert (CongA a b c A B C) by (conclude lemma_equalanglessymmetric).
assert (CongA d b e D B E) by (conclude lemma_equalanglessymmetric).
assert (nCol A B C) by (conclude lemma_equalanglesNC).
assert (neq A B) by (forward_using lemma_NCdistinct).
assert (neq B A) by (conclude lemma_inequalitysymmetric).
assert (nCol D B E) by (conclude lemma_equalanglesNC).
assert (neq B E) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:∃ T, (BetS A B T ∧ Cong B T B E)) by (conclude postulate_extension);destruct Tf as [T];spliter.
assert (Cong B D B D) by (conclude cn_congruencereflexive).
assert (Supp A B C D T) by (conclude_def Supp ).
assert (CongA a b c A B C) by (conclude lemma_equalanglessymmetric).
assert (CongA d b e D B E) by (conclude lemma_equalanglessymmetric).
assert (CongA d b e D B T) by (conclude lemma_supplements).
assert (CongA D B E D B T) by (conclude lemma_equalanglestransitive).
assert (CongA D B T D B E) by (conclude lemma_equalanglessymmetric).
assert (Col A B T) by (conclude_def Col ).
assert (neq B T) by (forward_using lemma_betweennotequal).
assert (neq T B) by (conclude lemma_inequalitysymmetric).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col A B B) by (conclude_def Col ).
assert (nCol T B C) by (conclude lemma_NChelper).
assert (nCol C B T) by (forward_using lemma_NCorder).
assert (Col B C D) by (conclude lemma_rayimpliescollinear).
assert (Col C B D) by (forward_using lemma_collinearorder).
assert (neq D B) by (forward_using lemma_NCdistinct).
assert (Col C B B) by (conclude_def Col ).
assert (nCol D B T) by (conclude lemma_NChelper).
assert (Triangle D B T) by (conclude_def Triangle ).
assert (Triangle D B E) by (conclude_def Triangle ).
assert (Cong D T D E) by (conclude proposition_04).
assert (Cong T D E D) by (forward_using lemma_congruenceflip).
assert (Cong T B E B) by (forward_using lemma_congruenceflip).
assert (Col D B B) by (conclude_def Col ).
assert (TS A D B E) by (conclude lemma_oppositesidesymmetric).
let Tf:=fresh in
assert (Tf:∃ m, (BetS A m E ∧ Col D B m ∧ nCol D B A)) by (conclude_def TS );destruct Tf as [m];spliter.
assert (BetS E m A) by (conclude axiom_betweennesssymmetry).
assert (BetS T B A) by (conclude axiom_betweennesssymmetry).
assert (OS T E D B) by (conclude_def OS ).
assert (neq B C) by (forward_using lemma_NCdistinct).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert (eq T E) by (conclude proposition_07).
assert (BetS A B E) by (conclude cn_equalitysub).
assert (Supp A B C D E) by (conclude_def Supp ).
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NChelper.
Require Export GeoCoq.Elements.OriginalProofs.lemma_oppositesidesymmetric.
Require Export GeoCoq.Elements.OriginalProofs.proposition_07.
Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma proposition_14 :
∀ A B C D E,
RT A B C D B E → Out B C D → TS E D B A →
Supp A B C D E ∧ BetS A B E.
Proof.
intros.
let Tf:=fresh in
assert (Tf:∃ a b c d e, (Supp a b c d e ∧ CongA A B C a b c ∧ CongA D B E d b e)) by (conclude_def RT );destruct Tf as [a[b[c[d[e]]]]];spliter.
assert (CongA a b c A B C) by (conclude lemma_equalanglessymmetric).
assert (CongA d b e D B E) by (conclude lemma_equalanglessymmetric).
assert (nCol A B C) by (conclude lemma_equalanglesNC).
assert (neq A B) by (forward_using lemma_NCdistinct).
assert (neq B A) by (conclude lemma_inequalitysymmetric).
assert (nCol D B E) by (conclude lemma_equalanglesNC).
assert (neq B E) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:∃ T, (BetS A B T ∧ Cong B T B E)) by (conclude postulate_extension);destruct Tf as [T];spliter.
assert (Cong B D B D) by (conclude cn_congruencereflexive).
assert (Supp A B C D T) by (conclude_def Supp ).
assert (CongA a b c A B C) by (conclude lemma_equalanglessymmetric).
assert (CongA d b e D B E) by (conclude lemma_equalanglessymmetric).
assert (CongA d b e D B T) by (conclude lemma_supplements).
assert (CongA D B E D B T) by (conclude lemma_equalanglestransitive).
assert (CongA D B T D B E) by (conclude lemma_equalanglessymmetric).
assert (Col A B T) by (conclude_def Col ).
assert (neq B T) by (forward_using lemma_betweennotequal).
assert (neq T B) by (conclude lemma_inequalitysymmetric).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col A B B) by (conclude_def Col ).
assert (nCol T B C) by (conclude lemma_NChelper).
assert (nCol C B T) by (forward_using lemma_NCorder).
assert (Col B C D) by (conclude lemma_rayimpliescollinear).
assert (Col C B D) by (forward_using lemma_collinearorder).
assert (neq D B) by (forward_using lemma_NCdistinct).
assert (Col C B B) by (conclude_def Col ).
assert (nCol D B T) by (conclude lemma_NChelper).
assert (Triangle D B T) by (conclude_def Triangle ).
assert (Triangle D B E) by (conclude_def Triangle ).
assert (Cong D T D E) by (conclude proposition_04).
assert (Cong T D E D) by (forward_using lemma_congruenceflip).
assert (Cong T B E B) by (forward_using lemma_congruenceflip).
assert (Col D B B) by (conclude_def Col ).
assert (TS A D B E) by (conclude lemma_oppositesidesymmetric).
let Tf:=fresh in
assert (Tf:∃ m, (BetS A m E ∧ Col D B m ∧ nCol D B A)) by (conclude_def TS );destruct Tf as [m];spliter.
assert (BetS E m A) by (conclude axiom_betweennesssymmetry).
assert (BetS T B A) by (conclude axiom_betweennesssymmetry).
assert (OS T E D B) by (conclude_def OS ).
assert (neq B C) by (forward_using lemma_NCdistinct).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert (eq T E) by (conclude proposition_07).
assert (BetS A B E) by (conclude cn_equalitysub).
assert (Supp A B C D E) by (conclude_def Supp ).
close.
Qed.
End Euclid.