equal
deleted
inserted
replaced
6 imports Coset Exponent |
6 imports Coset Exponent |
7 begin |
7 begin |
8 |
8 |
9 text \<open>See also @{cite "Kammueller-Paulson:1999"}.\<close> |
9 text \<open>See also @{cite "Kammueller-Paulson:1999"}.\<close> |
10 |
10 |
11 text \<open>The combinatorial argument is in theory @{theory Exponent}.\<close> |
11 text \<open>The combinatorial argument is in theory @{theory "HOL-Algebra.Exponent"}.\<close> |
12 |
12 |
13 lemma le_extend_mult: "\<lbrakk>0 < c; a \<le> b\<rbrakk> \<Longrightarrow> a \<le> b * c" |
13 lemma le_extend_mult: "\<lbrakk>0 < c; a \<le> b\<rbrakk> \<Longrightarrow> a \<le> b * c" |
14 for c :: nat |
14 for c :: nat |
15 by (metis divisors_zero dvd_triv_left leI less_le_trans nat_dvd_not_less zero_less_iff_neq_zero) |
15 by (metis divisors_zero dvd_triv_left leI less_le_trans nat_dvd_not_less zero_less_iff_neq_zero) |
16 |
16 |