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