coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] cases in leq proof

From: Patricia Peratto <psperatto AT vera.com.uy>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] cases in leq proof
Date: Tue, 22 Dec 2020 17:16:17 -0300 (UYT)
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mail.vera.com.uy
Dkim-filter: OpenDKIM Filter v2.9.0 mta04.in.vera.com.uy 33CF6222E07
Ironport-phdr: 9a23:GK0+xRW/rZCuTy8PkQex7K1X45PV8LGtZVwlr6E/grcLSJyIuqrYbBaCt8tkgFKBZ4jH8fUM07OQ7/m/HzZYvd3Y6i1KWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sAfcutMIjYd+Jas9xQbFrmVIdu9L2W5mOFWfkgrm6Myt5pBj6SNQu/wg985ET6r3erkzQKJbAjo7LW07/dXnuhbfQwSB4HscSXgWnQFTAwfZ9hH6X4z+vTX8u+FgxSSVJ8z2TbQzWTS/86dmTQLjhSkbOzIl9mzcl8p9h79Zrh28vRxy24DaboGLOvR9fKzdc84USmVdUcZQSyxMGZmzY5cTAOUaIepUs4vwql0TphW+HwmsA+bvxydSiHDswa06yeUhHh3H3AM6AtkAqmrbrM/vO6cOTeC1y7TDwDLbb/NNwTfy9pLIfQo9ofGQWrJ9atTRxlc1FwzflFmftYvlPzaP2uQQs2mW9uxtXv+ghGA7sQ9+uCSvxtsyhYnTgIIY0l/J+Cp7zYg6JNC2SFN3bcCkHpZQsyyXNoh7T8MmTm9opCs0xL4LtYCmcCUO1JkqxR/SZvyHfYWI/h7uW/udLCp+iXl4e7y/nw6//Va8xuHgTMW530pGojBLn9XRrHwA2Bze5tCaRvZ/4EutwyiD2g/J5uxKPEw4j6TWJ4Mnz7UtjJQcq17DETXzmEjujK+ZaEEk+u+w5uTieLrmp5ucO5Vqig7gKKQhgNazDvg/MggLRWSb5OS92KXi/U3/XrpKkuU7nrfFvJzGP8gWqbK1DxVb34o+8RqyADer3MwdnXYdLVJFfByHj5LuO1HLOP34Fey/g0yynzdx3f/GIqHhApLWI3jdjrjhZ6xy51RAxwo0yNBT/Y9UC7EZLPLpRkDxrMDYDgM+MwGs3+nnD8x92poCVmKLH6+WK7jfsUSI5+IqO+mDfpUZuDf7K/g/5v7hl2U1mVEHffrh4ZxCY3ehW/9iPk+xYHz2g95HH31ZkBA5SbnSgUGYUDVSbj6KUrg1+i08QNa+Fp/OXImxnLupwiqhF9tdYWUAF0HaQiSgTJmNR/pZMHHaGcRmiDFRDeH9Gb9k7gmnsUrB85QiNvDdo3ZKq5/53Z5+4OiViABgrWUlXfTY6HmESiRPpk1NQjY32K5lpkkkkQWd3LJxxfdfEJpO9qEQC1poBdvn1+V/TuvKdEfBc9OOEQb0R9ynBXcvQ8g4hdQJZgBgCof6gw==

I want to prove:

Theorem le_to_exist (n m:nat)(p:le (S n) m):
exists_prop nat
(fun (k:nat)=>add (S k) n = m).

Patricia

De: "Patricia Peratto" <psperatto AT vera.com.uy>
Para: "coq-club" <coq-club AT inria.fr>
Enviados: Martes, 22 de Diciembre 2020 17:04:08
Asunto: [Coq-Club] cases in leq proof

Is there some way to make a case analisis over a proof

of a leq proposition?

Regards,

Patricia

[Coq-Club] cases in leq proof, Patricia Peratto, 12/22/2020
- Re: [Coq-Club] cases in leq proof, Adam Chlipala, 12/22/2020
- Re: [Coq-Club] cases in leq proof, Patricia Peratto, 12/22/2020
  - Re: [Coq-Club] cases in leq proof, Adam Chlipala, 12/22/2020
    - Re: [Coq-Club] cases in leq proof, Robbert Krebbers, 12/22/2020
    - Re: [Coq-Club] cases in leq proof, Patricia Peratto, 12/22/2020
      - Re: [Coq-Club] cases in leq proof, Dominique Larchey-Wendling, 12/23/2020
      - Re: [Coq-Club] cases in leq proof, Castéran Pierre, 12/23/2020