[STATEMENT]
lemma pos_zmult_pos:"\<lbrakk> 0 \<le> (a::int); 0 < (b::int)\<rbrakk> \<Longrightarrow> a \<le> a * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; 0 < b\<rbrakk> \<Longrightarrow> a \<le> a * b
[PROOF STEP]
apply (case_tac "a = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 \<le> a; 0 < b; a = 0\<rbrakk> \<Longrightarrow> a \<le> a * b
 2. \<lbrakk>0 \<le> a; 0 < b; a \<noteq> 0\<rbrakk> \<Longrightarrow> a \<le> a * b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; 0 < b; a \<noteq> 0\<rbrakk> \<Longrightarrow> a \<le> a * b
[PROOF STEP]
apply (frule zle_imp_zless_or_eq[of "0" "a"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; 0 < b; a \<noteq> 0; 0 < a \<or> 0 = a\<rbrakk> \<Longrightarrow> a \<le> a * b
[PROOF STEP]
apply (thin_tac "0 \<le> a")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < b; a \<noteq> 0; 0 < a \<or> 0 = a\<rbrakk> \<Longrightarrow> a \<le> a * b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done