ssreflect - [ssreflect] Express a sum of reals

Subject: Ssreflect Users Discussion List

List archive

From: Edouard KLEIN <>
To:
Subject: [ssreflect] Express a sum of reals
Date: Fri, 15 Dec 2017 12:40:20 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
Ironport-phdr: 9a23:yf9/eRScxYHz/BIxvzoOFQFFctpsv+yvbD5Q0YIujvd0So/mwa6yZBaN2/xhgRfzUJnB7Loc0qyK6/mmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfa5+IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4KB2Rh/1kycHLyA2/33LisJziaJbrxyvpxt6w4HOYYGVMud1cqfTcN8GQGZMWNtaWS5cDYOmd4YAAOoPM+hboYfguVUBsQCzChOwCO710DJEmmP60K883u88EQ/GxgsgH9cWvXrbsdr1M7oSXvqvzKbV0D7NavVY1zj+5obQbxsspu+DUq93ccrM00YvDR7KjlaUqYP7PjOV0P8As2ee7+V6VOKvj3QrpB12ojiq38ohjJTCiIwSylDB7yp5wYA1KMW5SE5+bt6kDYFQuzuGOItxR8MvRXxjtiUiyrAep5K3YCwHxI4kyhPfcfCLbZWE7xP5WOqMIzp0mnRoc6+liRmo60iv0Oj8W9G00FlUqipFlcHBtnUX2BzS7siLU+J9/lu91TqW2QDf9+NJLV4umarULJ4hxbEwlp4NvkjZAiD2n0D2gLeXdkUi5Oeo9/zqbqv6qpKYLYN5iQHzPr4wlsCiAOk0KBUCUmqF9eik0b3s50z5QLFEjv0slanZtYjXKtoGqa6+Hg9ayJwj5Au8DzeiztsYnH8HIUlKeBKClYfpOlXOLOrkAve4hlSgiC1ryOzePr39HpXNKWDOkKz6fbZn9UFcxg4zws5D6JJIEbwBO/LyWkrptNPCFBM5Mgq0w/zmCNpnzI8eV3iPUeelN/bJqkWF6OYiKPWkYZQP/Tf7Mfksof/ol34w31EHLoez2p5CRXy/A/18Lw26RVfNpJ9VHGsNowMkQO/uhVyEeTFWbne2Gak742doW8qdEY7fS9X10/S61yChE8gNPm0=

Hi all !

I'm completely new to Coq and I'm trying to use the Koenig-Huygens Theorem in a proof (more specifically, this form:

From the book I see that I can make sets of finite types, but is it possible to express a set of reals ?

Thanks in advance,

Edouard.

[ssreflect] Express a sum of reals, Edouard KLEIN, 12/15/2017
- Re: [ssreflect] Express a sum of reals, Yves Bertot, 12/21/2017
  - Re: [ssreflect] Express a sum of reals, Yves Bertot, 12/21/2017
  - Re: [ssreflect] Express a sum of reals, Cyril, 12/21/2017