equal
deleted
inserted
replaced
1115 from `m \<ge> n` obtain q where "m = n + q" |
1115 from `m \<ge> n` obtain q where "m = n + q" |
1116 by (auto simp add: le_iff_add) |
1116 by (auto simp add: le_iff_add) |
1117 with `n > 0` show ?thesis by simp |
1117 with `n > 0` show ?thesis by simp |
1118 qed |
1118 qed |
1119 |
1119 |
|
1120 lemma div_eq_0_iff: "(a div b::nat) = 0 \<longleftrightarrow> a < b \<or> b = 0" |
|
1121 by (metis div_less div_positive div_by_0 gr0I less_numeral_extra(3) not_less) |
1120 |
1122 |
1121 subsubsection {* Remainder *} |
1123 subsubsection {* Remainder *} |
1122 |
1124 |
1123 lemma mod_less_divisor [simp]: |
1125 lemma mod_less_divisor [simp]: |
1124 fixes m n :: nat |
1126 fixes m n :: nat |