# Library GeoCoq.Elements.OriginalProofs.proposition_16

Require Export GeoCoq.Elements.OriginalProofs.proposition_10.

Require Export GeoCoq.Elements.OriginalProofs.proposition_15.

Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglesreflexive.

Require Export GeoCoq.Elements.OriginalProofs.lemma_angleorderrespectscongruence.

Require Export GeoCoq.Elements.OriginalProofs.lemma_angleorderrespectscongruence2.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_16 :

∀ A B C D,

Triangle A B C → BetS B C D →

LtA B A C A C D ∧ LtA C B A A C D.

Proof.

intros.

assert (nCol A B C) by (conclude_def Triangle ).

assert (nCol A B C) by (conclude_def Triangle ).

assert (¬ eq A C).

{

intro.

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

contradict.

}

assert (¬ eq B C).

{

intro.

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

contradict.

}

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

let Tf:=fresh in

assert (Tf:∃ E, (BetS A E C ∧ Cong E A E C)) by (conclude proposition_10);destruct Tf as [E];spliter.

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

assert (¬ eq B E).

{

intro.

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

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

contradict.

}

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

let Tf:=fresh in

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

assert (¬ eq A C).

{

intro.

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

contradict.

}

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

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

let Tf:=fresh in

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

assert (¬ Col B E A).

{

intro.

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

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

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

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

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

assert (Col A B C) by (conclude lemma_collinear4).

contradict.

}

assert (CongA B E A C E F) by (conclude proposition_15a).

assert (¬ Col A E B).

{

intro.

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

contradict.

}

assert (CongA A E B B E A) by (conclude lemma_ABCequalsCBA).

assert (CongA A E B C E F) by (conclude lemma_equalanglestransitive).

assert (Cong B E F E) by (forward_using lemma_doublereverse).

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

assert (¬ Col E A B).

{

intro.

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

contradict.

}

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

assert (¬ Col C E F).

{

intro.

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

assert (Col F E C) by (forward_using lemma_collinearorder).

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

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

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

assert (Col E C B) by (conclude lemma_collinear4).

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

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

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

assert (Col C B A) by (conclude lemma_collinear4).

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

contradict.

}

assert (Triangle C E F) by (conclude_def Triangle ).

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

assert ((Cong A B C F ∧ CongA E A B E C F ∧ CongA E B A E F C)) by (conclude proposition_04).

assert (¬ Col B A E).

{

intro.

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

contradict.

}

assert (CongA B A E E A B) by (conclude lemma_ABCequalsCBA).

assert (Cong A B A B) by (conclude cn_congruencereflexive).

assert (Out A C E) by (conclude lemma_ray4).

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

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

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

assert (Out A B B) by (conclude lemma_ray4).

assert (¬ Col B A C).

{

intro.

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

contradict.

}

assert (CongA B A C B A C) by (conclude lemma_equalanglesreflexive).

assert (CongA B A C B A E) by (conclude lemma_equalangleshelper).

assert (CongA B A E E A B) by (conclude lemma_ABCequalsCBA).

assert (CongA B A C E A B) by (conclude lemma_equalanglestransitive).

assert (CongA B A C E C F) by (conclude lemma_equalanglestransitive).

assert (BetS C E A) by (conclude axiom_betweennesssymmetry).

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

assert (Out C E A) by (conclude lemma_ray4).

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

assert (¬ Col E C F).

{

intro.

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

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

assert (Col F E C) by (forward_using lemma_collinearorder).

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

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

assert (Col E B C) by (conclude lemma_collinear4).

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

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

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

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

assert (Col C B A) by (conclude lemma_collinear4).

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

contradict.

}

assert (¬ eq C F).

{

intro.

assert (Col E C F) by (conclude_def Col ).

contradict.

}

assert (Out C F F) by (conclude lemma_ray4).

assert (CongA E C F E C F) by (conclude lemma_equalanglesreflexive).

assert (CongA E C F A C F) by (conclude lemma_equalangleshelper).

assert (CongA B A C A C F) by (conclude lemma_equalanglestransitive).

assert (BetS D C B) by (conclude axiom_betweennesssymmetry).

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

assert (¬ Col D B F).

{

intro.

assert (Col F B D) by (forward_using lemma_collinearorder).

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

assert (Col F B E) 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 D E) by (conclude lemma_collinear4).

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

assert (Col B C D) by (conclude_def Col ).

assert (Col D B C) by (forward_using lemma_collinearorder).

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

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

assert (Col B E C) by (conclude lemma_collinear4).

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

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

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

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

assert (Col C B A) by (conclude lemma_collinear4).

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

contradict.

}

rename_H H;

let Tf:=fresh in

assert (Tf:∃ H, (BetS D H E ∧ BetS F H C)) by (conclude postulate_Pasch_inner);destruct Tf as [H];spliter.

assert (BetS C H F) by (conclude axiom_betweennesssymmetry).

assert (Out C F H) by (conclude lemma_ray4).

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

assert (Out C A A) by (conclude lemma_ray4).

assert (CongA B A C A C H) by (conclude lemma_equalangleshelper).

assert (CongA B A C A C F) by (conclude lemma_equalangleshelper).

assert (BetS E H D) by (conclude axiom_betweennesssymmetry).

assert (Out C A E) by (conclude lemma_ray5).

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

assert (neq D C) by (forward_using lemma_betweennotequal).

assert (neq C D) by (conclude lemma_inequalitysymmetric).

assert (Out C D D) by (conclude lemma_ray4).

assert (CongA B A C A C H) by (conclude lemma_equalanglestransitive).

assert (LtA B A C A C D) by (conclude_def LtA ).

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

let Tf:=fresh in

assert (Tf:∃ e, (BetS B e C ∧ Cong e B e C)) by (conclude proposition_10);destruct Tf as [e];spliter.

assert (Col B e C) by (conclude_def Col ).

assert (¬ eq A e).

{

intro.

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

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

contradict.

}

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

let Tf:=fresh in

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

assert (¬ eq B C).

{

intro.

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

contradict.

}

assert (neq e C) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

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

assert (¬ Col A e B).

{

intro.

assert (Col B e C) by (conclude_def Col ).

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

assert (Col e B C) by (forward_using lemma_collinearorder).

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

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

assert (Col B A C) by (conclude lemma_collinear4).

contradict.

}

assert (CongA A e B C e f) by (conclude proposition_15a).

assert (¬ Col B e A).

{

intro.

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

contradict.

}

assert (CongA B e A A e B) by (conclude lemma_ABCequalsCBA).

assert (CongA B e A C e f) by (conclude lemma_equalanglestransitive).

assert (Cong A e f e) by (forward_using lemma_doublereverse).

assert (Cong e A e f) by (forward_using lemma_congruenceflip).

assert (¬ Col e B A).

{

intro.

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

contradict.

}

assert (Triangle e B A) by (conclude_def Triangle ).

assert (¬ Col C e f).

{

intro.

assert (Col A e f) by (conclude_def Col ).

assert (Col f e C) by (forward_using lemma_collinearorder).

assert (Col f e A) by (forward_using lemma_collinearorder).

assert (neq e f) by (forward_using lemma_betweennotequal).

assert (neq f e) by (conclude lemma_inequalitysymmetric).

assert (Col e C A) by (conclude lemma_collinear4).

assert (Col B e C) by (conclude_def Col ).

assert (Col e C B) by (forward_using lemma_collinearorder).

assert (neq e C) by (forward_using lemma_betweennotequal).

assert (Col C A B) by (conclude lemma_collinear4).

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

contradict.

}

assert (Triangle C e f) by (conclude_def Triangle ).

assert (Triangle B e A) by (conclude_def Triangle ).

assert ((Cong B A C f ∧ CongA e B A e C f ∧ CongA e A B e f C)) by (conclude proposition_04).

assert (¬ Col A B e).

{

intro.

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

contradict.

}

assert (CongA A B e e B A) by (conclude lemma_ABCequalsCBA).

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (Out B C e) by (conclude lemma_ray4).

assert (Out B A A) by (conclude lemma_ray4).

assert (¬ Col A B C).

{

intro.

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

contradict.

}

assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).

assert (CongA A B C A B e) by (conclude lemma_equalangleshelper).

assert (CongA A B e e B A) by (conclude lemma_ABCequalsCBA).

assert (CongA A B C e B A) by (conclude lemma_equalanglestransitive).

assert (CongA A B C e C f) by (conclude lemma_equalanglestransitive).

assert (BetS C e B) by (conclude axiom_betweennesssymmetry).

assert (neq C e) by (forward_using lemma_betweennotequal).

assert (Out C e B) by (conclude lemma_ray4).

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

assert (nCol e C f) by (conclude lemma_equalanglesNC).

assert (¬ eq C f).

{

intro.

assert (Col e C f) by (conclude_def Col ).

contradict.

}

assert (Out C f f) by (conclude lemma_ray4).

assert (¬ Col e C f).

{

intro.

assert (Col A e f) by (conclude_def Col ).

assert (Col f e A) by (forward_using lemma_collinearorder).

assert (Col f e C) by (forward_using lemma_collinearorder).

assert (neq e f) by (forward_using lemma_betweennotequal).

assert (neq f e) by (conclude lemma_inequalitysymmetric).

assert (Col e A C) by (conclude lemma_collinear4).

assert (Col e B C) by (conclude_def Col ).

assert (Col e C A) by (forward_using lemma_collinearorder).

assert (Col e C B) by (forward_using lemma_collinearorder).

assert (neq e C) by (forward_using lemma_betweennotequal).

assert (Col C A B) by (conclude lemma_collinear4).

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

contradict.

}

assert (CongA e C f e C f) by (conclude lemma_equalanglesreflexive).

assert (CongA e C f B C f) by (conclude lemma_equalangleshelper).

assert (CongA A B C B C f) by (conclude lemma_equalanglestransitive).

assert (BetS G C A) by (conclude axiom_betweennesssymmetry).

assert (neq G C) by (forward_using lemma_betweennotequal).

assert (neq C G) by (conclude lemma_inequalitysymmetric).

assert (BetS f e A) by (conclude axiom_betweennesssymmetry).

assert (¬ Col G A f).

{

intro.

assert (Col f A G) by (forward_using lemma_collinearorder).

assert (Col A e f) by (conclude_def Col ).

assert (Col f A e) by (forward_using lemma_collinearorder).

assert (neq A f) by (forward_using lemma_betweennotequal).

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

assert (Col A G e) by (conclude lemma_collinear4).

assert (Col G A e) by (forward_using lemma_collinearorder).

assert (Col A C G) by (conclude_def Col ).

assert (Col G A C) by (forward_using lemma_collinearorder).

assert (neq A G) by (forward_using lemma_betweennotequal).

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

assert (Col A e C) by (conclude lemma_collinear4).

assert (Col e C A) by (forward_using lemma_collinearorder).

assert (Col B e C) by (conclude_def Col ).

assert (Col e C B) by (forward_using lemma_collinearorder).

assert (neq e C) by (forward_using lemma_betweennotequal).

assert (Col C A B) by (conclude lemma_collinear4).

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ h, (BetS G h e ∧ BetS f h C)) by (conclude postulate_Pasch_inner);destruct Tf as [h];spliter.

assert (BetS C h f) by (conclude axiom_betweennesssymmetry).

assert (neq h C) by (forward_using lemma_betweennotequal).

assert (neq C h) by (conclude lemma_inequalitysymmetric).

assert (Out C h f) by (conclude lemma_ray4).

assert (Out C f h) by (conclude lemma_ray5).

assert (Out C B B) by (conclude lemma_ray4).

assert (CongA A B C B C h) by (conclude lemma_equalangleshelper).

assert (CongA A B C B C f) by (conclude lemma_equalangleshelper).

assert (BetS e h G) by (conclude axiom_betweennesssymmetry).

assert (BetS C e B) by (conclude axiom_betweennesssymmetry).

assert (Out C e B) by (conclude lemma_ray4).

assert (Out C B e) by (conclude lemma_ray5).

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

assert (Out C G G) by (conclude lemma_ray4).

assert (CongA A B C B C h) by (conclude lemma_equalanglestransitive).

assert (LtA A B C B C G) by (conclude_def LtA ).

assert (¬ Col G C B).

{

intro.

assert (Col A C G) by (conclude_def Col ).

assert (Col G C A) by (forward_using lemma_collinearorder).

assert (neq C G) by (forward_using lemma_betweennotequal).

assert (neq G C) by (conclude lemma_inequalitysymmetric).

assert (Col C B A) by (conclude lemma_collinear4).

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

contradict.

}

assert (CongA G C B D C A) by (conclude proposition_15a).

assert (¬ Col A C D).

{

intro.

assert (Col D C A) by (forward_using lemma_collinearorder).

assert (Col B C D) by (conclude_def Col ).

assert (Col D C B) by (forward_using lemma_collinearorder).

assert (neq C D) by (forward_using lemma_betweennotequal).

assert (neq D C) by (conclude lemma_inequalitysymmetric).

assert (Col C A B) by (conclude lemma_collinear4).

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

contradict.

}

assert (¬ Col B C G).

{

intro.

assert (Col G C B) by (forward_using lemma_collinearorder).

contradict.

}

assert (CongA G C B B C G) by (conclude lemma_ABCequalsCBA).

assert (LtA A B C G C B) by (conclude lemma_angleorderrespectscongruence).

assert (CongA A C D D C A) by (conclude lemma_ABCequalsCBA).

assert (¬ Col D C A).

{

intro.

assert (Col A C D) by (forward_using lemma_collinearorder).

contradict.

}

assert (CongA D C A A C D) by (conclude lemma_ABCequalsCBA).

assert (CongA G C B A C D) by (conclude lemma_equalanglestransitive).

assert (CongA A C D G C B) by (conclude lemma_equalanglessymmetric).

assert (LtA A B C A C D) by (conclude lemma_angleorderrespectscongruence).

assert (¬ Col C B A).

{

intro.

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

contradict.

}

assert (CongA C B A A B C) by (conclude lemma_ABCequalsCBA).

assert (LtA C B A A C D) by (conclude lemma_angleorderrespectscongruence2).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.proposition_15.

Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglesreflexive.

Require Export GeoCoq.Elements.OriginalProofs.lemma_angleorderrespectscongruence.

Require Export GeoCoq.Elements.OriginalProofs.lemma_angleorderrespectscongruence2.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_16 :

∀ A B C D,

Triangle A B C → BetS B C D →

LtA B A C A C D ∧ LtA C B A A C D.

Proof.

intros.

assert (nCol A B C) by (conclude_def Triangle ).

assert (nCol A B C) by (conclude_def Triangle ).

assert (¬ eq A C).

{

intro.

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

contradict.

}

assert (¬ eq B C).

{

intro.

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

contradict.

}

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

let Tf:=fresh in

assert (Tf:∃ E, (BetS A E C ∧ Cong E A E C)) by (conclude proposition_10);destruct Tf as [E];spliter.

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

assert (¬ eq B E).

{

intro.

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

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

contradict.

}

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

let Tf:=fresh in

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

assert (¬ eq A C).

{

intro.

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

contradict.

}

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

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

let Tf:=fresh in

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

assert (¬ Col B E A).

{

intro.

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

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

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

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

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

assert (Col A B C) by (conclude lemma_collinear4).

contradict.

}

assert (CongA B E A C E F) by (conclude proposition_15a).

assert (¬ Col A E B).

{

intro.

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

contradict.

}

assert (CongA A E B B E A) by (conclude lemma_ABCequalsCBA).

assert (CongA A E B C E F) by (conclude lemma_equalanglestransitive).

assert (Cong B E F E) by (forward_using lemma_doublereverse).

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

assert (¬ Col E A B).

{

intro.

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

contradict.

}

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

assert (¬ Col C E F).

{

intro.

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

assert (Col F E C) by (forward_using lemma_collinearorder).

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

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

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

assert (Col E C B) by (conclude lemma_collinear4).

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

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

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

assert (Col C B A) by (conclude lemma_collinear4).

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

contradict.

}

assert (Triangle C E F) by (conclude_def Triangle ).

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

assert ((Cong A B C F ∧ CongA E A B E C F ∧ CongA E B A E F C)) by (conclude proposition_04).

assert (¬ Col B A E).

{

intro.

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

contradict.

}

assert (CongA B A E E A B) by (conclude lemma_ABCequalsCBA).

assert (Cong A B A B) by (conclude cn_congruencereflexive).

assert (Out A C E) by (conclude lemma_ray4).

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

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

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

assert (Out A B B) by (conclude lemma_ray4).

assert (¬ Col B A C).

{

intro.

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

contradict.

}

assert (CongA B A C B A C) by (conclude lemma_equalanglesreflexive).

assert (CongA B A C B A E) by (conclude lemma_equalangleshelper).

assert (CongA B A E E A B) by (conclude lemma_ABCequalsCBA).

assert (CongA B A C E A B) by (conclude lemma_equalanglestransitive).

assert (CongA B A C E C F) by (conclude lemma_equalanglestransitive).

assert (BetS C E A) by (conclude axiom_betweennesssymmetry).

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

assert (Out C E A) by (conclude lemma_ray4).

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

assert (¬ Col E C F).

{

intro.

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

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

assert (Col F E C) by (forward_using lemma_collinearorder).

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

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

assert (Col E B C) by (conclude lemma_collinear4).

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

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

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

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

assert (Col C B A) by (conclude lemma_collinear4).

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

contradict.

}

assert (¬ eq C F).

{

intro.

assert (Col E C F) by (conclude_def Col ).

contradict.

}

assert (Out C F F) by (conclude lemma_ray4).

assert (CongA E C F E C F) by (conclude lemma_equalanglesreflexive).

assert (CongA E C F A C F) by (conclude lemma_equalangleshelper).

assert (CongA B A C A C F) by (conclude lemma_equalanglestransitive).

assert (BetS D C B) by (conclude axiom_betweennesssymmetry).

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

assert (¬ Col D B F).

{

intro.

assert (Col F B D) by (forward_using lemma_collinearorder).

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

assert (Col F B E) 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 D E) by (conclude lemma_collinear4).

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

assert (Col B C D) by (conclude_def Col ).

assert (Col D B C) by (forward_using lemma_collinearorder).

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

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

assert (Col B E C) by (conclude lemma_collinear4).

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

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

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

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

assert (Col C B A) by (conclude lemma_collinear4).

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

contradict.

}

rename_H H;

let Tf:=fresh in

assert (Tf:∃ H, (BetS D H E ∧ BetS F H C)) by (conclude postulate_Pasch_inner);destruct Tf as [H];spliter.

assert (BetS C H F) by (conclude axiom_betweennesssymmetry).

assert (Out C F H) by (conclude lemma_ray4).

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

assert (Out C A A) by (conclude lemma_ray4).

assert (CongA B A C A C H) by (conclude lemma_equalangleshelper).

assert (CongA B A C A C F) by (conclude lemma_equalangleshelper).

assert (BetS E H D) by (conclude axiom_betweennesssymmetry).

assert (Out C A E) by (conclude lemma_ray5).

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

assert (neq D C) by (forward_using lemma_betweennotequal).

assert (neq C D) by (conclude lemma_inequalitysymmetric).

assert (Out C D D) by (conclude lemma_ray4).

assert (CongA B A C A C H) by (conclude lemma_equalanglestransitive).

assert (LtA B A C A C D) by (conclude_def LtA ).

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

let Tf:=fresh in

assert (Tf:∃ e, (BetS B e C ∧ Cong e B e C)) by (conclude proposition_10);destruct Tf as [e];spliter.

assert (Col B e C) by (conclude_def Col ).

assert (¬ eq A e).

{

intro.

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

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

contradict.

}

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

let Tf:=fresh in

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

assert (¬ eq B C).

{

intro.

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

contradict.

}

assert (neq e C) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

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

assert (¬ Col A e B).

{

intro.

assert (Col B e C) by (conclude_def Col ).

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

assert (Col e B C) by (forward_using lemma_collinearorder).

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

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

assert (Col B A C) by (conclude lemma_collinear4).

contradict.

}

assert (CongA A e B C e f) by (conclude proposition_15a).

assert (¬ Col B e A).

{

intro.

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

contradict.

}

assert (CongA B e A A e B) by (conclude lemma_ABCequalsCBA).

assert (CongA B e A C e f) by (conclude lemma_equalanglestransitive).

assert (Cong A e f e) by (forward_using lemma_doublereverse).

assert (Cong e A e f) by (forward_using lemma_congruenceflip).

assert (¬ Col e B A).

{

intro.

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

contradict.

}

assert (Triangle e B A) by (conclude_def Triangle ).

assert (¬ Col C e f).

{

intro.

assert (Col A e f) by (conclude_def Col ).

assert (Col f e C) by (forward_using lemma_collinearorder).

assert (Col f e A) by (forward_using lemma_collinearorder).

assert (neq e f) by (forward_using lemma_betweennotequal).

assert (neq f e) by (conclude lemma_inequalitysymmetric).

assert (Col e C A) by (conclude lemma_collinear4).

assert (Col B e C) by (conclude_def Col ).

assert (Col e C B) by (forward_using lemma_collinearorder).

assert (neq e C) by (forward_using lemma_betweennotequal).

assert (Col C A B) by (conclude lemma_collinear4).

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

contradict.

}

assert (Triangle C e f) by (conclude_def Triangle ).

assert (Triangle B e A) by (conclude_def Triangle ).

assert ((Cong B A C f ∧ CongA e B A e C f ∧ CongA e A B e f C)) by (conclude proposition_04).

assert (¬ Col A B e).

{

intro.

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

contradict.

}

assert (CongA A B e e B A) by (conclude lemma_ABCequalsCBA).

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (Out B C e) by (conclude lemma_ray4).

assert (Out B A A) by (conclude lemma_ray4).

assert (¬ Col A B C).

{

intro.

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

contradict.

}

assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).

assert (CongA A B C A B e) by (conclude lemma_equalangleshelper).

assert (CongA A B e e B A) by (conclude lemma_ABCequalsCBA).

assert (CongA A B C e B A) by (conclude lemma_equalanglestransitive).

assert (CongA A B C e C f) by (conclude lemma_equalanglestransitive).

assert (BetS C e B) by (conclude axiom_betweennesssymmetry).

assert (neq C e) by (forward_using lemma_betweennotequal).

assert (Out C e B) by (conclude lemma_ray4).

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

assert (nCol e C f) by (conclude lemma_equalanglesNC).

assert (¬ eq C f).

{

intro.

assert (Col e C f) by (conclude_def Col ).

contradict.

}

assert (Out C f f) by (conclude lemma_ray4).

assert (¬ Col e C f).

{

intro.

assert (Col A e f) by (conclude_def Col ).

assert (Col f e A) by (forward_using lemma_collinearorder).

assert (Col f e C) by (forward_using lemma_collinearorder).

assert (neq e f) by (forward_using lemma_betweennotequal).

assert (neq f e) by (conclude lemma_inequalitysymmetric).

assert (Col e A C) by (conclude lemma_collinear4).

assert (Col e B C) by (conclude_def Col ).

assert (Col e C A) by (forward_using lemma_collinearorder).

assert (Col e C B) by (forward_using lemma_collinearorder).

assert (neq e C) by (forward_using lemma_betweennotequal).

assert (Col C A B) by (conclude lemma_collinear4).

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

contradict.

}

assert (CongA e C f e C f) by (conclude lemma_equalanglesreflexive).

assert (CongA e C f B C f) by (conclude lemma_equalangleshelper).

assert (CongA A B C B C f) by (conclude lemma_equalanglestransitive).

assert (BetS G C A) by (conclude axiom_betweennesssymmetry).

assert (neq G C) by (forward_using lemma_betweennotequal).

assert (neq C G) by (conclude lemma_inequalitysymmetric).

assert (BetS f e A) by (conclude axiom_betweennesssymmetry).

assert (¬ Col G A f).

{

intro.

assert (Col f A G) by (forward_using lemma_collinearorder).

assert (Col A e f) by (conclude_def Col ).

assert (Col f A e) by (forward_using lemma_collinearorder).

assert (neq A f) by (forward_using lemma_betweennotequal).

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

assert (Col A G e) by (conclude lemma_collinear4).

assert (Col G A e) by (forward_using lemma_collinearorder).

assert (Col A C G) by (conclude_def Col ).

assert (Col G A C) by (forward_using lemma_collinearorder).

assert (neq A G) by (forward_using lemma_betweennotequal).

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

assert (Col A e C) by (conclude lemma_collinear4).

assert (Col e C A) by (forward_using lemma_collinearorder).

assert (Col B e C) by (conclude_def Col ).

assert (Col e C B) by (forward_using lemma_collinearorder).

assert (neq e C) by (forward_using lemma_betweennotequal).

assert (Col C A B) by (conclude lemma_collinear4).

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ h, (BetS G h e ∧ BetS f h C)) by (conclude postulate_Pasch_inner);destruct Tf as [h];spliter.

assert (BetS C h f) by (conclude axiom_betweennesssymmetry).

assert (neq h C) by (forward_using lemma_betweennotequal).

assert (neq C h) by (conclude lemma_inequalitysymmetric).

assert (Out C h f) by (conclude lemma_ray4).

assert (Out C f h) by (conclude lemma_ray5).

assert (Out C B B) by (conclude lemma_ray4).

assert (CongA A B C B C h) by (conclude lemma_equalangleshelper).

assert (CongA A B C B C f) by (conclude lemma_equalangleshelper).

assert (BetS e h G) by (conclude axiom_betweennesssymmetry).

assert (BetS C e B) by (conclude axiom_betweennesssymmetry).

assert (Out C e B) by (conclude lemma_ray4).

assert (Out C B e) by (conclude lemma_ray5).

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

assert (Out C G G) by (conclude lemma_ray4).

assert (CongA A B C B C h) by (conclude lemma_equalanglestransitive).

assert (LtA A B C B C G) by (conclude_def LtA ).

assert (¬ Col G C B).

{

intro.

assert (Col A C G) by (conclude_def Col ).

assert (Col G C A) by (forward_using lemma_collinearorder).

assert (neq C G) by (forward_using lemma_betweennotequal).

assert (neq G C) by (conclude lemma_inequalitysymmetric).

assert (Col C B A) by (conclude lemma_collinear4).

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

contradict.

}

assert (CongA G C B D C A) by (conclude proposition_15a).

assert (¬ Col A C D).

{

intro.

assert (Col D C A) by (forward_using lemma_collinearorder).

assert (Col B C D) by (conclude_def Col ).

assert (Col D C B) by (forward_using lemma_collinearorder).

assert (neq C D) by (forward_using lemma_betweennotequal).

assert (neq D C) by (conclude lemma_inequalitysymmetric).

assert (Col C A B) by (conclude lemma_collinear4).

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

contradict.

}

assert (¬ Col B C G).

{

intro.

assert (Col G C B) by (forward_using lemma_collinearorder).

contradict.

}

assert (CongA G C B B C G) by (conclude lemma_ABCequalsCBA).

assert (LtA A B C G C B) by (conclude lemma_angleorderrespectscongruence).

assert (CongA A C D D C A) by (conclude lemma_ABCequalsCBA).

assert (¬ Col D C A).

{

intro.

assert (Col A C D) by (forward_using lemma_collinearorder).

contradict.

}

assert (CongA D C A A C D) by (conclude lemma_ABCequalsCBA).

assert (CongA G C B A C D) by (conclude lemma_equalanglestransitive).

assert (CongA A C D G C B) by (conclude lemma_equalanglessymmetric).

assert (LtA A B C A C D) by (conclude lemma_angleorderrespectscongruence).

assert (¬ Col C B A).

{

intro.

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

contradict.

}

assert (CongA C B A A B C) by (conclude lemma_ABCequalsCBA).

assert (LtA C B A A C D) by (conclude lemma_angleorderrespectscongruence2).

close.

Qed.

End Euclid.