Library GeoCoq.Elements.OriginalProofs.lemma_Euclid4
Require Export GeoCoq.Elements.OriginalProofs.proposition_20.
Require Export GeoCoq.Elements.OriginalProofs.lemma_TGflip.
Require Export GeoCoq.Elements.OriginalProofs.lemma_TGsymmetric.
Require Export GeoCoq.Elements.OriginalProofs.proposition_22.
Require Export GeoCoq.Elements.OriginalProofs.lemma_10_12.
Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma lemma_Euclid4 :
∀ A B C a b c,
Per A B C → Per a b c →
CongA A B C a b c.
Proof.
intros.
let Tf:=fresh in
assert (Tf:∃ D, (BetS A B D ∧ Cong A B D B ∧ Cong A C D C ∧ neq B C)) by (conclude_def Per );destruct Tf as [D];spliter.
let Tf:=fresh in
assert (Tf:∃ d, (BetS a b d ∧ Cong a b d b ∧ Cong a c d c ∧ neq b c)) by (conclude_def Per );destruct Tf as [d];spliter.
assert (neq a b) by (forward_using lemma_betweennotequal).
assert (neq b a) by (conclude lemma_inequalitysymmetric).
assert (neq A B) by (forward_using lemma_betweennotequal).
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ p, (Out b a p ∧ Cong b p B A)) by (conclude lemma_layoff);destruct Tf as [p];spliter.
let Tf:=fresh in
assert (Tf:∃ q, (Out b c q ∧ Cong b q B C)) by (conclude lemma_layoff);destruct Tf as [q];spliter.
assert (Per a b q) by (conclude lemma_8_3).
assert (Per q b a) by (conclude lemma_8_2).
assert (Per q b p) by (conclude lemma_8_3).
assert (Per p b q) by (conclude lemma_8_2).
let Tf:=fresh in
assert (Tf:∃ r, (BetS p b r ∧ Cong p b r b ∧ Cong p q r q ∧ neq b q)) by (conclude_def Per );destruct Tf as [r];spliter.
assert (Cong q p q r) by (forward_using lemma_congruenceflip).
assert (nCol p b q) by (conclude lemma_rightangleNC).
assert (¬ Col b q p).
{
intro.
assert (Col p b q) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ Col q p b).
{
intro.
assert (Col p b q) by (forward_using lemma_collinearorder).
contradict.
}
assert (Triangle p b q) by (conclude_def Triangle ).
assert (Triangle b q p) by (conclude_def Triangle ).
assert (Triangle q p b) by (conclude_def Triangle ).
assert (TG b p p q b q) by (conclude proposition_20).
assert (TG q b b p q p) by (conclude proposition_20).
assert (TG p q q b p b) by (conclude proposition_20).
assert (TG b q b p q p) by (forward_using lemma_TGflip).
assert (TG b q b p p q) by (forward_using lemma_TGflip).
assert (TG q b p q p b) by (conclude lemma_TGsymmetric).
assert (TG b q p q p b) by (forward_using lemma_TGflip).
assert (TG b q p q b p) by (forward_using lemma_TGflip).
assert (TG b p p q q b) by (forward_using lemma_TGflip).
let Tf:=fresh in
assert (Tf:∃ E F, (Cong B E b p ∧ Cong B F b q ∧ Cong E F p q ∧ Out B A E ∧ Triangle B E F)) by (conclude proposition_22);destruct Tf as [E[F]];spliter.
assert (BetS D B A) by (conclude axiom_betweennesssymmetry).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Out B A A) by (conclude lemma_ray4).
assert (Cong B E B A) by (conclude lemma_congruencetransitive).
assert (eq E A) by (conclude lemma_layoffunique).
assert (Cong B A b p) by (conclude cn_equalitysub).
assert (Cong A F p q) by (conclude cn_equalitysub).
assert (¬ eq p b).
{
intro.
assert (Col p b q) by (conclude_def Col ).
assert (nCol p b q) by (conclude lemma_rightangleNC).
contradict.
}
assert (Cong r b p b) by (conclude lemma_congruencesymmetric).
assert (Cong b r p b) by (forward_using lemma_congruenceflip).
assert (Cong b p B E) by (conclude lemma_congruencesymmetric).
assert (neq b p) by (conclude lemma_inequalitysymmetric).
assert (Cong B A A B) by (conclude cn_equalityreverse).
assert (Cong p b b r) by (conclude lemma_congruencesymmetric).
assert (Cong p q r q) by (conclude lemma_rightreverse).
assert (Cong p b A B) by (forward_using lemma_doublereverse).
assert (Cong b r p b) by (conclude lemma_congruencesymmetric).
assert (Cong b r A B) by (conclude lemma_congruencetransitive).
assert (Cong A B B D) by (forward_using lemma_congruenceflip).
assert (Cong b r B D) by (conclude lemma_congruencetransitive).
assert (Cong b q B F) by (conclude lemma_congruencesymmetric).
assert (Cong p q A F) by (conclude lemma_congruencesymmetric).
assert (Cong q r F D) by (conclude axiom_5_line).
assert (Cong A F r q) by (conclude lemma_congruencetransitive).
assert (Cong A F q r) by (forward_using lemma_congruenceflip).
assert (Cong A F F D) by (conclude lemma_congruencetransitive).
assert (Cong A F D F) by (forward_using lemma_congruenceflip).
assert (neq b q) by (conclude_def Per ).
assert (Cong q b b q) by (conclude cn_equalityreverse).
assert (Cong q b B F) by (conclude lemma_congruencetransitive).
assert (neq B F) by (conclude lemma_nullsegment3).
assert (Per A B F) by (conclude_def Per ).
assert (Cong b q B F) by (conclude lemma_congruencesymmetric).
assert (Cong B C b q) by (conclude lemma_congruencesymmetric).
assert (Cong B C B F) by (conclude lemma_congruencetransitive).
assert (Cong A C A F) by (conclude lemma_10_12).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Out B F F) by (conclude lemma_ray4).
assert (Out B C C) by (conclude lemma_ray4).
assert (Out B A A) by (conclude lemma_ray4).
assert (Cong B A B A) by (conclude cn_congruencereflexive).
assert (nCol A B C) by (conclude lemma_rightangleNC).
assert (CongA A B C A B F) by (conclude_def CongA ).
assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).
assert (CongA A B C A B F) by (conclude lemma_equalanglestransitive).
assert (eq p p) by (conclude cn_equalityreflexive).
assert (eq q q) by (conclude cn_equalityreflexive).
assert (Out b p p) by (conclude lemma_ray4).
assert (Out b q q) by (conclude lemma_ray4).
assert (Out B F F) by (conclude lemma_ray4).
assert (Out B A A) by (conclude lemma_ray4).
assert (Cong B A b p) by (conclude lemma_congruencesymmetric).
assert (Cong B A p b) by (forward_using lemma_congruenceflip).
assert (nCol A B F) by (conclude lemma_rightangleNC).
assert (CongA A B F p b q) by (conclude_def CongA ).
assert (CongA A B C p b q) by (conclude lemma_equalanglestransitive).
assert (nCol a b c) by (conclude lemma_rightangleNC).
assert (Out b p p) by (conclude lemma_ray4).
assert (Out b q q) by (conclude lemma_ray4).
assert (Cong b p b p) by (conclude cn_congruencereflexive).
assert (Cong b q b q) by (conclude cn_congruencereflexive).
assert (Cong p q p q) by (conclude cn_congruencereflexive).
assert (CongA a b c p b q) by (conclude_def CongA ).
assert (CongA p b q a b c) by (conclude lemma_equalanglessymmetric).
assert (CongA A B C a b c) by (conclude lemma_equalanglestransitive).
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.lemma_TGflip.
Require Export GeoCoq.Elements.OriginalProofs.lemma_TGsymmetric.
Require Export GeoCoq.Elements.OriginalProofs.proposition_22.
Require Export GeoCoq.Elements.OriginalProofs.lemma_10_12.
Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma lemma_Euclid4 :
∀ A B C a b c,
Per A B C → Per a b c →
CongA A B C a b c.
Proof.
intros.
let Tf:=fresh in
assert (Tf:∃ D, (BetS A B D ∧ Cong A B D B ∧ Cong A C D C ∧ neq B C)) by (conclude_def Per );destruct Tf as [D];spliter.
let Tf:=fresh in
assert (Tf:∃ d, (BetS a b d ∧ Cong a b d b ∧ Cong a c d c ∧ neq b c)) by (conclude_def Per );destruct Tf as [d];spliter.
assert (neq a b) by (forward_using lemma_betweennotequal).
assert (neq b a) by (conclude lemma_inequalitysymmetric).
assert (neq A B) by (forward_using lemma_betweennotequal).
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ p, (Out b a p ∧ Cong b p B A)) by (conclude lemma_layoff);destruct Tf as [p];spliter.
let Tf:=fresh in
assert (Tf:∃ q, (Out b c q ∧ Cong b q B C)) by (conclude lemma_layoff);destruct Tf as [q];spliter.
assert (Per a b q) by (conclude lemma_8_3).
assert (Per q b a) by (conclude lemma_8_2).
assert (Per q b p) by (conclude lemma_8_3).
assert (Per p b q) by (conclude lemma_8_2).
let Tf:=fresh in
assert (Tf:∃ r, (BetS p b r ∧ Cong p b r b ∧ Cong p q r q ∧ neq b q)) by (conclude_def Per );destruct Tf as [r];spliter.
assert (Cong q p q r) by (forward_using lemma_congruenceflip).
assert (nCol p b q) by (conclude lemma_rightangleNC).
assert (¬ Col b q p).
{
intro.
assert (Col p b q) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ Col q p b).
{
intro.
assert (Col p b q) by (forward_using lemma_collinearorder).
contradict.
}
assert (Triangle p b q) by (conclude_def Triangle ).
assert (Triangle b q p) by (conclude_def Triangle ).
assert (Triangle q p b) by (conclude_def Triangle ).
assert (TG b p p q b q) by (conclude proposition_20).
assert (TG q b b p q p) by (conclude proposition_20).
assert (TG p q q b p b) by (conclude proposition_20).
assert (TG b q b p q p) by (forward_using lemma_TGflip).
assert (TG b q b p p q) by (forward_using lemma_TGflip).
assert (TG q b p q p b) by (conclude lemma_TGsymmetric).
assert (TG b q p q p b) by (forward_using lemma_TGflip).
assert (TG b q p q b p) by (forward_using lemma_TGflip).
assert (TG b p p q q b) by (forward_using lemma_TGflip).
let Tf:=fresh in
assert (Tf:∃ E F, (Cong B E b p ∧ Cong B F b q ∧ Cong E F p q ∧ Out B A E ∧ Triangle B E F)) by (conclude proposition_22);destruct Tf as [E[F]];spliter.
assert (BetS D B A) by (conclude axiom_betweennesssymmetry).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Out B A A) by (conclude lemma_ray4).
assert (Cong B E B A) by (conclude lemma_congruencetransitive).
assert (eq E A) by (conclude lemma_layoffunique).
assert (Cong B A b p) by (conclude cn_equalitysub).
assert (Cong A F p q) by (conclude cn_equalitysub).
assert (¬ eq p b).
{
intro.
assert (Col p b q) by (conclude_def Col ).
assert (nCol p b q) by (conclude lemma_rightangleNC).
contradict.
}
assert (Cong r b p b) by (conclude lemma_congruencesymmetric).
assert (Cong b r p b) by (forward_using lemma_congruenceflip).
assert (Cong b p B E) by (conclude lemma_congruencesymmetric).
assert (neq b p) by (conclude lemma_inequalitysymmetric).
assert (Cong B A A B) by (conclude cn_equalityreverse).
assert (Cong p b b r) by (conclude lemma_congruencesymmetric).
assert (Cong p q r q) by (conclude lemma_rightreverse).
assert (Cong p b A B) by (forward_using lemma_doublereverse).
assert (Cong b r p b) by (conclude lemma_congruencesymmetric).
assert (Cong b r A B) by (conclude lemma_congruencetransitive).
assert (Cong A B B D) by (forward_using lemma_congruenceflip).
assert (Cong b r B D) by (conclude lemma_congruencetransitive).
assert (Cong b q B F) by (conclude lemma_congruencesymmetric).
assert (Cong p q A F) by (conclude lemma_congruencesymmetric).
assert (Cong q r F D) by (conclude axiom_5_line).
assert (Cong A F r q) by (conclude lemma_congruencetransitive).
assert (Cong A F q r) by (forward_using lemma_congruenceflip).
assert (Cong A F F D) by (conclude lemma_congruencetransitive).
assert (Cong A F D F) by (forward_using lemma_congruenceflip).
assert (neq b q) by (conclude_def Per ).
assert (Cong q b b q) by (conclude cn_equalityreverse).
assert (Cong q b B F) by (conclude lemma_congruencetransitive).
assert (neq B F) by (conclude lemma_nullsegment3).
assert (Per A B F) by (conclude_def Per ).
assert (Cong b q B F) by (conclude lemma_congruencesymmetric).
assert (Cong B C b q) by (conclude lemma_congruencesymmetric).
assert (Cong B C B F) by (conclude lemma_congruencetransitive).
assert (Cong A C A F) by (conclude lemma_10_12).
assert (eq F F) by (conclude cn_equalityreflexive).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Out B F F) by (conclude lemma_ray4).
assert (Out B C C) by (conclude lemma_ray4).
assert (Out B A A) by (conclude lemma_ray4).
assert (Cong B A B A) by (conclude cn_congruencereflexive).
assert (nCol A B C) by (conclude lemma_rightangleNC).
assert (CongA A B C A B F) by (conclude_def CongA ).
assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).
assert (CongA A B C A B F) by (conclude lemma_equalanglestransitive).
assert (eq p p) by (conclude cn_equalityreflexive).
assert (eq q q) by (conclude cn_equalityreflexive).
assert (Out b p p) by (conclude lemma_ray4).
assert (Out b q q) by (conclude lemma_ray4).
assert (Out B F F) by (conclude lemma_ray4).
assert (Out B A A) by (conclude lemma_ray4).
assert (Cong B A b p) by (conclude lemma_congruencesymmetric).
assert (Cong B A p b) by (forward_using lemma_congruenceflip).
assert (nCol A B F) by (conclude lemma_rightangleNC).
assert (CongA A B F p b q) by (conclude_def CongA ).
assert (CongA A B C p b q) by (conclude lemma_equalanglestransitive).
assert (nCol a b c) by (conclude lemma_rightangleNC).
assert (Out b p p) by (conclude lemma_ray4).
assert (Out b q q) by (conclude lemma_ray4).
assert (Cong b p b p) by (conclude cn_congruencereflexive).
assert (Cong b q b q) by (conclude cn_congruencereflexive).
assert (Cong p q p q) by (conclude cn_congruencereflexive).
assert (CongA a b c p b q) by (conclude_def CongA ).
assert (CongA p b q a b c) by (conclude lemma_equalanglessymmetric).
assert (CongA A B C a b c) by (conclude lemma_equalanglestransitive).
close.
Qed.
End Euclid.