proposition: Lemma subF__eq0 : forall x y:F, x - y =F= 0 <-> x =F= y.
proof: Proof. intros; split; intro; nsatz. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems