proposition: Lemma coordinates_of_point_F : forall P, {C: F*F | Cd O E SS U1 U2 P (proj1_sig (fst C)) (proj1_sig (snd C))}.
proof: Proof. intros; destruct (coordinates_of_point_f P) as [C HC]. assert (T:=HC); apply Cd_Col in HC; destruct HC as [HCol1 HCol2]. exists (exist (fun P => Col O E P) (fst C) HCol1, exist (fun P => Col O E P) (snd C) HCol2); simpl; assumption. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems