proposition: Theorem ropp_neq_0 r : ~ -(1) == 0 -> ~ r == 0 -> ~ -r == 0.
proof: Proof. intros. setoid_replace (- r) with (- (1) * r). - apply field_is_integral_domain; trivial. - now rewrite <- ropp_mul_l, rmul_1_l. Qed.
imports: ZArith_base