equal
deleted
inserted
replaced
13 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)" |
13 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)" |
14 by (rule_tac x="b-a" in exI, simp) |
14 by (rule_tac x="b-a" in exI, simp) |
15 |
15 |
16 text{*As a special case, the sum of two positives is positive. One of the |
16 text{*As a special case, the sum of two positives is positive. One of the |
17 premises could be weakened to the relation @{text "\<le>"}.*} |
17 premises could be weakened to the relation @{text "\<le>"}.*} |
18 lemma pos_add_strict: "[|0<a; b<c|] ==> b < a + (c::'a::ordered_semiring)" |
18 lemma pos_add_strict: "[|0<a; b<c|] ==> b < a + (c::'a::ordered_semidom)" |
19 by (insert add_strict_mono [of 0 a b c], simp) |
19 by (insert add_strict_mono [of 0 a b c], simp) |
20 |
20 |
21 lemma interval_empty_iff: |
21 lemma interval_empty_iff: |
22 "({y::'a::ordered_field. x < y & y < z} = {}) = (~(x < z))" |
22 "({y::'a::ordered_field. x < y & y < z} = {}) = (~(x < z))" |
23 by (blast dest: dense intro: order_less_trans) |
23 by (blast dest: dense intro: order_less_trans) |