equal
deleted
inserted
replaced
927 proof cases |
927 proof cases |
928 assume "c < y" with a show ?thesis |
928 assume "c < y" with a show ?thesis |
929 by (auto intro!: image_eqI[of _ _ "a + c"]) |
929 by (auto intro!: image_eqI[of _ _ "a + c"]) |
930 next |
930 next |
931 assume "\<not> c < y" with a show ?thesis |
931 assume "\<not> c < y" with a show ?thesis |
932 by (auto intro!: image_eqI[of _ _ x] split: split_if_asm) |
932 by (auto intro!: image_eqI[of _ _ x] split: if_split_asm) |
933 qed |
933 qed |
934 qed auto |
934 qed auto |
935 |
935 |
936 lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}" |
936 lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}" |
937 by (auto intro!: image_eqI [where x = "nat x" for x]) |
937 by (auto intro!: image_eqI [where x = "nat x" for x]) |