# Library GeoCoq.Elements.OriginalProofs.proposition_44

Require Export GeoCoq.Elements.OriginalProofs.proposition_42B.

Require Export GeoCoq.Elements.OriginalProofs.proposition_44A.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_44 :

∀ A B D J N R a b c,

Triangle a b c → nCol J D N → nCol A B R →

∃ X Y Z, PG A B X Y ∧ CongA A B X J D N ∧ EF a b Z c A B X Y ∧ Midpoint b Z c ∧ TS X A B R.

Proof.

intros.

assert (neq A B) by (forward_using lemma_NCdistinct).

assert (nCol a b c) by (conclude_def Triangle ).

assert (neq b c) by (forward_using lemma_NCdistinct).

let Tf:=fresh in

assert (Tf:∃ m, (BetS b m c ∧ Cong m b m c)) by (conclude proposition_10);destruct Tf as [m];spliter.

assert (Cong b m m c) by (forward_using lemma_congruenceflip).

assert (Midpoint b m c) by (conclude_def Midpoint ).

assert (neq m c) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

assert (Tf:∃ E, (BetS A B E ∧ Cong B E m c)) by (conclude postulate_extension);destruct Tf as [E];spliter.

assert (neq B E) by (forward_using lemma_betweennotequal).

assert (Col A B E) by (conclude_def Col ).

assert (Col B A E) by (forward_using lemma_collinearorder).

assert (eq B B) by (conclude cn_equalityreflexive).

assert (Col B A B) by (conclude_def Col ).

assert (nCol B A R) by (forward_using lemma_NCorder).

assert (nCol B E R) by (conclude lemma_NChelper).

let Tf:=fresh in

assert (Tf:∃ g e, (Out B E e ∧ CongA g B e J D N ∧ OS g R B E)) by (conclude proposition_23C);destruct Tf as [g[e]];spliter.

assert ((BetS B e E ∨ eq E e ∨ BetS B E e)) by (conclude lemma_ray1).

assert (BetS A B e).

by cases on (BetS B e E ∨ eq E e ∨ BetS B E e).

{

assert (BetS A B e) by (conclude axiom_innertransitivity).

close.

}

{

assert (BetS A B e) by (conclude cn_equalitysub).

close.

}

{

assert (BetS A B e) by (conclude lemma_3_7b).

close.

}

assert (neq B A) by (conclude lemma_inequalitysymmetric).

let Tf:=fresh in

assert (Tf:∃ P, (BetS B A P ∧ Cong A P B A)) by (conclude postulate_extension);destruct Tf as [P];spliter.

assert (BetS P A B) by (conclude axiom_betweennesssymmetry).

assert (Cong P A A B) by (forward_using lemma_congruenceflip).

assert (Midpoint P A B) by (conclude_def Midpoint ).

assert (neq B E) by (forward_using lemma_betweennotequal).

assert (neq E B) by (conclude lemma_inequalitysymmetric).

assert (neq b m) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

assert (Tf:∃ Q, (BetS E B Q ∧ Cong B Q b m)) by (conclude postulate_extension);destruct Tf as [Q];spliter.

assert (Cong b m m c) by (forward_using lemma_congruenceflip).

assert (Cong B Q m c) by (conclude lemma_congruencetransitive).

assert (Cong m c B E) by (conclude lemma_congruencesymmetric).

assert (Cong B Q B E) by (conclude lemma_congruencetransitive).

assert (BetS Q B E) by (conclude axiom_betweennesssymmetry).

assert (Cong Q B B E) by (forward_using lemma_congruenceflip).

assert (Midpoint Q B E) by (conclude_def Midpoint ).

assert (Cong E B m c) by (forward_using lemma_congruenceflip).

assert (nCol B A R) by (forward_using lemma_NCorder).

assert (eq A A) by (conclude cn_equalityreflexive).

assert (Col B A A) by (conclude_def Col ).

assert (Col A B E) by (conclude_def Col ).

assert (Col B A E) by (forward_using lemma_collinearorder).

assert (neq B E) by (forward_using lemma_betweennotequal).

assert (neq E B) by (conclude lemma_inequalitysymmetric).

assert (nCol B E R) by (conclude lemma_NChelper).

assert (nCol R B E) by (forward_using lemma_NCorder).

let Tf:=fresh in

assert (Tf:∃ G F, (PG G B E F ∧ EF a b m c G B E F ∧ CongA E B G J D N ∧ OS R G B E)) by (conclude proposition_42B);destruct Tf as [G[F]];spliter.

assert (PG B E F G) by (conclude lemma_PGrotate).

let Tf:=fresh in

assert (Tf:∃ M L, (PG A B M L ∧ CongA A B M J D N ∧ EF B E F G L M B A ∧ BetS G B M)) by (conclude proposition_44A);destruct Tf as [M[L]];spliter.

assert (eq B B) by (conclude cn_equalityreflexive).

assert (Col A B B) by (conclude_def Col ).

assert (Par G B E F) by (conclude_def PG ).

assert (nCol G B E) by (forward_using lemma_parallelNC).

assert (nCol E B G) by (forward_using lemma_NCorder).

assert (Col A B E) by (conclude_def Col ).

assert (Col E B A) by (forward_using lemma_collinearorder).

assert (eq B B) by (conclude cn_equalityreflexive).

assert (Col E B B) by (conclude_def Col ).

assert (nCol A B G) by (conclude lemma_NChelper).

assert (TS G A B M) by (conclude_def TS ).

assert (EF a b m c B E F G) by (forward_using axiom_EFpermutation).

assert (EF a b m c L M B A) by (conclude axiom_EFtransitive).

assert (Par A B M L) by (conclude_def PG ).

assert (EF a b m c A B M L) by (forward_using axiom_EFpermutation).

assert (Col B E A) by (forward_using lemma_collinearorder).

assert (OS R G B A) by (conclude lemma_samesidecollinear).

assert (OS R G A B) by (conclude lemma_samesideflip).

assert (OS G R A B) by (forward_using lemma_samesidesymmetric).

assert (TS R A B M) by (conclude lemma_planeseparation).

assert (TS M A B R) by (conclude lemma_oppositesidesymmetric).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.proposition_44A.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_44 :

∀ A B D J N R a b c,

Triangle a b c → nCol J D N → nCol A B R →

∃ X Y Z, PG A B X Y ∧ CongA A B X J D N ∧ EF a b Z c A B X Y ∧ Midpoint b Z c ∧ TS X A B R.

Proof.

intros.

assert (neq A B) by (forward_using lemma_NCdistinct).

assert (nCol a b c) by (conclude_def Triangle ).

assert (neq b c) by (forward_using lemma_NCdistinct).

let Tf:=fresh in

assert (Tf:∃ m, (BetS b m c ∧ Cong m b m c)) by (conclude proposition_10);destruct Tf as [m];spliter.

assert (Cong b m m c) by (forward_using lemma_congruenceflip).

assert (Midpoint b m c) by (conclude_def Midpoint ).

assert (neq m c) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

assert (Tf:∃ E, (BetS A B E ∧ Cong B E m c)) by (conclude postulate_extension);destruct Tf as [E];spliter.

assert (neq B E) by (forward_using lemma_betweennotequal).

assert (Col A B E) by (conclude_def Col ).

assert (Col B A E) by (forward_using lemma_collinearorder).

assert (eq B B) by (conclude cn_equalityreflexive).

assert (Col B A B) by (conclude_def Col ).

assert (nCol B A R) by (forward_using lemma_NCorder).

assert (nCol B E R) by (conclude lemma_NChelper).

let Tf:=fresh in

assert (Tf:∃ g e, (Out B E e ∧ CongA g B e J D N ∧ OS g R B E)) by (conclude proposition_23C);destruct Tf as [g[e]];spliter.

assert ((BetS B e E ∨ eq E e ∨ BetS B E e)) by (conclude lemma_ray1).

assert (BetS A B e).

by cases on (BetS B e E ∨ eq E e ∨ BetS B E e).

{

assert (BetS A B e) by (conclude axiom_innertransitivity).

close.

}

{

assert (BetS A B e) by (conclude cn_equalitysub).

close.

}

{

assert (BetS A B e) by (conclude lemma_3_7b).

close.

}

assert (neq B A) by (conclude lemma_inequalitysymmetric).

let Tf:=fresh in

assert (Tf:∃ P, (BetS B A P ∧ Cong A P B A)) by (conclude postulate_extension);destruct Tf as [P];spliter.

assert (BetS P A B) by (conclude axiom_betweennesssymmetry).

assert (Cong P A A B) by (forward_using lemma_congruenceflip).

assert (Midpoint P A B) by (conclude_def Midpoint ).

assert (neq B E) by (forward_using lemma_betweennotequal).

assert (neq E B) by (conclude lemma_inequalitysymmetric).

assert (neq b m) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

assert (Tf:∃ Q, (BetS E B Q ∧ Cong B Q b m)) by (conclude postulate_extension);destruct Tf as [Q];spliter.

assert (Cong b m m c) by (forward_using lemma_congruenceflip).

assert (Cong B Q m c) by (conclude lemma_congruencetransitive).

assert (Cong m c B E) by (conclude lemma_congruencesymmetric).

assert (Cong B Q B E) by (conclude lemma_congruencetransitive).

assert (BetS Q B E) by (conclude axiom_betweennesssymmetry).

assert (Cong Q B B E) by (forward_using lemma_congruenceflip).

assert (Midpoint Q B E) by (conclude_def Midpoint ).

assert (Cong E B m c) by (forward_using lemma_congruenceflip).

assert (nCol B A R) by (forward_using lemma_NCorder).

assert (eq A A) by (conclude cn_equalityreflexive).

assert (Col B A A) by (conclude_def Col ).

assert (Col A B E) by (conclude_def Col ).

assert (Col B A E) by (forward_using lemma_collinearorder).

assert (neq B E) by (forward_using lemma_betweennotequal).

assert (neq E B) by (conclude lemma_inequalitysymmetric).

assert (nCol B E R) by (conclude lemma_NChelper).

assert (nCol R B E) by (forward_using lemma_NCorder).

let Tf:=fresh in

assert (Tf:∃ G F, (PG G B E F ∧ EF a b m c G B E F ∧ CongA E B G J D N ∧ OS R G B E)) by (conclude proposition_42B);destruct Tf as [G[F]];spliter.

assert (PG B E F G) by (conclude lemma_PGrotate).

let Tf:=fresh in

assert (Tf:∃ M L, (PG A B M L ∧ CongA A B M J D N ∧ EF B E F G L M B A ∧ BetS G B M)) by (conclude proposition_44A);destruct Tf as [M[L]];spliter.

assert (eq B B) by (conclude cn_equalityreflexive).

assert (Col A B B) by (conclude_def Col ).

assert (Par G B E F) by (conclude_def PG ).

assert (nCol G B E) by (forward_using lemma_parallelNC).

assert (nCol E B G) by (forward_using lemma_NCorder).

assert (Col A B E) by (conclude_def Col ).

assert (Col E B A) by (forward_using lemma_collinearorder).

assert (eq B B) by (conclude cn_equalityreflexive).

assert (Col E B B) by (conclude_def Col ).

assert (nCol A B G) by (conclude lemma_NChelper).

assert (TS G A B M) by (conclude_def TS ).

assert (EF a b m c B E F G) by (forward_using axiom_EFpermutation).

assert (EF a b m c L M B A) by (conclude axiom_EFtransitive).

assert (Par A B M L) by (conclude_def PG ).

assert (EF a b m c A B M L) by (forward_using axiom_EFpermutation).

assert (Col B E A) by (forward_using lemma_collinearorder).

assert (OS R G B A) by (conclude lemma_samesidecollinear).

assert (OS R G A B) by (conclude lemma_samesideflip).

assert (OS G R A B) by (forward_using lemma_samesidesymmetric).

assert (TS R A B M) by (conclude lemma_planeseparation).

assert (TS M A B R) by (conclude lemma_oppositesidesymmetric).

close.

Qed.

End Euclid.