proposition: Theorem field_is_integral_domain r1 r2 : ~ r1 == 0 -> ~ r2 == 0 -> ~ r1 * r2 == 0.
proof: Proof. intros H1 H2. contradict H2. transitivity (/r1 * r1 * r2). - now rewrite rinv_l. - now rewrite <- rmul_assoc, H2. Qed.
imports: ZArith_base