[STATEMENT]
lemma sdiv_pos_neg: "0 \<le> a \<Longrightarrow> b < 0 \<Longrightarrow> a sdiv b = - (a div - b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; b < 0\<rbrakk> \<Longrightarrow> a sdiv b = - (a div - b)
[PROOF STEP]
by (simp add: sdiv_def sgn_if)