coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Automation for division over nat

From: Gert Smolka <smolka AT ps.uni-saarland.de>
To: "coq-club AT inria.fr Club" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Automation for division over nat
Date: Sat, 9 Feb 2019 19:07:38 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=smolka AT ps.uni-saarland.de; spf=Pass smtp.mailfrom=smolka AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
Ironport-phdr: 9a23:slrgVBAcWDgH/lr7kNAFUyQJP3N1i/DPJgcQr6AfoPdwSPv9r8bcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyI2/m7YhcJtgqxbrgyvqB58zYDTe4yVKPhzfqbBcdMaWWZNQMBcXDFBDIOmaIsPCvIMM+dGoInnu1sFsAawBQyrBOPryT9HnGL90Koh0+QkFgHG2A8gEMgVvXTMt9X5LroSUea0zKXR1jXMdelZ2S356IfSdBAuvOuAUq9ufsfIz0QkCgDLjk2IpID4MT6Y2f4Bvmya4uZ6V++jkXArpgFprjSx28shiJPFi4ELxlze8Sh0xJw5KcCkREN9fNWqCoFftzuAOItzWs4iQ39nuCI9yrAepZ67ZikKyIggxx7ZcfCHaYmJ7gj+VOaXIDd0nWlld6iliBao9Uiv0Ov8WdSu3FlXsCVJitjMtnYT2BzP8sWLV/Vw80i71TuL1g3f8ONJLVoqmafbM5Ihx6Q/lpsXsUTNBC/2n0D2gbeNdkUh/eio7+fnba/9q5+ELI94kBz+MqIvmsCmGuQ3KBIBX3Kf+eum0r3s4Ff1T6hUgfEuiKnWrIjaJdgHpq6+GwJazoEj6w+mAzi61NQYgGIIIUleeBOHiojpI0vBLOr5Dfe5mVSskS1ky+rIPr37Ud3xKS2Jm7D4OL159kR0yQwpzNkZ6YgcIbUcKri7DkT2rZnTCgIzGw2y2efuTttngNAwQ2WKV4CUKr+ailqP4uEma72XYYgRuz/VM+Nj+vjvyGQwkEUZdK+lm5caPiPrVs96KlmUNCK/yuwKFn0H61JnHb7azWaaWDsWXE6cGqc15zU1EoWjV9+RXpvrnbqAmTyyF4dSb2ZKTFyBQy6xK9e0HswUYSfXGfdP1yQeXOL5GZc6kwyotUrhwrN9KuPS9msUuMC7jYUn16jojRg3sAdMIYGd3mWKFT4mgnkJWzgwmrpt51F7yxKY2KFih/VeGZpf6qERXw==

> On 9. Feb 2019, at 18:20, Laurent Thery
> <laurent.thery AT inria.fr>
> wrote:
>
> Here is how you can solve "automatically" your 3 examples:
>

Very nice. Much appreciated, Gert

[Coq-Club] Automation for division over nat, Gert Smolka, 02/09/2019
- Re: [Coq-Club] Automation for division over nat, Laurent Thery, 02/09/2019
  - Re: [Coq-Club] Automation for division over nat, Bas Spitters, 02/09/2019
  - Re: [Coq-Club] Automation for division over nat, Gert Smolka, 02/09/2019