coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Michael Soegtrop <MSoegtrop AT yahoo.de>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Proving p: Z is prime for large p
- Date: Tue, 5 Apr 2022 16:49:12 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=MSoegtrop AT yahoo.de; spf=Pass smtp.mailfrom=msoegtrop AT yahoo.de; spf=None smtp.helo=postmaster AT sonic309-20.consmr.mail.ne1.yahoo.com
- Ironport-data: A9a23:XDum1azRPzsSs5fMWBJ6t+eiwCrEfRIJ4+MujC+fZmUNrF6WrkUPz mRLUWyBPf7bYjSmLtp+PY629RwGucDQyNRjTAtlqlhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefQAOOU5NfsYkidfyc9IMsaoU8lyrZRbrJA24DjWVvR4 Y6q+aUzBXf8s9JKGjJMg068gEg31BjCkGtwUosWOJinFHeH/5UkJMp3yZOZdxMUcaEIdgKOf Nsv+Znilo/vE7jBPfv++lrzWhVirrc/pmFigFIOM0SpqkAqSiDfTs/XOdJEAXq7hQllkPgo6 edzmKS6cTt5AfXdn7sUVhB7KCFxaPguFL/veRBTsOSIyEvHeCC0krA0VAc9OosD//wxBGhP8 boeJWlLfxmDgOXwy7W+IgVurpp9apC1Z8VG6i0mlG2HZRolacirr6Hi4MRf0TgsnMdWNefXZ 80eLzZiBPjFS0YXYwdOWM1k9AuurijGc2II8QO/nPFt/nLsxVFx64euF9WAL7RmQu0OxBjC+ zufl4jjOTkRM8Xawj6Y+Fq3l+rXlGX6XpgTHfu27JZXbEa73WsVCRZNDQr++6H/gUm4QNdFb Ukd+y5oq6Vrsl2iTt76GRa/pRZooyLwRfIJMt8ExTmH8paE3F6IATcNSzdiU9wp4ZpeqSMR6 neFmNbgBDpKubKTSG6A+rr8kd9UEXdIRYPlTXBaJTbp8+UPs6lv10iRF48L/Lqdy4yoSGqtn 1hmuQBn3+1L5fPnwZlX6rwub9iEgZ3ATgddCu7/ADL8v1wRiGJIi+WVBbXz9vFGLY3CFgjE5 iBCkM+Y9+UUS5SElSjLRuhUWqCg5/GCdjbbhDaD/qXNFRzyqhZPnqgKuFmSwXuF1O5ZIFcFh 2eO42tsCGd7ZifCUEOOS9vZ5z4W5abhD8/5cfvfc8BDZJN8HCfeon0/PRfBgz63zhF9+U3aB Xt9WZn2ZZr9Ifs8pAdau89HuVPW7n1vmj6LGfgXMTz9gebDDJJqdVv1GADUMLpktfrsTPT99 N9DN4OKzBFTUevxeUHqHX07cjg3wYwALcmu8aR/L7bdSiI/QT1JI6KPndsJJtM994wIx7+g1 izsASdwlQuv7VWZcl7iQi44N9vSsWNX9i5T0doEZgvwhxDOoO+HsM8iSnfAVeJ+rrY+kqcoE aJtlgfpKq0ndwkrMg81NfHVxLGOvjzw7e5XFyb6MjU5YbB6QAnFpo3tcgf1pHsfByqwso0yr uT4hA/cRJMCQSVkDdrXMa7+kQnu4CJFwO8iDVHVJtRzeVn39NQ4ISLGiPJqcdoHLg/Ox2fH2 gvPWUUYqODBrpUb6t7MgazY/Y6lH/EuTFtTH27cq7q7bHGI8m2myI5GceCJYTGECDKqovr/P 70NwqilYvMdnVtMv45tKJpRzPozt4n1urtX7gV4B3GXPV6lPbVtfyud1s5Vu6wRm7JUtFfkW k+L/dUGa7yFNNm+TwwKIwwkZb/bhLROwn/Z6vIuJV+84SZ2+PyBXBwULhCMjysbJ7xwadt3z eAksc8Qygq+lht1Y47a1n0OrzyBfi4aTqEqlpAGG4u02Acmz1d1Z5aDWCL75Ze4bcpBbxsxK TiOiaue3LlRmhjYf3woGSSf1OZRn89R6gtNyl4JfAzY34CdwPQw2gZU63IyRwVRiBNKiqRiM 2hsMAt+IqDXp2Vkg81KXmaNHQBdBULIohCplgFRzGCJHVO1UmHtLXEmPbnf8U0c9VVadGcJ8 bydzlHjTju3Ltr62TE/WBI+pvHuJTCrGtYuRCx68wW585gGjf7NmaioZGFT80qiW5t3j0rBv uxwuuN5aKm9MyNJ5bwyC46dk78XTXho4YCEre5JpMs08aP0IVleGgRi72igc8NKILrG/CdUz uRwc9lXWU3WODmm91gm6G1lH1OwtO8g5N0FPL/mTYLDX31zsRIx2K/tGuPCaKPHjjmgfQvR6 m8cSt5aLlGtuA==
- Ironport-hdrordr: A9a23:b/CfCawDy9Z2JbO8QGnOKrPw0b1zdoMgy1knxilNoG9uA6ilvu qpm+kW0gKxrToXVmwg8OrwRJVoJkmsj6KdgLNhRotKOTOMhILGFuFfBOfZskTd8mjFh5ZgPM RbAstD4b/LbGSS5PySiGbXLz9j+qjgzEnCv5a6854Cd3AMV0gt1XYaNu/iKDwKeCB2QaAeM7 q3oudkhx7lQ1Q4Sa2AbEUtbqz4odrKntbDTnc9ayLOvGG14A+V1A==
- Ironport-phdr: A9a23:Dt4L0BLh4lfHKT0La9mcuL5tWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCFv7M00wOCAtiTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnA JYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yf6+94fObwhKizexbrF/I RWrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+V rxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4 aV2Rx/ykCoJNDA3/27ZhcJtkqxbrhKvqB5jzIDbZ4+YL+Z+c6HHcN8GX2dMUMRcWipcCY28d YsPCO8BMP5foYn8u1QOrQGxCheoBOjy1zFIgWH53aIm0+Q7FgHGxBErEtUJvnrJq9X6KqgSU fyvzKnP1TXOdPNX1i396IjPdRAtu+yDUqxpfMfX1EIgGB/LgE+Kpoz5IzOayP4Ns26D4ud8V ++ilWoqpg5xrzWgwsohipfFiIwJx13Y+ih0zpo4KcO5RUB1YNOpEoVcuiKUOodqX84sTGFmt SY5x7Eap5K2ejUBxpc/xxPHavGKcpKE7g/iWeufOzt0mXFodb2lixqv/kWty+vxXdSu3llQt CpKiNzMu2gN1xPN7siHTeNw/lym2TaJ1gDc9u9JLVwwmKbCNZIt3qQ8mYYUsUTFBS/2nV/2g LWTdko+++io7/7rYrP4qZOBLYN1ihvxMqQpmsy4G+g3Lg8OX22D9eS90r3s41H5Ta1Lg/A3i KXVrZHXKMoBqqKkAAJY3Zwv5wuwAjqnyNgYmGMILFNBeBKJlYjpPFTOLej9DfekhFSjjjhrx +zcPr3mGpXANXjCn63hfbZ67E5Q0hc8ws5H65JSEb4OOOjzVVPptNzEEh85NBS5z/v/BNVny oweQX6PArOeMK7KrVCI4fsvL/CQa48RpTbyMOMo5+XujH88gV8SZ7Ol3ZoRaHCiH/RpOV+VY XT2goRJLWBftQ0nCefulVeqUDhJZn/0UbhvyCs8DdeDDIzDT42pyIeG0SinBJpOLjRjMVeBH mvycJ2sSv4MbyXULsI3wW9MbqSoV4J0jULmjwT90bcydoI8mwUdvJPnjp1u4vHL0As1/npyB tic1GeESyd1mHkJTnk4xvM3ulRzn3GE16UwmPlEDZpL/focdzw9OJHA1etiI8H7WgXGONuEG x69WtvzOTgqVZoqxsMWJUN0GtGslBfGii+xBLIai6aMHLQl+6Lb2D79KpU10G7IgY8miVRuW c5TLSumi6p4ohDUHJLMml6FmryCbqMa3SWWrDbGlzLIt0ZeSwtqF6DMXHRZYEaP68Xw5kTFC bSpDNzLKyNnzsiPYutPY9zt1xBdQev7fc7ZaCS3knuxAhCBwvWNapDrciMTxneVDk9MiA0V8 XucUGp2Ti68v2LTCiBvHlPzcgvt9+d5snayUk4zyUmDcURg07O//hNdi+abTrsf2bcNuSFpr DsRfh71+unRBtWcvQ15VLRVYdQ6pltKlCrYuwF7Ip28PvV6nFdNOw9zvk7oy1B2EtAez45z8 ihslVoub/vEjgAkFXvQx537N7zJJ3On+Rmub/STwVTCyJOM/axJ7v0kqlLltQXvF0w48nwh3 cMGthnUrpjMEgcWVor8F0gt8B0v7bTBZSQy+5nTzVV9OKmztXnO1ph6YYltggblZNpZPK6eQ UXXKMoXCNS0L/QCilGpaRVCMO0Yp+YkesihcfWBwquiOu1tySmngWpw64d4ykuQ9iB4R4Ykx r49yuqDlkuCXjb41hK6t9zv3JpDbncUF3a+zi7tAMhQYLdzdMAFEzXmL8qyz9R4z5njPhwQv Fu4AF4JxNWuYTKDZlz62ktc2AwbrGemli2x0zFv22936PPBh2qXk7ikLUZZcmdQDHFvl1LtP ZS5g7V4FACzYg4lmQHkrUf2yq5HpbhuemzaQENGZS/zfClpVqq9sKbHYtYats1u6HsMFr3sP RbDFuCuxnlSmznuFGZf2j0hIjSju5Gj2gd/lHrYNnF46nzQZcB3wx7bot3aX/9YmDQcF0waw XHaAEaxO96x8JCajZDG56q7TGWsWYFJdjHD3IqAsyz96WAgUnjd17ij38bqFwQ3y3qx0sJtW CrUthHkSpji16O9d+5qNBogFBr37Mx0HZt7m407icQL2HQUsZ6S+GIOjWb5NdgIvMC2JGpIX zMAxMTZpRT0wEA2ZGzc3Jr3Dz/OitskfdSxZXkanz4w/9wfQrnB96RKxGNtvkDqvAvRZv87l TAYrJlmoGYGmbMYsQoqyWObD6xaSkBcOWaEew2gyde4oe0XYW+udeL1z09ihZW7C7rEpAhAW XH/c5NkHClq78w5PkiemHv0oprpftXdd7dx/lWdjgvAgu5JKZkwiutChCxpPnj4tGEkzOhzh AJn3JWztoyKY2t3+6fxDhldPzzzL8Qdn1Olxb5ZhdqT1puzE49JATINXZCzFaPtSmpUvvPhL AOUVjg1q3PdH7eGWx6W6EBh6XnIFtHOVTnfJXUUy8ljWAjIJEFbh1NcVzE7k5glUwGykZK/N h4nvXZItgK+80cSmYcKf1HlX2zSpRmlcGIxQZmbdl9N6x1aol3SOoqY5/5yGCdR+tugqhaMI yqVfVctbylBV0qaClTkJrTr68PH9r3SA/G5IvTSe7KWgf1XV/CPg56imNgDnX7EJoCUM39uA udukFJERmx8Et/Fli8nUCsRlimWN5/e/k/68SpxtcWltvHiWQap44bWTapbMdJovRuxhO3QU ozYzDY8IjFe2JQWwHbOw7VKx18ehRZlcDy1GKgBvyrAJEo1sr5eDxkcLS9+ZpMgB0MUxQ5LO MWA0oKwjOY+hfkzEFJfE1nom8XvY8FTZXC0NFTAQk2MMebeTdUk69D+YaS7D7Fd3rw8ig==
- Ironport-sdr: nHpxRYZrGnD9NCLSBhbK4IUjvTUwLmMbH4I5h55qhtCmuBjUHiB/NNOLuJGiLLSuLpJ5FwFLqJ yhUYGabPLkDsQzjcFGDxA4PUEPrMvOPxJIMp5G59uY4Ab0q1/rp51EjsOfCTI49rHv0wUlB2NH CEllhwJQnUFwsub5MahmSAwJmb1jNa38qCATvRCRnCXvh2fjNtI6uv2B2+cseZbB1SDeeoDxD+ 6CJWKRWcn0WbiwnnM0lY/tje9ae+wQEHRgtRgsxdIIb25lE6XOU4IHxQlu/036a1ya/f0+QkSA NsyBTLbH0MVa0o0Wi/5xN8zb
Btw.: CoqPrime (the libraries and the certificate generators and converters) is included in Coq Platform since the 2022.01 release. The certificate generators and prerequisites also have opam packages since then, so it should be easy to install.
Best regards,
Michael
- [Coq-Club] Proving p: Z is prime for large p, Timothy Carstens, 04/04/2022
- Re: [Coq-Club] Proving p: Z is prime for large p, roux cody, 04/05/2022
- Re: [Coq-Club] Proving p: Z is prime for large p, Benoît Viguier, 04/05/2022
- Re: [Coq-Club] Proving p: Z is prime for large p, Timothy Carstens, 04/05/2022
- Re: [Coq-Club] Proving p: Z is prime for large p, Michael Soegtrop, 04/05/2022
- Re: [Coq-Club] Proving p: Z is prime for large p, Benoît Viguier, 04/05/2022
- Re: [Coq-Club] Proving p: Z is prime for large p, mukesh tiwari, 04/05/2022
- Re: [Coq-Club] Proving p: Z is prime for large p, roux cody, 04/05/2022
Archive powered by MHonArc 2.6.19+.