src/HOL/Integ/IntDef.thy

 
 
 subsection{*Strict Monotonicity of Multiplication*}
 
 text{*strict, in 1st argument; proof is by induction on k>0*}
-lemma zmult_zless_mono2_lemma [rule_format]:
-     "i<j ==> 0<k --> int k * i < int k * j"
-apply (induct_tac "k", simp)
+lemma zmult_zless_mono2_lemma:
+     "i<j ==> 0<k ==> int k * i < int k * j"
+apply (induct "k", simp)
 apply (simp add: int_Suc)
-apply (case_tac "n=0")
+apply (case_tac "k=0")
 apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less)
 apply (simp add: zadd_zless_mono int_Suc0_eq_1 order_le_less)
 done
 
 lemma zero_le_imp_eq_int: "0 \<le> k ==> \<exists>n. k = int n"