src/HOL/Rings.thy

--- a/src/HOL/Rings.thy	Fri Sep 05 16:09:03 2014 +0100
+++ b/src/HOL/Rings.thy	Sat Sep 06 20:12:32 2014 +0200
@@ -30,6 +30,13 @@
   assumes mult_zero_right [simp]: "a * 0 = 0"
 
 class semiring_0 = semiring + comm_monoid_add + mult_zero
+begin
+
+lemma mult_not_zero:
+  "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0"
+  by auto
+
+end
 
 class semiring_0_cancel = semiring + cancel_comm_monoid_add
 begin