proposition: Lemma neqO_mul_neqO : forall x y:F, ~ x =F= 0 -> ~ y =F= 0 -> ~ x * y =F= 0.
proof: Proof. intros x y Hx Hy Hxy; apply Fmult_integral in Hxy; intuition. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems