Library construction_functions

Require Import Epsilon.
Require Import gravityCenter.

Section T.

Context `{MT:Tarski_2D_euclidean}.
Context `{EqDec:EqDecidability Tpoint}.
Context `{InterDec:InterDecidability Tpoint Col}.

Lemma symmetric_point_ex_unicity :
 ∀ I A, ∃! B, is_midpoint I A B.
Proof.
intros.
elim (symmetric_point_construction A I).
intros B H.
∃ B.
unfold unique.
split.
assumption.
eauto using symmetric_point_unicity.
Qed.

Definition symmetric_point I A := select_the (symmetric_point_ex_unicity I A).

Definition gravity_center A B C (H:¬Col A B C ) := select_the (is_gravity_center_exist_unique A B C H).

End T.