# Library RulerCompassGeometry.B8_Point_Def

Require Export B7_Triangle_Equilateral.

Section POINT_PROPERTIES.

Lemma ExistsHalfLineEquidistant : forall A B C D : Point,
A <> B ->
C <> D ->
{E : Point |
HalfLine A B E /\
Distance A E = Distance C D}.
Proof.
intros A B C D Hab Hcd.
setLine A B Hab ipattern:L ipattern:AB.
setCircle A C D Hcd ipattern:G ipattern:ACD.
setLinterposC L G AB ACD ipattern:E ipattern:H1 ipattern:H2 ipattern:H3 ipattern:H4.
apply CollinearABA.
exists E; canonize.
Qed.

Lemma HalfLineEquidistantEqual : forall A B C : Point,
A <> B ->
HalfLine A B C ->
Distance A B = Distance A C ->
B = C.
Proof.
intros.
setLine A B H ipattern:L ipattern:AB.
setCircle A A B H ipattern:G ipattern:Aab.
setLinterposC L G AB Aab ipattern:D ipattern:H2 ipattern:H3 ipattern:H4 ipattern:H5.
apply CollinearABA.
rewrite <- (H5 B).
apply H5.
canonize.
elim (NotClockwiseBAA C A); auto.
generalizeChangeSense.
elim (NotClockwiseABA C A); auto.
canonize.
exact (NotClockwiseBAA B A H2).
exact (NotClockwiseABA B A H2).
Qed.

Lemma ExistsBetweenEquidistant : forall A B C D : Point,
A <> B ->
C <> D ->
{E : Point |
Between E A B /\
Distance A E = Distance C D}.
Proof.
intros A B C D Hab Hcd.
setLine A B Hab ipattern:L ipattern:AB.
setCircle A C D Hcd ipattern:G ipattern:ACD.
setLinternegC L G AB ACD ipattern:E ipattern:H1 ipattern:H2 ipattern:H3 ipattern:H4.
apply CollinearABA.
exists E; canonize.
destruct (ClockwiseExists B A (sym_not_eq Hab)) as (F, H5).
subst; elim (NotClockwiseAAB A F); auto.
generalizeChangeSide.
Qed.

Lemma ExistsEquidistantBetween : forall A B C D : Point,
A <> B ->
C <> D ->
{E : Point |
Between A B E /\
Distance B E = Distance C D}.
Proof.
intros A B C D Hab Hcd.
setLine A B Hab ipattern:L ipattern:AB.
setCircle B C D Hcd ipattern:G ipattern:BCD.
setLinterposC L G AB BCD ipattern:E ipattern:H1 ipattern:H2 ipattern:H3
ipattern:H4.
apply CollinearABB.
exists E; canonize.
Qed.

Lemma CentralSymetPoint : forall A B : Point,
A <> B ->
{C : Point | Distance A B = Distance B C /\ Between A B C}.
Proof.
intros.
destruct (ExistsBetweenEquidistant B A A B (sym_not_eq H) H) as (C, (H0, H1)).
exists C; generalizeChangeSide.
Qed.

Lemma CoordinatePoint : forall A B : Point,
A <> B ->
{C : Point | HalfLine Oo Uu C /\ Distance Oo C = Distance A B}.
Proof.
intros.
exact (ExistsHalfLineEquidistant Oo Uu A B DistinctOoUu H).
Qed.

End POINT_PROPERTIES.