Library GeoCoq.Elements.OriginalProofs.proposition_04
Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglesNC.
Require Export GeoCoq.Elements.OriginalProofs.lemma_layoffunique.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ray5.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ray3.
Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma proposition_04 :
∀ A B C a b c,
Cong A B a b → Cong A C a c → CongA B A C b a c →
Cong B C b c ∧ CongA A B C a b c ∧ CongA A C B a c b.
Proof.
intros.
assert (nCol b a c) by (conclude lemma_equalanglesNC).
let Tf:=fresh in
assert (Tf:∃ U V u v, (Out A B U ∧ Out A C V ∧ Out a b u ∧ Out a c v ∧ Cong A U a u ∧ Cong A V a v ∧ Cong U V u v ∧ nCol B A C)) by (conclude_def CongA );destruct Tf as [U[V[u[v]]]];spliter.
assert (neq a b) by (conclude lemma_ray2).
assert (neq b a) by (conclude lemma_inequalitysymmetric).
assert (¬ Col A B C).
{
intro.
assert (Col B A C) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ eq A B).
{
intro.
assert (Col A B C) by (conclude_def Col ).
assert (Col B A C) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ eq A C).
{
intro.
assert (Col A B C) by (conclude_def Col ).
assert (Col B A C) by (forward_using lemma_collinearorder).
contradict.
}
assert (neq C A) by (conclude lemma_inequalitysymmetric).
assert (¬ eq a c).
{
intro.
assert (Col b a c) by (conclude_def Col ).
contradict.
}
assert (neq c a) by (conclude lemma_inequalitysymmetric).
assert (¬ eq b c).
{
intro.
assert (Col b a c) by (conclude_def Col ).
contradict.
}
assert (neq c b) by (conclude lemma_inequalitysymmetric).
assert (¬ eq B C).
{
intro.
assert (Col A B C) by (conclude_def Col ).
assert (Col B A C) by (forward_using lemma_collinearorder).
contradict.
}
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert ((BetS A U B ∨ eq B U ∨ BetS A B U)) by (conclude lemma_ray1).
assert (Cong B V b v).
by cases on (BetS A U B ∨ eq B U ∨ BetS A B U).
{
assert (Cong A U A U) by (conclude cn_congruencereflexive).
assert (Lt A U A B) by (conclude_def Lt ).
assert (Lt A U a b) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ w, (BetS a w b ∧ Cong a w A U)) by (conclude_def Lt );destruct Tf as [w];spliter.
assert (Cong a w a u) by (conclude lemma_congruencetransitive).
assert (neq a b) by (forward_using lemma_betweennotequal).
assert (Out a b w) by (conclude lemma_ray4).
assert (Cong a w a u) by (conclude lemma_congruencetransitive).
assert (eq w u) by (conclude lemma_layoffunique).
assert (BetS a u b) by (conclude cn_equalitysub).
assert (Cong U B u b) by (conclude lemma_differenceofparts).
assert (Cong V B v b) by (conclude axiom_5_line).
assert (Cong B V b v) by (forward_using lemma_congruenceflip).
close.
}
{
assert (Cong B V u v) by (conclude cn_equalitysub).
assert (Cong a b A B) by (conclude lemma_congruencesymmetric).
assert (Cong A B A B) by (conclude cn_congruencereflexive).
assert (Cong A B A U) by (conclude cn_equalitysub).
assert (Cong a b A U) by (conclude lemma_congruencetransitive).
assert (Cong a b a u) by (conclude lemma_congruencetransitive).
assert ((BetS a u b ∨ eq b u ∨ BetS a b u)) by (conclude lemma_ray1).
assert (eq b u).
by cases on (BetS a u b ∨ eq b u ∨ BetS a b u).
{
assert (¬ neq b u).
{
intro.
assert (¬ Cong a u a b) by (conclude lemma_partnotequalwhole).
assert (Cong a u a b) by (conclude lemma_congruencesymmetric).
contradict.
}
close.
}
{
close.
}
{
assert (¬ neq b u).
{
intro.
assert (¬ Cong a b a u) by (conclude lemma_partnotequalwhole).
assert (Cong a b A B) by (conclude lemma_congruencesymmetric).
assert (Cong A B A B) by (conclude cn_congruencereflexive).
assert (Cong A B A U) by (conclude cn_equalitysub).
assert (Cong A B a u) by (conclude lemma_congruencetransitive).
assert (Cong a b a u) by (conclude lemma_congruencetransitive).
contradict.
}
close.
}
assert (Cong B V b v) by (conclude cn_equalitysub).
close.
}
{
assert (Cong A B A B) by (conclude cn_congruencereflexive).
assert (Lt A B A U) by (conclude_def Lt ).
assert (Lt A B a u) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ f, (BetS a f u ∧ Cong a f A B)) by (conclude_def Lt );destruct Tf as [f];spliter.
assert (neq a u) by (forward_using lemma_betweennotequal).
assert (Out a u f) by (conclude lemma_ray4).
assert (Out a u b) by (conclude lemma_ray5).
assert (Out a b f) by (conclude lemma_ray3).
assert (Cong a f a b) by (conclude lemma_congruencetransitive).
assert (eq f b) by (conclude lemma_layoffunique).
assert (BetS a b u) by (conclude cn_equalitysub).
assert (Cong B U b u) by (conclude lemma_differenceofparts).
assert (BetS a b u) by (conclude lemma_betweennesspreserved).
assert (Cong B U b u) by (conclude lemma_differenceofparts).
assert (Cong B V b v) by (conclude lemma_interior5).
close.
}
assert ((BetS A V C ∨ eq C V ∨ BetS A C V)) by (conclude lemma_ray1).
assert (Cong B C b c).
by cases on (BetS A V C ∨ eq C V ∨ BetS A C V).
{
assert (Cong A V A V) by (conclude cn_congruencereflexive).
assert (Lt A V A C) by (conclude_def Lt ).
assert (Lt A V a c) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ g, (BetS a g c ∧ Cong a g A V)) by (conclude_def Lt );destruct Tf as [g];spliter.
assert (neq a g) by (forward_using lemma_betweennotequal).
assert (Out a g c) by (conclude lemma_ray4).
assert (Out a c g) by (conclude lemma_ray5).
assert (Cong a g a v) by (conclude lemma_congruencetransitive).
assert (eq g v) by (conclude lemma_layoffunique).
assert (BetS a v c) by (conclude cn_equalitysub).
assert (Cong V C v c) by (conclude lemma_differenceofparts).
assert (Cong V B v b) by (forward_using lemma_congruenceflip).
assert (Cong B C b c) by (conclude axiom_5_line).
close.
}
{
assert (Cong A C a v) by (conclude cn_equalitysub).
assert (Cong a c A C) by (conclude lemma_congruencesymmetric).
assert (Cong a c a v) by (conclude lemma_congruencetransitive).
assert (neq a c) by (conclude lemma_ray2).
assert (eq c c) by (conclude cn_equalityreflexive).
assert (Out a c c) by (conclude lemma_ray4).
assert (eq c v) by (conclude lemma_layoffunique).
assert (Cong B C b v) by (conclude cn_equalitysub).
assert (Cong B C b c) by (conclude cn_equalitysub).
close.
}
{
assert (Cong A C A C) by (conclude cn_congruencereflexive).
assert (Lt A C A V) by (conclude_def Lt ).
assert (Lt A C a v) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ g, (BetS a g v ∧ Cong a g A C)) by (conclude_def Lt );destruct Tf as [g];spliter.
assert (neq a g) by (forward_using lemma_betweennotequal).
assert (Out a g v) by (conclude lemma_ray4).
assert (Out a v g) by (conclude lemma_ray5).
assert (Cong a g a c) by (conclude lemma_congruencetransitive).
assert (Cong a c a g) by (conclude lemma_congruencesymmetric).
assert (Out a v c) by (conclude lemma_ray5).
assert (eq c g) by (conclude lemma_layoffunique).
assert (BetS a c v) by (conclude cn_equalitysub).
assert (Cong C V c v) by (conclude lemma_differenceofparts).
assert (Cong V B v b) by (forward_using lemma_congruenceflip).
assert (Cong C B c b) by (conclude lemma_interior5).
assert (Cong B C b c) by (forward_using lemma_congruenceflip).
close.
}
assert (eq A A) by (conclude cn_equalityreflexive).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (eq a a) by (conclude cn_equalityreflexive).
assert (eq c c) by (conclude cn_equalityreflexive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (eq b b) by (conclude cn_equalityreflexive).
assert (neq B A) by (conclude lemma_inequalitysymmetric).
assert (Out B A A) by (conclude lemma_ray4).
assert (Out B C C) by (conclude lemma_ray4).
assert (Out b a a) by (conclude lemma_ray4).
assert (Out b c c) by (conclude lemma_ray4).
assert (Cong B A b a) by (forward_using lemma_congruenceflip).
assert (CongA A B C a b c) by (conclude_def CongA ).
assert (Out C A A) by (conclude lemma_ray4).
assert (Out C B B) by (conclude lemma_ray4).
assert (Out c a a) by (conclude lemma_ray4).
assert (Out c b b) by (conclude lemma_ray4).
assert (Cong C A c a) by (forward_using lemma_congruenceflip).
assert (Cong C B c b) by (forward_using lemma_congruenceflip).
assert (¬ Col A C B).
{
intro.
assert (Col A B C) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA A C B a c b) by (conclude_def CongA ).
close.
Qed.
End Euclid.
Require Export GeoCoq.Elements.OriginalProofs.lemma_layoffunique.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ray5.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ray3.
Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma proposition_04 :
∀ A B C a b c,
Cong A B a b → Cong A C a c → CongA B A C b a c →
Cong B C b c ∧ CongA A B C a b c ∧ CongA A C B a c b.
Proof.
intros.
assert (nCol b a c) by (conclude lemma_equalanglesNC).
let Tf:=fresh in
assert (Tf:∃ U V u v, (Out A B U ∧ Out A C V ∧ Out a b u ∧ Out a c v ∧ Cong A U a u ∧ Cong A V a v ∧ Cong U V u v ∧ nCol B A C)) by (conclude_def CongA );destruct Tf as [U[V[u[v]]]];spliter.
assert (neq a b) by (conclude lemma_ray2).
assert (neq b a) by (conclude lemma_inequalitysymmetric).
assert (¬ Col A B C).
{
intro.
assert (Col B A C) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ eq A B).
{
intro.
assert (Col A B C) by (conclude_def Col ).
assert (Col B A C) by (forward_using lemma_collinearorder).
contradict.
}
assert (¬ eq A C).
{
intro.
assert (Col A B C) by (conclude_def Col ).
assert (Col B A C) by (forward_using lemma_collinearorder).
contradict.
}
assert (neq C A) by (conclude lemma_inequalitysymmetric).
assert (¬ eq a c).
{
intro.
assert (Col b a c) by (conclude_def Col ).
contradict.
}
assert (neq c a) by (conclude lemma_inequalitysymmetric).
assert (¬ eq b c).
{
intro.
assert (Col b a c) by (conclude_def Col ).
contradict.
}
assert (neq c b) by (conclude lemma_inequalitysymmetric).
assert (¬ eq B C).
{
intro.
assert (Col A B C) by (conclude_def Col ).
assert (Col B A C) by (forward_using lemma_collinearorder).
contradict.
}
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert ((BetS A U B ∨ eq B U ∨ BetS A B U)) by (conclude lemma_ray1).
assert (Cong B V b v).
by cases on (BetS A U B ∨ eq B U ∨ BetS A B U).
{
assert (Cong A U A U) by (conclude cn_congruencereflexive).
assert (Lt A U A B) by (conclude_def Lt ).
assert (Lt A U a b) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ w, (BetS a w b ∧ Cong a w A U)) by (conclude_def Lt );destruct Tf as [w];spliter.
assert (Cong a w a u) by (conclude lemma_congruencetransitive).
assert (neq a b) by (forward_using lemma_betweennotequal).
assert (Out a b w) by (conclude lemma_ray4).
assert (Cong a w a u) by (conclude lemma_congruencetransitive).
assert (eq w u) by (conclude lemma_layoffunique).
assert (BetS a u b) by (conclude cn_equalitysub).
assert (Cong U B u b) by (conclude lemma_differenceofparts).
assert (Cong V B v b) by (conclude axiom_5_line).
assert (Cong B V b v) by (forward_using lemma_congruenceflip).
close.
}
{
assert (Cong B V u v) by (conclude cn_equalitysub).
assert (Cong a b A B) by (conclude lemma_congruencesymmetric).
assert (Cong A B A B) by (conclude cn_congruencereflexive).
assert (Cong A B A U) by (conclude cn_equalitysub).
assert (Cong a b A U) by (conclude lemma_congruencetransitive).
assert (Cong a b a u) by (conclude lemma_congruencetransitive).
assert ((BetS a u b ∨ eq b u ∨ BetS a b u)) by (conclude lemma_ray1).
assert (eq b u).
by cases on (BetS a u b ∨ eq b u ∨ BetS a b u).
{
assert (¬ neq b u).
{
intro.
assert (¬ Cong a u a b) by (conclude lemma_partnotequalwhole).
assert (Cong a u a b) by (conclude lemma_congruencesymmetric).
contradict.
}
close.
}
{
close.
}
{
assert (¬ neq b u).
{
intro.
assert (¬ Cong a b a u) by (conclude lemma_partnotequalwhole).
assert (Cong a b A B) by (conclude lemma_congruencesymmetric).
assert (Cong A B A B) by (conclude cn_congruencereflexive).
assert (Cong A B A U) by (conclude cn_equalitysub).
assert (Cong A B a u) by (conclude lemma_congruencetransitive).
assert (Cong a b a u) by (conclude lemma_congruencetransitive).
contradict.
}
close.
}
assert (Cong B V b v) by (conclude cn_equalitysub).
close.
}
{
assert (Cong A B A B) by (conclude cn_congruencereflexive).
assert (Lt A B A U) by (conclude_def Lt ).
assert (Lt A B a u) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ f, (BetS a f u ∧ Cong a f A B)) by (conclude_def Lt );destruct Tf as [f];spliter.
assert (neq a u) by (forward_using lemma_betweennotequal).
assert (Out a u f) by (conclude lemma_ray4).
assert (Out a u b) by (conclude lemma_ray5).
assert (Out a b f) by (conclude lemma_ray3).
assert (Cong a f a b) by (conclude lemma_congruencetransitive).
assert (eq f b) by (conclude lemma_layoffunique).
assert (BetS a b u) by (conclude cn_equalitysub).
assert (Cong B U b u) by (conclude lemma_differenceofparts).
assert (BetS a b u) by (conclude lemma_betweennesspreserved).
assert (Cong B U b u) by (conclude lemma_differenceofparts).
assert (Cong B V b v) by (conclude lemma_interior5).
close.
}
assert ((BetS A V C ∨ eq C V ∨ BetS A C V)) by (conclude lemma_ray1).
assert (Cong B C b c).
by cases on (BetS A V C ∨ eq C V ∨ BetS A C V).
{
assert (Cong A V A V) by (conclude cn_congruencereflexive).
assert (Lt A V A C) by (conclude_def Lt ).
assert (Lt A V a c) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ g, (BetS a g c ∧ Cong a g A V)) by (conclude_def Lt );destruct Tf as [g];spliter.
assert (neq a g) by (forward_using lemma_betweennotequal).
assert (Out a g c) by (conclude lemma_ray4).
assert (Out a c g) by (conclude lemma_ray5).
assert (Cong a g a v) by (conclude lemma_congruencetransitive).
assert (eq g v) by (conclude lemma_layoffunique).
assert (BetS a v c) by (conclude cn_equalitysub).
assert (Cong V C v c) by (conclude lemma_differenceofparts).
assert (Cong V B v b) by (forward_using lemma_congruenceflip).
assert (Cong B C b c) by (conclude axiom_5_line).
close.
}
{
assert (Cong A C a v) by (conclude cn_equalitysub).
assert (Cong a c A C) by (conclude lemma_congruencesymmetric).
assert (Cong a c a v) by (conclude lemma_congruencetransitive).
assert (neq a c) by (conclude lemma_ray2).
assert (eq c c) by (conclude cn_equalityreflexive).
assert (Out a c c) by (conclude lemma_ray4).
assert (eq c v) by (conclude lemma_layoffunique).
assert (Cong B C b v) by (conclude cn_equalitysub).
assert (Cong B C b c) by (conclude cn_equalitysub).
close.
}
{
assert (Cong A C A C) by (conclude cn_congruencereflexive).
assert (Lt A C A V) by (conclude_def Lt ).
assert (Lt A C a v) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:∃ g, (BetS a g v ∧ Cong a g A C)) by (conclude_def Lt );destruct Tf as [g];spliter.
assert (neq a g) by (forward_using lemma_betweennotequal).
assert (Out a g v) by (conclude lemma_ray4).
assert (Out a v g) by (conclude lemma_ray5).
assert (Cong a g a c) by (conclude lemma_congruencetransitive).
assert (Cong a c a g) by (conclude lemma_congruencesymmetric).
assert (Out a v c) by (conclude lemma_ray5).
assert (eq c g) by (conclude lemma_layoffunique).
assert (BetS a c v) by (conclude cn_equalitysub).
assert (Cong C V c v) by (conclude lemma_differenceofparts).
assert (Cong V B v b) by (forward_using lemma_congruenceflip).
assert (Cong C B c b) by (conclude lemma_interior5).
assert (Cong B C b c) by (forward_using lemma_congruenceflip).
close.
}
assert (eq A A) by (conclude cn_equalityreflexive).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (eq a a) by (conclude cn_equalityreflexive).
assert (eq c c) by (conclude cn_equalityreflexive).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (eq b b) by (conclude cn_equalityreflexive).
assert (neq B A) by (conclude lemma_inequalitysymmetric).
assert (Out B A A) by (conclude lemma_ray4).
assert (Out B C C) by (conclude lemma_ray4).
assert (Out b a a) by (conclude lemma_ray4).
assert (Out b c c) by (conclude lemma_ray4).
assert (Cong B A b a) by (forward_using lemma_congruenceflip).
assert (CongA A B C a b c) by (conclude_def CongA ).
assert (Out C A A) by (conclude lemma_ray4).
assert (Out C B B) by (conclude lemma_ray4).
assert (Out c a a) by (conclude lemma_ray4).
assert (Out c b b) by (conclude lemma_ray4).
assert (Cong C A c a) by (forward_using lemma_congruenceflip).
assert (Cong C B c b) by (forward_using lemma_congruenceflip).
assert (¬ Col A C B).
{
intro.
assert (Col A B C) by (forward_using lemma_collinearorder).
contradict.
}
assert (CongA A C B a c b) by (conclude_def CongA ).
close.
Qed.
End Euclid.