src/HOL/Power.thy
 changeset 22624 7a6c8ed516ab parent 22390 378f34b1e380 child 22853 7f000a385606
equal inserted replaced
22623:5fcee5b319a2 22624:7a6c8ed516ab
`   289      "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"`
`   289      "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"`
`   290   by (blast intro: power_less_imp_less_exp power_strict_increasing) `
`   290   by (blast intro: power_less_imp_less_exp power_strict_increasing) `
`   291 `
`   291 `
`   292 lemma power_le_imp_le_base:`
`   292 lemma power_le_imp_le_base:`
`   293   assumes le: "a ^ Suc n \<le> b ^ Suc n"`
`   293   assumes le: "a ^ Suc n \<le> b ^ Suc n"`
`   294       and xnonneg: "(0::'a::{ordered_semidom,recpower}) \<le> a"`
`   294       and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"`
`   295       and ynonneg: "0 \<le> b"`
`       `
`   296   shows "a \<le> b"`
`   295   shows "a \<le> b"`
`   297  proof (rule ccontr)`
`   296  proof (rule ccontr)`
`   298    assume "~ a \<le> b"`
`   297    assume "~ a \<le> b"`
`   299    then have "b < a" by (simp only: linorder_not_le)`
`   298    then have "b < a" by (simp only: linorder_not_le)`
`   300    then have "b ^ Suc n < a ^ Suc n"`
`   299    then have "b ^ Suc n < a ^ Suc n"`