# Library GeoCoq.Elements.OriginalProofs.proposition_26A

Require Export GeoCoq.Elements.OriginalProofs.lemma_angletrichotomy.

Require Export GeoCoq.Elements.OriginalProofs.lemma_trichotomy1.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_26A :

∀ A B C D E F,

Triangle A B C → Triangle D E F → CongA A B C D E F → CongA B C A E F D → Cong B C E F →

Cong A B D E ∧ Cong A C D F ∧ CongA B A C E D F.

Proof.

intros.

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

assert (¬ eq A B).

{

intro.

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

contradict.

}

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

assert (¬ eq B C).

{

intro.

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

contradict.

}

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

assert (¬ eq A C).

{

intro.

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

contradict.

}

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

assert (¬ Lt D E A B).

{

intro.

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

assert (Lt D E B A) by (conclude lemma_lessthancongruence).

let Tf:=fresh in

assert (Tf:∃ G, (BetS B G A ∧ Cong B G D E)) by (conclude_def Lt );destruct Tf as [G];spliter.

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

assert (Cong B G E D) by (forward_using lemma_congruenceflip).

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

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

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

assert (Cong G C G C) by (conclude cn_congruencereflexive).

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

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

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

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

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

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

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

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

assert (¬ Col G B C).

{

intro.

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

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

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

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

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

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

contradict.

}

assert (Triangle G B C) by (conclude_def Triangle ).

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

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

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

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

assert (¬ Col B C G).

{

intro.

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

contradict.

}

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

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

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

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

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

assert (¬ LtA B C A B C A) by (conclude lemma_angletrichotomy).

contradict.

}

assert (¬ Lt A B D E).

{

intro.

assert (Cong D E E D) by (conclude cn_equalityreverse).

assert (Lt A B E D) by (conclude lemma_lessthancongruence).

let Tf:=fresh in

assert (Tf:∃ G, (BetS E G D ∧ Cong E G A B)) by (conclude_def Lt );destruct Tf as [G];spliter.

assert (Cong E G B A) by (forward_using lemma_congruenceflip).

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

assert (Out E D G) by (conclude lemma_ray4).

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

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

assert (nCol D E F) by (conclude_def Triangle ).

assert (¬ eq E F).

{

intro.

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

contradict.

}

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

assert (Cong G F G F) by (conclude cn_congruencereflexive).

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

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

assert (neq E G) by (conclude lemma_raystrict).

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

assert (Cong E G E G) by (conclude cn_congruencereflexive).

assert (Cong E F E F) by (conclude cn_congruencereflexive).

assert (CongA D E F G E F) by (conclude_def CongA ).

assert (CongA G E F D E F) by (conclude lemma_equalanglessymmetric).

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

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

assert (¬ Col G E F).

{

intro.

assert (Col E G D) by (conclude_def Col ).

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

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

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

assert (Col E F D) by (conclude lemma_collinear4).

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

contradict.

}

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

assert (Cong E F B C) by (conclude lemma_congruencesymmetric).

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

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

assert (CongA E F G E F D) by (conclude lemma_equalanglestransitive).

assert (CongA E F D E F G) by (conclude lemma_equalanglessymmetric).

assert (¬ Col E F G).

{

intro.

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

contradict.

}

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

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

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

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

assert (neq F D) by (forward_using lemma_angledistinct).

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

assert (LtA E F D E F D) by (conclude_def LtA ).

assert (¬ LtA E F D E F D) by (conclude lemma_angletrichotomy).

contradict.

}

assert (¬ eq D E).

{

intro.

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

assert (nCol D E F) by (conclude_def Triangle ).

contradict.

}

assert (Cong A B D E) by (conclude lemma_trichotomy1).

assert (Cong B A E D) by (forward_using lemma_congruenceflip).

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

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_trichotomy1.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_26A :

∀ A B C D E F,

Triangle A B C → Triangle D E F → CongA A B C D E F → CongA B C A E F D → Cong B C E F →

Cong A B D E ∧ Cong A C D F ∧ CongA B A C E D F.

Proof.

intros.

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

assert (¬ eq A B).

{

intro.

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

contradict.

}

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

assert (¬ eq B C).

{

intro.

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

contradict.

}

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

assert (¬ eq A C).

{

intro.

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

contradict.

}

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

assert (¬ Lt D E A B).

{

intro.

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

assert (Lt D E B A) by (conclude lemma_lessthancongruence).

let Tf:=fresh in

assert (Tf:∃ G, (BetS B G A ∧ Cong B G D E)) by (conclude_def Lt );destruct Tf as [G];spliter.

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

assert (Cong B G E D) by (forward_using lemma_congruenceflip).

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

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

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

assert (Cong G C G C) by (conclude cn_congruencereflexive).

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

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

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

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

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

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

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

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

assert (¬ Col G B C).

{

intro.

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

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

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

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

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

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

contradict.

}

assert (Triangle G B C) by (conclude_def Triangle ).

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

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

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

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

assert (¬ Col B C G).

{

intro.

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

contradict.

}

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

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

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

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

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

assert (¬ LtA B C A B C A) by (conclude lemma_angletrichotomy).

contradict.

}

assert (¬ Lt A B D E).

{

intro.

assert (Cong D E E D) by (conclude cn_equalityreverse).

assert (Lt A B E D) by (conclude lemma_lessthancongruence).

let Tf:=fresh in

assert (Tf:∃ G, (BetS E G D ∧ Cong E G A B)) by (conclude_def Lt );destruct Tf as [G];spliter.

assert (Cong E G B A) by (forward_using lemma_congruenceflip).

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

assert (Out E D G) by (conclude lemma_ray4).

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

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

assert (nCol D E F) by (conclude_def Triangle ).

assert (¬ eq E F).

{

intro.

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

contradict.

}

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

assert (Cong G F G F) by (conclude cn_congruencereflexive).

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

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

assert (neq E G) by (conclude lemma_raystrict).

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

assert (Cong E G E G) by (conclude cn_congruencereflexive).

assert (Cong E F E F) by (conclude cn_congruencereflexive).

assert (CongA D E F G E F) by (conclude_def CongA ).

assert (CongA G E F D E F) by (conclude lemma_equalanglessymmetric).

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

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

assert (¬ Col G E F).

{

intro.

assert (Col E G D) by (conclude_def Col ).

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

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

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

assert (Col E F D) by (conclude lemma_collinear4).

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

contradict.

}

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

assert (Cong E F B C) by (conclude lemma_congruencesymmetric).

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

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

assert (CongA E F G E F D) by (conclude lemma_equalanglestransitive).

assert (CongA E F D E F G) by (conclude lemma_equalanglessymmetric).

assert (¬ Col E F G).

{

intro.

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

contradict.

}

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

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

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

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

assert (neq F D) by (forward_using lemma_angledistinct).

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

assert (LtA E F D E F D) by (conclude_def LtA ).

assert (¬ LtA E F D E F D) by (conclude lemma_angletrichotomy).

contradict.

}

assert (¬ eq D E).

{

intro.

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

assert (nCol D E F) by (conclude_def Triangle ).

contradict.

}

assert (Cong A B D E) by (conclude lemma_trichotomy1).

assert (Cong B A E D) by (forward_using lemma_congruenceflip).

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

close.

Qed.

End Euclid.