Require Export GeoCoq.Elements.OriginalProofs.lemma_extension.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_samesidereflexive : 
   forall A B P, 
   nCol A B P ->
   OS P P A B.
Proof.
(* Goal: forall (A B P : @Point Ax) (_ : @nCol Ax A B P), @OS Ax P P A B *)
intros.
(* Goal: @OS Ax P P A B *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: @OS Ax P P A B *)
assert (~ eq P A).
(* Goal: not (@eq Ax P A) *)
(* Goal: @OS Ax P P A B *)
 {
(* Goal: not (@eq Ax P A) *)
 intro.
(* Goal: @OS Ax P P A B *)
 assert (Col A B A) by (conclude_def Col ).
(* Goal: False *)
 assert (Col A B P) by (conclude cn_equalitysub).
(* Goal: False *)
 contradict.
 }
(* Goal: @OS Ax P P A B *)
assert (neq A P) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists C, (BetS P A C /\ Cong A C A P)) by (conclude lemma_extension);destruct Tf as [C];spliter.
(* Goal: @OS Ax P P A B *)
assert (Col A B A) by (conclude_def Col ).
(* Goal: @OS Ax P P A B *)
assert (OS P P A B) by (conclude_def OS ).
(* Goal: @OS Ax P P A B *)
close.
Qed.

End Euclid.


