proposition: Lemma field_prop_zero : forall a b, ~ b =F= 0 -> a/b =F= 0 -> a=F=0.
proof: Proof. intros. assert (a/b * b =F= 0*b). rewrite H0. field. setoid_replace (a/b*b) with (a) in H1. rewrite H1. ring. field. 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