Library GeoCoq.Elements.OriginalProofs.lemma_supplements

Require Export GeoCoq.Elements.OriginalProofs.lemma_raystrict.
Require Export GeoCoq.Elements.OriginalProofs.lemma_congruenceflip.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ray1.
Require Export GeoCoq.Elements.OriginalProofs.lemma_rayimpliescollinear.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ray3.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_supplements :
   ∀ A B C D F a b c d f,
   CongA A B C a b c → Supp A B C D F → Supp a b c d f →
   CongA D B F d b f.
Proof.
intros.
assert (BetS A B F) by (conclude_def Supp ).
assert (Out B C D) by (conclude_def Supp ).
assert (BetS a b f) by (conclude_def Supp ).
assert (Out b c d) by (conclude_def Supp ).
let Tf:=fresh in
assert (Tf:∃ U V u v, (Out B A U ∧ Out B C V ∧ Out b a u ∧ Out b c v ∧ Cong B U b u ∧ Cong B V b v ∧ Cong U V u v ∧ nCol A B C)) by (conclude_def CongA );destruct Tf as [U[V[u[v]]]];spliter.
assert (neq A B) by (forward_using lemma_betweennotequal).
assert (neq B U) by (conclude lemma_raystrict).
assert (neq U B) by (conclude lemma_inequalitysymmetric).
assert (neq b u) by (conclude lemma_raystrict).
assert (neq u b) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ W, (BetS U B W ∧ Cong B W U B)) by (conclude postulate_extension);destruct Tf as [W];spliter.
assert (neq a b) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:∃ w, (BetS u b w ∧ Cong b w U B)) by (conclude postulate_extension);destruct Tf as [w];spliter.
assert (Cong U B b w) by (conclude lemma_congruencesymmetric).
assert (Cong B W b w) by (conclude lemma_congruencetransitive).
assert (Cong U B u b) by (forward_using lemma_congruenceflip).
assert (Cong V W v w) by (conclude axiom_5_line).
assert ((BetS B U A ∨ eq A U ∨ BetS B A U)) by (conclude lemma_ray1).
assert (BetS A B W).
by cases on (BetS B U A ∨ eq A U ∨ BetS B A U).
{
 assert (BetS A U B) by (conclude axiom_betweennesssymmetry).
 assert (BetS A B W) by (conclude lemma_3_7a).
 close.
 }
{
 assert (BetS A B W) by (conclude cn_equalitysub).
 close.
 }
{
 assert (BetS U A B) by (conclude axiom_betweennesssymmetry).
 assert (BetS A B W) by (conclude lemma_3_6a).
 close.
 }

assert (Out B F W) by (conclude_def Out ).
assert ((BetS B W F ∨ eq F W ∨ BetS B F W)) by (conclude lemma_ray1).
assert (BetS U B F).
by cases on (BetS B W F ∨ eq F W ∨ BetS B F W).
{
 assert (BetS U B F) by (conclude lemma_3_7b).
 close.
 }
{
 assert (BetS U B F) by (conclude cn_equalitysub).
 close.
 }
{
 assert (BetS U B F) by (conclude axiom_innertransitivity).
 close.
 }

assert (neq B F) by (forward_using lemma_betweennotequal).
assert (Out B F W) by (conclude_def Out ).
assert ((BetS b u a ∨ eq a u ∨ BetS b a u)) by (conclude lemma_ray1).
assert (BetS a b w).
by cases on (BetS b u a ∨ eq a u ∨ BetS b a u).
{
 assert (BetS a u b) by (conclude axiom_betweennesssymmetry).
 assert (BetS a b w) by (conclude lemma_3_7a).
 close.
 }
{
 assert (BetS a b w) by (conclude cn_equalitysub).
 close.
 }
{
 assert (BetS u a b) by (conclude axiom_betweennesssymmetry).
 assert (BetS a b w) by (conclude lemma_3_6a).
 close.
 }

assert (Out b f w) by (conclude_def Out ).
assert ((BetS b w f ∨ eq f w ∨ BetS b f w)) by (conclude lemma_ray1).
assert (BetS u b f).
by cases on (BetS b w f ∨ eq f w ∨ BetS b f w).
{
 assert (BetS u b f) by (conclude lemma_3_7b).
 close.
 }
{
 assert (BetS u b f) by (conclude cn_equalitysub).
 close.
 }
{
 assert (BetS u b f) by (conclude axiom_innertransitivity).
 close.
 }

assert (neq b f) by (forward_using lemma_betweennotequal).
assert (Out b f w) by (conclude_def Out ).
assert (neq b f) by (forward_using lemma_betweennotequal).
assert (Out b f w) by (conclude_def Out ).
assert (Col U B W) by (conclude_def Col ).
assert (Col B A U) by (conclude lemma_rayimpliescollinear).
assert (¬ Col D B F).
 {
 intro.
 assert (Col B C D) by (conclude lemma_rayimpliescollinear).
 assert (Col D B C) by (forward_using lemma_collinearorder).
 assert (neq B D) by (conclude lemma_raystrict).
 assert (neq D B) by (conclude lemma_inequalitysymmetric).
 assert (Col B F C) by (conclude lemma_collinear4).
 assert (Col A B F) by (conclude_def Col ).
 assert (Col F B A) by (forward_using lemma_collinearorder).
 assert (Col F B C) by (forward_using lemma_collinearorder).
 assert (neq B F) by (forward_using lemma_betweennotequal).
 assert (neq F B) by (conclude lemma_inequalitysymmetric).
 assert (Col B A C) by (conclude lemma_collinear4).
 assert (Col A B C) by (forward_using lemma_collinearorder).
 contradict.
 }
assert (Out B D V) by (conclude lemma_ray3).
assert (Out b d v) by (conclude lemma_ray3).
assert (CongA D B F d b f) by (conclude_def CongA ).
close.
Qed.

End Euclid.