proposition: Lemma coordinates_of_point_f : forall P, {C | Cd O E SS U1 U2 P (fst C) (snd C)}.
proof: Proof. intros; apply constructive_definite_description; rewrite <- unique_existence. split. { destruct (coordinates_of_point O E SS U1 U2 P orthonormal_grid) as [X [Y H]]. exists (X,Y); auto. } { intros x y Hx Hy; destruct x as [Xx Xy]; destruct y as [Yx Yy]; simpl in *. assert (T:=eq_points_coordinates O E SS U1 U2 P Xx Xy P Yx Yy Hx Hy). assert (U: Xx = Yx /\ Xy = Yy) by intuition. destruct U; subst; auto. } Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems