equal
deleted
inserted
replaced
1724 by auto |
1724 by auto |
1725 then consider "y < (-?N x e)/ real c" | "y > (- ?N x e) / real c" |
1725 then consider "y < (-?N x e)/ real c" | "y > (- ?N x e) / real c" |
1726 by atomize_elim auto |
1726 by atomize_elim auto |
1727 then show ?case |
1727 then show ?case |
1728 proof cases |
1728 proof cases |
1729 case y: 1 |
1729 case 1 |
1730 then have "y * real c < - ?N x e" |
1730 then have "y * real c < - ?N x e" |
1731 by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) |
1731 by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) |
1732 then have "real c * y + ?N x e < 0" |
1732 then have "real c * y + ?N x e < 0" |
1733 by (simp add: algebra_simps) |
1733 by (simp add: algebra_simps) |
1734 then show ?thesis |
1734 then show ?thesis |
1735 using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp |
1735 using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp |
1736 next |
1736 next |
1737 case y: 2 |
1737 case 2 |
1738 with yu have eu: "u > (- ?N x e) / real c" |
1738 with yu have eu: "u > (- ?N x e) / real c" |
1739 by auto |
1739 by auto |
1740 with noSc ly yu have "(- ?N x e) / real c \<le> l" |
1740 with noSc ly yu have "(- ?N x e) / real c \<le> l" |
1741 by (cases "(- ?N x e) / real c > l") auto |
1741 by (cases "(- ?N x e) / real c > l") auto |
1742 with lx pxc have False |
1742 with lx pxc have False |
1757 by auto |
1757 by auto |
1758 then consider "y < (- ?N x e) / real c" | "y > (-?N x e) / real c" |
1758 then consider "y < (- ?N x e) / real c" | "y > (-?N x e) / real c" |
1759 by atomize_elim auto |
1759 by atomize_elim auto |
1760 then show ?case |
1760 then show ?case |
1761 proof cases |
1761 proof cases |
1762 case y: 1 |
1762 case 1 |
1763 then have "y * real c < - ?N x e" |
1763 then have "y * real c < - ?N x e" |
1764 by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) |
1764 by (simp add: pos_less_divide_eq[OF cp, where a="y" and b="-?N x e", symmetric]) |
1765 then have "real c * y + ?N x e < 0" |
1765 then have "real c * y + ?N x e < 0" |
1766 by (simp add: algebra_simps) |
1766 by (simp add: algebra_simps) |
1767 then show ?thesis |
1767 then show ?thesis |
1768 using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp |
1768 using numbound0_I[OF nb, where bs="bs" and b="x" and b'="y"] by simp |
1769 next |
1769 next |
1770 case y: 2 |
1770 case 2 |
1771 with yu have eu: "u > (- ?N x e) / real c" |
1771 with yu have eu: "u > (- ?N x e) / real c" |
1772 by auto |
1772 by auto |
1773 with noSc ly yu have "(- ?N x e) / real c \<le> l" |
1773 with noSc ly yu have "(- ?N x e) / real c \<le> l" |
1774 by (cases "(- ?N x e) / real c > l") auto |
1774 by (cases "(- ?N x e) / real c > l") auto |
1775 with lx pxc have False |
1775 with lx pxc have False |