# Library GeoCoq.Elements.OriginalProofs.proposition_26B

Require Export GeoCoq.Elements.OriginalProofs.lemma_26helper.

Require Export GeoCoq.Elements.OriginalProofs.lemma_trichotomy1.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_26B :

∀ 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 A B D E →

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

Proof.

intros.

assert (¬ Lt E F B C) by (conclude lemma_26helper).

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

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

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

assert (¬ Lt B C E F) by (conclude lemma_26helper).

assert (¬ eq B C).

{

intro.

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

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

contradict.

}

assert (¬ eq E F).

{

intro.

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

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

contradict.

}

assert (Cong B C E F) 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_26B :

∀ 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 A B D E →

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

Proof.

intros.

assert (¬ Lt E F B C) by (conclude lemma_26helper).

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

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

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

assert (¬ Lt B C E F) by (conclude lemma_26helper).

assert (¬ eq B C).

{

intro.

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

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

contradict.

}

assert (¬ eq E F).

{

intro.

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

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

contradict.

}

assert (Cong B C E F) 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.