# Library GeoCoq.Elements.OriginalProofs.proposition_06

Require Export GeoCoq.Elements.OriginalProofs.proposition_06a.

Require Export GeoCoq.Elements.OriginalProofs.lemma_trichotomy1.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_06 :

∀ A B C,

Triangle A B C → CongA A B C A C B →

Cong A B A C.

Proof.

intros.

assert (¬ Lt A C A B) by (conclude proposition_06a).

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

assert (¬ Col A C B).

{

intro.

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

contradict.

}

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

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

assert (¬ Lt A B A C) by (conclude proposition_06a).

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

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

assert (Cong A B A C) by (conclude lemma_trichotomy1).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_trichotomy1.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_06 :

∀ A B C,

Triangle A B C → CongA A B C A C B →

Cong A B A C.

Proof.

intros.

assert (¬ Lt A C A B) by (conclude proposition_06a).

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

assert (¬ Col A C B).

{

intro.

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

contradict.

}

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

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

assert (¬ Lt A B A C) by (conclude proposition_06a).

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

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

assert (Cong A B A C) by (conclude lemma_trichotomy1).

close.

Qed.

End Euclid.