proposition: Theorem fld_eq_mul_0_r : ∀ n m, (n * m = 0)%K → (n ≠ 0)%K → (m = 0)%K.
proof: Proof. intros n m Hnm Hm; simpl in Hnm, Hm; simpl. rewrite <- rng_mul_0_r in Hnm. apply fld_mul_reg_l in Hnm; assumption. Qed.
imports: Utf8 Setoid