coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Frank Schwidom <schwidom AT gmx.net>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Beginner question: 0 - 1 = 0?
- Date: Sun, 23 Jul 2023 16:53:35 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=schwidom AT gmx.net; spf=Pass smtp.mailfrom=schwidom AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
- Ironport-data: A9a23:AlxLVqnPtdSrLF1z0n2E+EXo5gyAIkRdPkR7XQ2eYbSJt1+Wr1Gzt xIbDWzVOfeOY2X8ft5yb9m28klS6peGmNVrGwM6qiw2RFtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayajt8B56r8ks156yt4mhA5DTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1tChg2NNUW39xTAEVzx eQiDR81cReq0rfeLLKTEoGAh+wmK9T3eowaqjdmwC2x4fQOG8mZBf+QupkBgXFp16iiHt6GD yYdQSFkbAvBbxpKElgSGNQ4kfvAanzXLWcA+AzM9fpfD2770QN24ICqPf/vY4KqXflvvEmkq 2DoxjGsav0dHIXClWTcqyzEavX0tSj8QccZEKCy3uV7hUWagG0VEhwfE1WhycRVkWa7XM9Db UMR6mwooLRaGFGXosfVXBvhoHfcsDsmf9t0Lt0i0iSi8rXTylPMboQbdQJpZNsjvc4wYDUl0 F6Vgt/kbQCDVpXKERpxEZ/K/FuP1TgpwXwqOHZaFlpUizX3iN1t10iSJjp2OPTt1rXI9SfML yeiigxWa187v8MV2qOx8ErIjjTESnPhElFrvG07skqD6RllZMaPfYWi4F7Hhcuswa6cSUSd+ ncBi46Y4fxm4XCxeM6lEb9l8FKBva/t3NjgbbhHQcBJG9OFpSfLQGyoyGsiTHqFy+5dEdMTX GfduBlK+LhYN2awYKl8buqZUpp7lfC9TYq+Dq6ENrKih6SdkifYo0mCgmbPjwjQfLQEyv5X1 WqzLJj3UStHYUiZ5GDtHLhNuVPU+szO7TqOGc6ilkrPPUu2PTDMAbYDLFaUaO0lpKqLyDg5A P4PX/ZmPy53CbWkCgGOqdB7BQlTcRATW8qqw+QJLbTrClQ9Rwkc5wr5mu5Jl3pNxPgOyY8lP xiVBidl9bYIrSaddljUNig8NumHsFQWhStTABHA9G2AgxALCbtDJo9GH3fuVel6pL5Q3rRvQ uMbes6NJP1KR36Vs34edJTx5sgqPhiimQvEbWLvbSkdbqxQYVXD2ublWQ/zqwgILC687vUlr 5Oaiwj0fJskRiZZNvjwVs6B9V2KkEImqLpAZHeQeth3U2fwwbduMB3036MWIdlTCBDtxQm69 gexADUer9nCvoUwzoHohL+FnaitAeBRDkpXJEiFzLeUZA3x3Huv/p9Ea8mMJQvibWLT/L6zQ 9lVw9XXEuw1rHwTv6VSS79UnL8Dvf3xrLpk/yFYNXTsbWXzLIh/I3ODjPJ9hocUypB34QKJC 1+yoP9EMrC0OeTgIl4bBCwhSs+hjfg0uD3j3c4ZEXXAxh1c3eS4CB1JHhy2liZiAqN/M9olz ccfqccm0VGDpSRwAOmWrBJ/1jqqHiQbXrQFp6MqJtbhqjAWx2FoZb3eDS7L46+zVehcD3lyH BiqgPvturcN4GvDbHs5KlbV18V/m5klmU5H3X0CFXuzi/vHgf4FhkQN1TFqSgh+7w5m1thrM TNBLHxFJqSp/hZpivNcXmuqJRpzOR2B9mH1yHoLjGf8TXT0ZlfSLWY4B/mBzHoZ/01YYDJf2 rOSk0ThbhrHY+Dz2XEUdXN+ivm+U+F0yBLOqPqnE+uBAZM+Rzjv2Y2qRGgQrirYEdEDv1LGq cZq7dRPR/XCbwBImJICCq6eybg0YzKHLjYbQfheoYU4LVuFczS2gTWzO0S9f/1WHMPz8Gi6N Z1KBtlOXBGAxiqxvmglJaoTEYRVwt8txvQ/I43OG0BXkoGivgJIsY3R/BfQnGUEYctjuudjJ 5LzdwCtKH2xh3xVkVCc9cVvZ2yyUdYZbgjChMG07+Q7OJYRu858cUwJ8+WVvlfEFCBF7h6rr Af4SKuO9NNbyKNohJnJPpRYIgeJdePIS+WD9T6sv+R0bd/gNdnEsyUXoALFOzt6EKQwWdMts 5iwq//ygV34uYgpX1Djm5WuE7dD4eOwVrF1NuP1NHxrojuQavTz4hcs+3GKFrIRqYlzvvKYf gqfbNe8UfU3WN0HnX1cVHV4IiYnUq/yav/tmDO5o/GyESMi6A3gLu32xU+xOCsfPmUNNoblA wD5h+e265oK5M5QDRsDHLd9D4U+PFbnXrA8esbssSWDSFOlmU6GpqCogC9IBesn0ZVYOJ2SD VP5qhnCmNCavabV0JdWtpw0uBALZJq4bS/cYWpFk+OaSRjjZILFEQjZGZoDGtdSnzCaOFTQe mTWdGV7YcnidW0sTPg/iegPmi+QA/xIPNrlTtDsE4V4dA/ubL697HBdGuuMLpu4lvYPDA1qF D3GxkDNAw==
- Ironport-hdrordr: A9a23:35JBvK3esEMKrlOA9omZowqjBJwkLtp133Aq2lEZdPVwSL39qy nOpoV/6faQsl0ssR4b9uxoVJPvfZq+z+8W3WByB8bAYOCOggLBQe1fBODZowEIdReeysdg9e NHb7V0DsH2AGN3lMDg/WCDYq4dKZW8gceVbfy19QYKceiGUdAY0+/zZzzwLnFL
- Ironport-phdr: A9a23:p6Cbsx3hsZxcSNsvsmDOdg8yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaBo6gzxwCYFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoV J8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9q22uyo+5DeYgpEiTi5bLhvM Bi4sALdu9UMj4B/MKgx0BzJonVJe+RS22xlIE+Ykgj/6Mmt4pNt6jxctP09+cFOV6X6ZLk4Q qdDDDs6KWA15dbkugfFQACS+3YTSGQWkh5PAwjY8BH3W4r6vyXmuuZh3iSRIMv7Rq02Vzu/9 admUBHmhicZOTAk82/YhdB/g79Vrx+6uxxz35TZbJ2JOPdwYK/Qe84RS2pbXsZWUixMGoOyb 5EVAOoHPuZTspTzqEcOrRqwBAmjGeTvyjpVjXLxxq01z+QhEA/H3AM9GNIOtW/ZrNrwNKYdS +y1yrfHzSnaYv5QxDzy55TGfAo7rvGQQbJ/b9DRyU83Gg7Yilidp5LoMjOU2+kOvWaW4PZsW +yhhmM6twx8oCaiy8Yxh4THmI8YyF/J+Dt2zYg6O9C1SFB2b96mHZdMqi2XMZZ9TMA6Q2xwp io216MKtYSlcCQUypkr3QPTZvydf4SV5h/vTOmcLDZiiH54Zb6yiAy+/VW8xuD+TMW4zVJHo yhDn9LRrH4CzQbT5dKCSvZl/keuxzKP1wfL5+FBJkA0iLbbJ4Quwr41mZsfq0LDETHqmEnuj a+WcFsr+vSw5uj5f7nquIWQO5Fqhgz8KKgih8yyDf4lPgUKR2Sb/P6z1Lzn/U33WrVKifg2n 7HCsJ/GJcQaqK+5DBJS0oYm8Bu/ADKm0dsCkXkBMl1FZAqLj47yNF7WOvD3Ee+/g0iwkDds3 /3KI6XtAo/RIXjbjLfhYbF95lZAxwo01NBT/o5bCrUcIP3oQULxr9zZDhohMwOu2ernCdN91 pkfWW2VGKOZPrnS4he04bckJPDJb4sIsh78LeIk7rjglywXg1gYKIez1J0UIEuzHutnL0KcK S73idceEGsNuyIxSfysjlCeB20AL02uVr4xs2loQLmtCp3OE9jFaN2p2S66GsYTfWVaEhWXF m+ucYyYWvAKYSbUI8l7kzVCW6LyA5Q520SIswn3g6FiMvKS4jcR4Ino1Md06+rWvR435XpyA tjOm3qVQTRMl3gTDyQzwLg5pEV8zlmZ1q0tmPdYCt1f4PZhXQIqc5jR078yEMj8DyTGeNrBU 1O6WpOmDDU2G8o22MMLal1hFs+Kixfew2ylBq9TkbGXbHAt2oTb2XW5Z8N0ynKdkbIkk0FjW cxXc2uvmq948QHXQY/PiUSQ0aiwJ+wa22bW+WGPwHDr3gkQWRNsUajDQXEUZ1fH5dX/6ETYS rayCLMhegJfwM+GI6FOZ5Xnl1JDDPvkPd3fZSq2lQLSTV6TzbOTbYbtfk0S2TWbDkUY0kgS8 XuAKQkiF3K5uWuNRDdqFF/pfwbt6bwk8Sn9FBVriVjXKRQwhN/XslYPiPeRSu0exOcBsSYl8 HBvGUqlmsnRE5yGrhZge6NVZZU85k1G3CTXrV8YXNToIqZ8i1oZawkysVnp0kA9EY5Ajskmq 3YCww9ib6SVzBkSElHQlYC1IbDRJmToqVq0YK7J213Z1f6Z/7dJ7vkk4QarrESiEUws9G9i2 t9e3i6H55nEOwEVVIr4Tkc98xUSS6jyWiAm/MuU0HRtNfLxqTrew5cyA/NjzB+8ftBZOafCF QnoEsRcCdL8YOAtnlGoaFoDMoUwvOYvNMO5dveB3YakOfYmmj+6xWhK+4Fy1EuQ+jE0ELeSm cxfnLfBg03eBn/1lx+5v9rymJxYaD13fCL30iXiCINLJ+VzcYsNFWayMpiyz9R6iYTqXi0Q/ 1qiClUanc6xLEDLNRqnh1IWjBlR+C30/EnwhyZ5mDwosKeFiSnHwuC5MQECJnYOX256y1HlP YmzidkeGkmudQkg0hW/tiOYj+BWorpyK27LTAJGZS/zeit5Wauvt7aFZuZA7YNutyhLGrfZA xjSWvvmrh0W3jm2VXBVxC86ezavkpr8j1p8hX7Xfz5j6XHef8933xLW4tfREOVQ0jQxTy59k TDLB1K4MorMn53ch9LZv+u5TW7kSoxLfHyh09abrCXirz4iEVilkvu0gNGiDQUqzXqxyYxxT SuRyXS0Kojzi/bgaLkhJxc1QgGgrZI9QNo2k5Ns1s5MnyJC1tPIuyRb1j2tedRDhfCkNSBLH 2RUhYePvk68gh0kdC/spcqxV23BkJE4PZ/gODxQg397t4cQVe+V9OAWx3Iv5ADi8kSIPr4l2 W1Cgfo2tCxF36dT4FprkmPEU+pVRxc9X2SklgzUvYDk6vwJOSD2LOn2jA0kwZigFO3Q+FgDH imjPM16QmkoqZ8geFPUjC+jsMe9JoSWN4hC8EbN9nWIx+lNdMBhzLxT23chYzml+yd8g/gyi RgktX2jlK6ALWglvKewAxoDcybwe9tW4Tb1y6BXgseR2YmrWJRnADQCGpXyH7quF3oJuPLrO hzrcnV0o2qHGbfZAQ6U6Vt353PJHZexMniLJX4fhdx8TRiZLUZbjUgaRjI/1pI+EwmrwoTmf iIbrngJ4UXkrxJX1u9yHxz4T3uZqwK4LDE5VNnXLRZb6B1D+1aAMcGa6bEWfWkQ9ZmgoQqRb 22DMl4RVydTABPCXg2lZ+j9gLuIu/KVDee/MfbUNLCHqOgFEuyN2YrqyYx+uTCFKsSIOHBmS fw9wEtKG35jSKG7030CTTIakyXVYouVvhC5r2dspcCg8fjsXSrg4JvJDbZOe4YKmVj+keKYO uiciTwsYy5fzY8JzGTUxaI32VkPl2dhcinrF7kc/32oLuqYiupcCBgVbDl2Pc1D4vcn3wVDD sXcj8v8yr9yivNd47htWlnx3MekeZ5TS4lcHFbAGVrNO7GWYzvG35OvCUtZYbJVnKNSugHi4 V6m
- Ironport-sdr: 64bd3f29_IRqaoWot20ujT3qMxdRTlPHpXIujtbUsoEoivgjM00RKguy tFSmrO7kMv45tazDOFzoe19Z8Ec946d0jc44fqA==
- Ui-outboundreport: notjunk:1;M01:P0:fowRa60EQX8=;tY8yVm3DohYktQfL+AQLmYyMH/g zflMrdVYonWpXCHpgntSSra1wB9MyXhLl6NU710/t4zzApJu5fBH+O/FfErfc/ZH0aShACPQy kKLUCQnn/oO86ZF8tQOgc9AMRFgaU67G5Tb7fykXm4gJ6QPeJDHP6a3739RPv0WxM5HVVfWSX nA4JYJ2yVHB/1Hr55/qmrQQKqX9QaUpQOtA+iSNDWIoSM5UGivAOxyY5oP8btOT/6FTo4Y8Ct 5PN/nPOQVEJnU7cak4H7e/nmqXI/IxwYEeGcobWOY8beWoEfYK/CiLlkhCARQJlzUEhjqm/Y2 MHm7AbI5PjKis/gfhz158galeHN1mlQQzfV8AsvowGIQH6civKsbJOmx2PKkh78iDKUzSsGCP M67m6pch8aSknw6+f9aIHBCyGJJclsUUHu6py4J4X2CImcbq2B77p+cNjMBWR57I32CqHpF1r VK/dTVy138dL1LHKSXrvy9oWzDu5hsxr7eElGeg7HmyFtxiE8qHzUR234wbcjd5KepQiou32V ByD++5an32u0VskV73GdEICE1OHi5dOon9pgRxqODZE1MuwzIB5YnNpmCiu4QYcvF6b6aCQ/O giZ0kkhS0yaiPS1Alu3Fokxi0STJmvFi+g8L4wJwXdpBPvGM5fXiIix7q0G0CwKue0NsafXTy 6r1Nb3zpg/k1Sl+r0sH0YCjrzkWxI0+xsK+Z8P9pn51ceapACQIMaY5uQ/klPCbMILBjWsPv2 UQf84dFEbHKp9JJacnYnBzG2Rn0H9+Eb4KFFPdsrmgryY+rb50N8N4itg8OfToznSl9xiojyj dQt9Ztbwk6uQSSKgbWNnU43VhSSLOguJX/22uotJJkyAJVRRuQgyAOLKVzMSkTeRAtBkPfkvY FNETxM/oIhP74v29hrHianw9v8ec2jgfeRieIcHSKuOK257rcjRw1BUJOhxLVbaK8YAXaHUTn Baveg1hLK63wbDqBLuxqXRF0pFw=
Hi,
what puzzles me is that I can obviously get a wromg result from the view of
the natural understanding:
Coq < Compute 0 - 1.
= 0
: nat
How can it be clear that this makes no problems in proofs?
Regards,
Frank
- [Coq-Club] Beginner question: 0 - 1 = 0?, Frank Schwidom, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Dominique Larchey-Wendling, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Sylvain Boulmé, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Ana Borges, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Castéran Pierre, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Qinshi Wang, 07/24/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Hugo Herbelin, 07/26/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Qinshi Wang, 07/24/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Castéran Pierre, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Tadeusz Litak, 07/24/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Ana Borges, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Sylvain Boulmé, 07/23/2023
- Re: [Coq-Club] Beginner question: 0 - 1 = 0?, Dominique Larchey-Wendling, 07/23/2023
Archive powered by MHonArc 2.6.19+.