equal
deleted
inserted
replaced
36 lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y" |
36 lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y" |
37 unfolding less_le by blast |
37 unfolding less_le by blast |
38 |
38 |
39 lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y" |
39 lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y" |
40 unfolding less_le by blast |
40 unfolding less_le by blast |
41 |
|
42 lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y" |
|
43 by (erule contrapos_pn, erule subst, rule less_irrefl) |
|
44 |
41 |
45 |
42 |
46 text {* Useful for simplification, but too risky to include by default. *} |
43 text {* Useful for simplification, but too risky to include by default. *} |
47 |
44 |
48 lemma less_imp_not_eq: "x < y \<Longrightarrow> (x = y) \<longleftrightarrow> False" |
45 lemma less_imp_not_eq: "x < y \<Longrightarrow> (x = y) \<longleftrightarrow> False" |