# Library GeoCoq.Elements.OriginalProofs.lemma_samesidereflexive

Require Export GeoCoq.Elements.OriginalProofs.lemma_inequalitysymmetric.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_samesidereflexive :

∀ A B P,

neq A B → nCol A B P →

OS P P A B.

Proof.

intros.

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

assert (¬ eq P A).

{

intro.

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

assert (Col A B P) by (conclude cn_equalitysub).

contradict.

}

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

let Tf:=fresh in

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

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

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

close.

Qed.

End Euclid.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_samesidereflexive :

∀ A B P,

neq A B → nCol A B P →

OS P P A B.

Proof.

intros.

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

assert (¬ eq P A).

{

intro.

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

assert (Col A B P) by (conclude cn_equalitysub).

contradict.

}

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

let Tf:=fresh in

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

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

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

close.

Qed.

End Euclid.