equal
deleted
inserted
replaced
990 done |
990 done |
991 |
991 |
992 lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k" |
992 lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k" |
993 by (drule mult_less_mono2) (simp_all add: mult_commute) |
993 by (drule mult_less_mono2) (simp_all add: mult_commute) |
994 |
994 |
995 lemma zero_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)" |
995 text{*Differs from the standard @{text zero_less_mult_iff} in that |
|
996 there are no negative numbers.*} |
|
997 lemma nat_0_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)" |
996 apply (induct m) |
998 apply (induct m) |
997 apply (case_tac [2] n, simp_all) |
999 apply (case_tac [2] n, simp_all) |
998 done |
1000 done |
999 |
1001 |
1000 lemma one_le_mult_iff [simp]: "(Suc 0 <= m * n) = (1 <= m & 1 <= n)" |
1002 lemma one_le_mult_iff [simp]: "(Suc 0 <= m * n) = (1 <= m & 1 <= n)" |