equal
deleted
inserted
replaced
32 (** Combining of literal coefficients in sums of products **) |
32 (** Combining of literal coefficients in sums of products **) |
33 |
33 |
34 lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$-y $< #0)" |
34 lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$-y $< #0)" |
35 by (simp add: zcompare_rls) |
35 by (simp add: zcompare_rls) |
36 |
36 |
37 lemma eq_iff_zdiff_eq_0: "[| x: int; y: int |] ==> (x = y) \<longleftrightarrow> (x$-y = #0)" |
37 lemma eq_iff_zdiff_eq_0: "[| x \<in> int; y \<in> int |] ==> (x = y) \<longleftrightarrow> (x$-y = #0)" |
38 by (simp add: zcompare_rls) |
38 by (simp add: zcompare_rls) |
39 |
39 |
40 lemma zle_iff_zdiff_zle_0: "(x $<= y) \<longleftrightarrow> (x$-y $<= #0)" |
40 lemma zle_iff_zdiff_zle_0: "(x $<= y) \<longleftrightarrow> (x$-y $<= #0)" |
41 by (simp add: zcompare_rls) |
41 by (simp add: zcompare_rls) |
42 |
42 |