proposition: Lemma oppF_neq0 : forall f, ~ f =F= 0 <-> ~ - f =F= 0.
proof: Proof. intro; split; intro HF; intro H; apply HF; clear HF; 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