proposition: Lemma Cd_Cd_EqF : forall P Px1 Py1 Px2 Py2, Cd O E SS U1 U2 P (proj1_sig Px1) (proj1_sig Py1) -> Cd O E SS U1 U2 P (proj1_sig Px2) (proj1_sig Py2) -> Px1 =F= Px2 /\ Py1 =F= Py2.
proof: Proof. intros. unfold EqF. rewrite <- (eq_points_coordinates O E SS U1 U2 P _ _ P);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