<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<title>Flocq.Core.Fcore_rnd</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library Flocq.Core.Fcore_rnd</h1>
<div class="code">
</div>
<div class="doc">
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
<div class="paragraph"> </div>
Copyright (C) 2010-2013 Sylvie Boldo
<br />
Copyright (C) 2010-2013 Guillaume Melquiond
<div class="paragraph"> </div>
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
<div class="paragraph"> </div>
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
<div class="paragraph"> </div>
<a name="lab9"></a><h1 class="section">Roundings: properties and/or functions</h1>
</div>
<div class="code">
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore_Raux.html#"><span class="id" title="library">Fcore_Raux</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore_defs.html#"><span class="id" title="library">Fcore_defs</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="RND_prop"><span class="id" title="section">RND_prop</span></a>.<br/>
<br/>
<span class="id" title="keyword">Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">R_scope</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="round_val_of_pred"><span class="id" title="lemma">round_val_of_pred</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">rnd</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred"><span class="id" title="definition">round_pred</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">{</span></a> <span class="id" title="var">f</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">f</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">}</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="round_fun_of_pred"><span class="id" title="lemma">round_fun_of_pred</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">rnd</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred"><span class="id" title="definition">round_pred</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">{</span></a> <span class="id" title="var">f</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> (<span class="id" title="var">f</span> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">}</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="round_unicity"><span class="id" title="lemma">round_unicity</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">rnd</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred_monotone"><span class="id" title="definition">round_pred_monotone</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f2"><span class="id" title="variable">f2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f2"><span class="id" title="variable">f2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_DN_pt_monotone"><span class="id" title="lemma">Rnd_DN_pt_monotone</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred_monotone"><span class="id" title="definition">round_pred_monotone</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_DN_pt_unicity"><span class="id" title="lemma">Rnd_DN_pt_unicity</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f2"><span class="id" title="variable">f2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f2"><span class="id" title="variable">f2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_DN_unicity"><span class="id" title="lemma">Rnd_DN_unicity</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">rnd1</span> <span class="id" title="var">rnd2</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN"><span class="id" title="definition">Rnd_DN</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd1"><span class="id" title="variable">rnd1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN"><span class="id" title="definition">Rnd_DN</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd2"><span class="id" title="variable">rnd2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd1"><span class="id" title="variable">rnd1</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd2"><span class="id" title="variable">rnd2</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_UP_pt_monotone"><span class="id" title="lemma">Rnd_UP_pt_monotone</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred_monotone"><span class="id" title="definition">round_pred_monotone</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_UP_pt_unicity"><span class="id" title="lemma">Rnd_UP_pt_unicity</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f2"><span class="id" title="variable">f2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f2"><span class="id" title="variable">f2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_UP_unicity"><span class="id" title="lemma">Rnd_UP_unicity</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">rnd1</span> <span class="id" title="var">rnd2</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP"><span class="id" title="definition">Rnd_UP</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd1"><span class="id" title="variable">rnd1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP"><span class="id" title="definition">Rnd_UP</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd2"><span class="id" title="variable">rnd2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd1"><span class="id" title="variable">rnd1</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd2"><span class="id" title="variable">rnd2</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_DN_UP_pt_sym"><span class="id" title="lemma">Rnd_DN_UP_pt_sym</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_UP_DN_pt_sym"><span class="id" title="lemma">Rnd_UP_DN_pt_sym</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_DN_UP_sym"><span class="id" title="lemma">Rnd_DN_UP_sym</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">rnd1</span> <span class="id" title="var">rnd2</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN"><span class="id" title="definition">Rnd_DN</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd1"><span class="id" title="variable">rnd1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP"><span class="id" title="definition">Rnd_UP</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd2"><span class="id" title="variable">rnd2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd1"><span class="id" title="variable">rnd1</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd2"><span class="id" title="variable">rnd2</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_DN_UP_pt_split"><span class="id" title="lemma">Rnd_DN_UP_pt_split</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">d</span> <span class="id" title="var">u</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">f</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">)</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_DN_pt_refl"><span class="id" title="lemma">Rnd_DN_pt_refl</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_DN_pt_idempotent"><span class="id" title="lemma">Rnd_DN_pt_idempotent</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_UP_pt_refl"><span class="id" title="lemma">Rnd_UP_pt_refl</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_UP_pt_idempotent"><span class="id" title="lemma">Rnd_UP_pt_idempotent</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Only_DN_or_UP"><span class="id" title="lemma">Only_DN_or_UP</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">fd</span> <span class="id" title="var">fu</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#fd"><span class="id" title="variable">fd</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#fu"><span class="id" title="variable">fu</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (<a class="idref" href="Flocq.Core.Fcore_rnd.html#fd"><span class="id" title="variable">fd</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#777fa820f32591f17d50731841113fa3"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#777fa820f32591f17d50731841113fa3"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#fu"><span class="id" title="variable">fu</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#fd"><span class="id" title="variable">fd</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#fu"><span class="id" title="variable">fu</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_ZR_abs"><span class="id" title="lemma">Rnd_ZR_abs</span></a> :<br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>) (<span class="id" title="var">rnd</span>: <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>),<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_ZR"><span class="id" title="definition">Rnd_ZR</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>, (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_ZR_pt_monotone"><span class="id" title="lemma">Rnd_ZR_pt_monotone</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred_monotone"><span class="id" title="definition">round_pred_monotone</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_ZR_pt"><span class="id" title="definition">Rnd_ZR_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_N_pt_DN_or_UP"><span class="id" title="lemma">Rnd_N_pt_DN_or_UP</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_N_pt_DN_or_UP_eq"><span class="id" title="lemma">Rnd_N_pt_DN_or_UP_eq</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">fd</span> <span class="id" title="var">fu</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#fd"><span class="id" title="variable">fd</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#fu"><span class="id" title="variable">fu</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#fd"><span class="id" title="variable">fd</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#fu"><span class="id" title="variable">fu</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_N_pt_sym"><span class="id" title="lemma">Rnd_N_pt_sym</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_N_pt_monotone"><span class="id" title="lemma">Rnd_N_pt_monotone</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">f</span> <span class="id" title="var">g</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#g"><span class="id" title="variable">g</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_N_pt_unicity"><span class="id" title="lemma">Rnd_N_pt_unicity</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">d</span> <span class="id" title="var">u</span> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f2"><span class="id" title="variable">f2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f2"><span class="id" title="variable">f2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_N_pt_refl"><span class="id" title="lemma">Rnd_N_pt_refl</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_N_pt_idempotent"><span class="id" title="lemma">Rnd_N_pt_idempotent</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_N_pt_0"><span class="id" title="lemma">Rnd_N_pt_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> 0 0.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_N_pt_pos"><span class="id" title="lemma">Rnd_N_pt_pos</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span>, 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_N_pt_neg"><span class="id" title="lemma">Rnd_N_pt_neg</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> 0.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_N_pt_abs"><span class="id" title="lemma">Rnd_N_pt_abs</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_DN_UP_pt_N"><span class="id" title="lemma">Rnd_DN_UP_pt_N</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">d</span> <span class="id" title="var">u</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_DN_pt_N"><span class="id" title="lemma">Rnd_DN_pt_N</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">d</span> <span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_UP_pt_N"><span class="id" title="lemma">Rnd_UP_pt_N</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">d</span> <span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="Rnd_NG_pt_unicity_prop"><span class="id" title="definition">Rnd_NG_pt_unicity_prop</span></a> <span class="id" title="var">F</span> <span class="id" title="var">P</span> :=<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">d</span> <span class="id" title="var">u</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_NG_pt_unicity"><span class="id" title="lemma">Rnd_NG_pt_unicity</span></a> :<br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>) (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>),<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#Rnd_NG_pt_unicity_prop"><span class="id" title="definition">Rnd_NG_pt_unicity_prop</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NG_pt"><span class="id" title="definition">Rnd_NG_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NG_pt"><span class="id" title="definition">Rnd_NG_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f2"><span class="id" title="variable">f2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f2"><span class="id" title="variable">f2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_NG_pt_monotone"><span class="id" title="lemma">Rnd_NG_pt_monotone</span></a> :<br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>) (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>),<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#Rnd_NG_pt_unicity_prop"><span class="id" title="definition">Rnd_NG_pt_unicity_prop</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred_monotone"><span class="id" title="definition">round_pred_monotone</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NG_pt"><span class="id" title="definition">Rnd_NG_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_NG_pt_refl"><span class="id" title="lemma">Rnd_NG_pt_refl</span></a> :<br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>) (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>),<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NG_pt"><span class="id" title="definition">Rnd_NG_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_NG_pt_sym"><span class="id" title="lemma">Rnd_NG_pt_sym</span></a> :<br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>) (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>),<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NG_pt"><span class="id" title="definition">Rnd_NG_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NG_pt"><span class="id" title="definition">Rnd_NG_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_NG_unicity"><span class="id" title="lemma">Rnd_NG_unicity</span></a> :<br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>) (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>),<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#Rnd_NG_pt_unicity_prop"><span class="id" title="definition">Rnd_NG_pt_unicity_prop</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">rnd1</span> <span class="id" title="var">rnd2</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NG"><span class="id" title="definition">Rnd_NG</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd1"><span class="id" title="variable">rnd1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NG"><span class="id" title="definition">Rnd_NG</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd2"><span class="id" title="variable">rnd2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd1"><span class="id" title="variable">rnd1</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd2"><span class="id" title="variable">rnd2</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_NA_NG_pt"><span class="id" title="lemma">Rnd_NA_NG_pt</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NA_pt"><span class="id" title="definition">Rnd_NA_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">↔</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NG_pt"><span class="id" title="definition">Rnd_NG_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_NA_pt_unicity_prop"><span class="id" title="lemma">Rnd_NA_pt_unicity_prop</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#Rnd_NG_pt_unicity_prop"><span class="id" title="definition">Rnd_NG_pt_unicity_prop</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> ⇒ (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#b"><span class="id" title="variable">b</span></a>)%<span class="id" title="var">R</span>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_NA_pt_unicity"><span class="id" title="lemma">Rnd_NA_pt_unicity</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NA_pt"><span class="id" title="definition">Rnd_NA_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NA_pt"><span class="id" title="definition">Rnd_NA_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f2"><span class="id" title="variable">f2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f2"><span class="id" title="variable">f2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_NA_N_pt"><span class="id" title="lemma">Rnd_NA_N_pt</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_N_pt"><span class="id" title="definition">Rnd_N_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NA_pt"><span class="id" title="definition">Rnd_NA_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_NA_unicity"><span class="id" title="lemma">Rnd_NA_unicity</span></a> :<br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>),<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">rnd1</span> <span class="id" title="var">rnd2</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NA"><span class="id" title="definition">Rnd_NA</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd1"><span class="id" title="variable">rnd1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NA"><span class="id" title="definition">Rnd_NA</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd2"><span class="id" title="variable">rnd2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd1"><span class="id" title="variable">rnd1</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#rnd2"><span class="id" title="variable">rnd2</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_NA_pt_monotone"><span class="id" title="lemma">Rnd_NA_pt_monotone</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred_monotone"><span class="id" title="definition">round_pred_monotone</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NA_pt"><span class="id" title="definition">Rnd_NA_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_NA_pt_refl"><span class="id" title="lemma">Rnd_NA_pt_refl</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NA_pt"><span class="id" title="definition">Rnd_NA_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_NA_pt_idempotent"><span class="id" title="lemma">Rnd_NA_pt_idempotent</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NA_pt"><span class="id" title="definition">Rnd_NA_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="round_pred_ge_0"><span class="id" title="lemma">round_pred_ge_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred_monotone"><span class="id" title="definition">round_pred_monotone</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> 0 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="round_pred_gt_0"><span class="id" title="lemma">round_pred_gt_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred_monotone"><span class="id" title="definition">round_pred_monotone</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> 0 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="round_pred_le_0"><span class="id" title="lemma">round_pred_le_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred_monotone"><span class="id" title="definition">round_pred_monotone</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> 0 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> 0.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="round_pred_lt_0"><span class="id" title="lemma">round_pred_lt_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred_monotone"><span class="id" title="definition">round_pred_monotone</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> 0 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> 0.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_DN_pt_equiv_format"><span class="id" title="lemma">Rnd_DN_pt_equiv_format</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F1</span> <span class="id" title="var">F2</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#777fa820f32591f17d50731841113fa3"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#777fa820f32591f17d50731841113fa3"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">↔</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#777fa820f32591f17d50731841113fa3"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#777fa820f32591f17d50731841113fa3"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_UP_pt_equiv_format"><span class="id" title="lemma">Rnd_UP_pt_equiv_format</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F1</span> <span class="id" title="var">F2</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#777fa820f32591f17d50731841113fa3"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#777fa820f32591f17d50731841113fa3"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">↔</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">f</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#777fa820f32591f17d50731841113fa3"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#777fa820f32591f17d50731841113fa3"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#f"><span class="id" title="variable">f</span></a>.<br/>
<br/>
</div>
<div class="doc">
ensures a real number can always be rounded
</div>
<div class="code">
<span class="id" title="keyword">Inductive</span> <a name="satisfies_any"><span class="id" title="inductive">satisfies_any</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>) :=<br/>
<a name="Satisfies_any"><span class="id" title="constructor">Satisfies_any</span></a> :<br/>
<span class="id" title="var">F</span> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a>, <span class="id" title="var">F</span> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="var">F</span> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0575b33c544988081e4e30ee15f09d84"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred_total"><span class="id" title="definition">round_pred_total</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <span class="id" title="var">F</span>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#satisfies_any"><span class="id" title="inductive">satisfies_any</span></a> <span class="id" title="var">F</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="satisfies_any_eq"><span class="id" title="lemma">satisfies_any_eq</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F1</span> <span class="id" title="var">F2</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_rnd.html#F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">↔</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#satisfies_any"><span class="id" title="inductive">satisfies_any</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#satisfies_any"><span class="id" title="inductive">satisfies_any</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F2"><span class="id" title="variable">F2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="satisfies_any_imp_DN"><span class="id" title="lemma">satisfies_any_imp_DN</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#satisfies_any"><span class="id" title="inductive">satisfies_any</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred"><span class="id" title="definition">round_pred</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="satisfies_any_imp_UP"><span class="id" title="lemma">satisfies_any_imp_UP</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#satisfies_any"><span class="id" title="inductive">satisfies_any</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred"><span class="id" title="definition">round_pred</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="satisfies_any_imp_ZR"><span class="id" title="lemma">satisfies_any_imp_ZR</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#satisfies_any"><span class="id" title="inductive">satisfies_any</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred"><span class="id" title="definition">round_pred</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_ZR_pt"><span class="id" title="definition">Rnd_ZR_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="NG_existence_prop"><span class="id" title="definition">NG_existence_prop</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>) (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>) :=<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">d</span> <span class="id" title="var">u</span>, <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#611abc97cba304de784fa909dbdea1fa"><span class="id" title="notation">¬</span></a><a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#d"><span class="id" title="variable">d</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="satisfies_any_imp_NG"><span class="id" title="lemma">satisfies_any_imp_NG</span></a> :<br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>) (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>),<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#satisfies_any"><span class="id" title="inductive">satisfies_any</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#NG_existence_prop"><span class="id" title="definition">NG_existence_prop</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred_total"><span class="id" title="definition">round_pred_total</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NG_pt"><span class="id" title="definition">Rnd_NG_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#P"><span class="id" title="variable">P</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="satisfies_any_imp_NA"><span class="id" title="lemma">satisfies_any_imp_NA</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">F</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_rnd.html#satisfies_any"><span class="id" title="inductive">satisfies_any</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#round_pred"><span class="id" title="definition">round_pred</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Rnd_NA_pt"><span class="id" title="definition">Rnd_NA_pt</span></a> <a class="idref" href="Flocq.Core.Fcore_rnd.html#F"><span class="id" title="variable">F</span></a>).<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_rnd.html#RND_prop"><span class="id" title="section">RND_prop</span></a>.<br/>
</div>
</div>
<div id="footer">
<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>
distrib
>
Mageia
>
6
>
armv5tl
>
media
>
core-release
>
by-pkgid
>
3c7997fe0e8405f6d7b5563e63d17a78
>
files
>
93
