<!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.Appli.Fappli_rnd_odd</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library Flocq.Appli.Fappli_rnd_odd</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="lab23"></a><h1 class="section">Rounding to odd and its properties, including the equivalence</h1>
between rnd_NE and double rounding with rnd_odd and then rnd_NE
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore.html#"><span class="id" title="library">Fcore</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#"><span class="id" title="library">Fcalc_ops</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="Zrnd_odd"><span class="id" title="definition">Zrnd_odd</span></a> <span class="id" title="var">x</span> := <span class="id" title="keyword">match</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.RIneq.html#Req_EM_T"><span class="id" title="lemma">Req_EM_T</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#Zfloor"><span class="id" title="definition">Zfloor</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a>)) <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#left"><span class="id" title="constructor">left</span></a> <span class="id" title="var">_</span> ⇒ <a class="idref" href="Flocq.Core.Fcore_Raux.html#Zfloor"><span class="id" title="definition">Zfloor</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Specif.html#right"><span class="id" title="constructor">right</span></a> <span class="id" title="var">_</span> ⇒ <span class="id" title="keyword">match</span> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#Zfloor"><span class="id" title="definition">Zfloor</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a>)) <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> ⇒ <a class="idref" href="Flocq.Core.Fcore_Raux.html#Zceil"><span class="id" title="definition">Zceil</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> ⇒ <a class="idref" href="Flocq.Core.Fcore_Raux.html#Zfloor"><span class="id" title="definition">Zfloor</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a><br/>
<span class="id" title="keyword">end</span><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Global Instance</span> <a name="valid_rnd_odd"><span class="id" title="instance">valid_rnd_odd</span></a> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_rnd"><span class="id" title="class">Valid_rnd</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Zrnd_odd"><span class="id" title="definition">Zrnd_odd</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="Zrnd_odd_Zodd"><span class="id" title="lemma">Zrnd_odd_Zodd</span></a>: <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#Zfloor"><span class="id" title="definition">Zfloor</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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#32263a1c8b01baecdff9deb038955bc9"><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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> (<a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Zrnd_odd"><span class="id" title="definition">Zrnd_odd</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fcore_rnd_odd"><span class="id" title="section">Fcore_rnd_odd</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <span class="id" title="keyword">beta</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix"><span class="id" title="record">radix</span></a>.<br/>
<br/>
<span class="id" title="keyword">Notation</span> <a name="bpow"><span class="id" title="abbreviation">bpow</span></a> <span class="id" title="var">e</span> := (<a class="idref" href="Flocq.Core.Fcore_Raux.html#bpow"><span class="id" title="definition">bpow</span></a> <span class="id" title="keyword">beta</span> <span class="id" title="var">e</span>).<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fcore_rnd_odd.fexp"><span class="id" title="variable">fexp</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</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.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<br/>
<span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_exp</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_exp"><span class="id" title="class">Valid_exp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Fcore_rnd_odd.fexp"><span class="id" title="variable">fexp</span></a> }.<br/>
<span class="id" title="keyword">Context</span> { <span class="id" title="var">exists_NE_</span> : <a class="idref" href="Flocq.Core.Fcore_rnd_ne.html#Exists_NE"><span class="id" title="class">Exists_NE</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Fcore_rnd_odd.fexp"><span class="id" title="variable">fexp</span></a> }.<br/>
<br/>
<span class="id" title="keyword">Notation</span> <a name="format"><span class="id" title="abbreviation">format</span></a> := (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Fcore_rnd_odd.fexp"><span class="id" title="variable">fexp</span></a>).<br/>
<span class="id" title="keyword">Notation</span> <a name="canonic"><span class="id" title="abbreviation">canonic</span></a> := (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#canonic"><span class="id" title="definition">canonic</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Fcore_rnd_odd.fexp"><span class="id" title="variable">fexp</span></a>).<br/>
<span class="id" title="keyword">Notation</span> <a name="cexp"><span class="id" title="abbreviation">cexp</span></a> := (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#canonic_exp"><span class="id" title="definition">canonic_exp</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Fcore_rnd_odd.fexp"><span class="id" title="variable">fexp</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="Rnd_odd_pt"><span class="id" title="definition">Rnd_odd_pt</span></a> (<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.Appli.Fappli_rnd_odd.html#format"><span class="id" title="abbreviation">format</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">(</span></a>(<a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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.Appli.Fappli_rnd_odd.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#7a45dffb109c3069e5c675be68643e60"><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="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><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.Appli.Fappli_rnd_odd.html#format"><span class="id" title="abbreviation">format</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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.Appli.Fappli_rnd_odd.html#format"><span class="id" title="abbreviation">format</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">g</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#canonic"><span class="id" title="abbreviation">canonic</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Fnum"><span class="id" title="projection">Fnum</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</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#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">)</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="Rnd_odd"><span class="id" title="definition">Rnd_odd</span></a> (<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/>
<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.Appli.Fappli_rnd_odd.html#Rnd_odd_pt"><span class="id" title="definition">Rnd_odd_pt</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#rnd"><span class="id" title="variable">rnd</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_odd_pt_sym"><span class="id" title="lemma">Rnd_odd_pt_sym</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="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.Appli.Fappli_rnd_odd.html#Rnd_odd_pt"><span class="id" title="definition">Rnd_odd_pt</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.Appli.Fappli_rnd_odd.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.Appli.Fappli_rnd_odd.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.Appli.Fappli_rnd_odd.html#Rnd_odd_pt"><span class="id" title="definition">Rnd_odd_pt</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#f"><span class="id" title="variable">f</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="round_odd_opp"><span class="id" title="lemma">round_odd_opp</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Fcore_rnd_odd.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Zrnd_odd"><span class="id" title="definition">Zrnd_odd</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.Appli.Fappli_rnd_odd.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.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_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Fcore_rnd_odd.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Zrnd_odd"><span class="id" title="definition">Zrnd_odd</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="round_odd_pt"><span class="id" title="lemma">round_odd_pt</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
<a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Rnd_odd_pt"><span class="id" title="definition">Rnd_odd_pt</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Fcore_rnd_odd.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Zrnd_odd"><span class="id" title="definition">Zrnd_odd</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_odd_pt_unicity"><span class="id" title="lemma">Rnd_odd_pt_unicity</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.Appli.Fappli_rnd_odd.html#Rnd_odd_pt"><span class="id" title="definition">Rnd_odd_pt</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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.Appli.Fappli_rnd_odd.html#Rnd_odd_pt"><span class="id" title="definition">Rnd_odd_pt</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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.Appli.Fappli_rnd_odd.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.Appli.Fappli_rnd_odd.html#f2"><span class="id" title="variable">f2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Rnd_odd_pt_monotone"><span class="id" title="lemma">Rnd_odd_pt_monotone</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.Appli.Fappli_rnd_odd.html#Rnd_odd_pt"><span class="id" title="definition">Rnd_odd_pt</span></a>).<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Fcore_rnd_odd"><span class="id" title="section">Fcore_rnd_odd</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Odd_prop_aux"><span class="id" title="section">Odd_prop_aux</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <span class="id" title="keyword">beta</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix"><span class="id" title="record">radix</span></a>.<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="Odd_prop_aux.Even_beta"><span class="id" title="variable">Even_beta</span></a>: <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix_val"><span class="id" title="projection">radix_val</span></a> <span class="id" title="keyword">beta</span>)<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.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<br/>
<span class="id" title="keyword">Notation</span> <a name="bpow"><span class="id" title="abbreviation">bpow</span></a> <span class="id" title="var">e</span> := (<a class="idref" href="Flocq.Core.Fcore_Raux.html#bpow"><span class="id" title="definition">bpow</span></a> <span class="id" title="keyword">beta</span> <span class="id" title="var">e</span>).<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</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.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<span class="id" title="keyword">Variable</span> <a name="Odd_prop_aux.fexpe"><span class="id" title="variable">fexpe</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</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.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<br/>
<span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_exp</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_exp"><span class="id" title="class">Valid_exp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> }.<br/>
<span class="id" title="keyword">Context</span> { <span class="id" title="var">exists_NE_</span> : <a class="idref" href="Flocq.Core.Fcore_rnd_ne.html#Exists_NE"><span class="id" title="class">Exists_NE</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> }. <span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_expe</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_exp"><span class="id" title="class">Valid_exp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexpe"><span class="id" title="variable">fexpe</span></a> }.<br/>
<span class="id" title="keyword">Context</span> { <span class="id" title="var">exists_NE_e</span> : <a class="idref" href="Flocq.Core.Fcore_rnd_ne.html#Exists_NE"><span class="id" title="class">Exists_NE</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexpe"><span class="id" title="variable">fexpe</span></a> }.
<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="Odd_prop_aux.fexpe_fexp"><span class="id" title="variable">fexpe_fexp</span></a>: <span class="id" title="keyword">∀</span> <span class="id" title="var">e</span>, (<a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexpe"><span class="id" title="variable">fexpe</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a>2)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="generic_format_fexpe_fexp"><span class="id" title="lemma">generic_format_fexpe_fexp</span></a>: <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexpe"><span class="id" title="variable">fexpe</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="exists_even_fexp_lt"><span class="id" title="lemma">exists_even_fexp_lt</span></a>: <span class="id" title="keyword">∀</span> (<span class="id" title="var">c</span>:<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</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.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</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>),<br/>
<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#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">f</span>:<a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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.Appli.Fappli_rnd_odd.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#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> (<a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#c"><span class="id" title="variable">c</span></a> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#Fexp"><span class="id" title="projection">Fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#f"><span class="id" title="variable">f</span></a>)%<span class="id" title="var">Z</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="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#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">f</span>:<a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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.Appli.Fappli_rnd_odd.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#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#canonic"><span class="id" title="definition">canonic</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#c"><span class="id" title="variable">c</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Fnum"><span class="id" title="projection">Fnum</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Odd_prop_aux.choice"><span class="id" title="variable">choice</span></a>:<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</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.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<span class="id" title="keyword">Variable</span> <a name="Odd_prop_aux.x"><span class="id" title="variable">x</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/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Odd_prop_aux.d"><span class="id" title="variable">d</span></a> <a name="Odd_prop_aux.u"><span class="id" title="variable">u</span></a>: <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>.<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="Odd_prop_aux.Hd"><span class="id" title="variable">Hd</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_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a>) <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.d"><span class="id" title="variable">d</span></a>).<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="Odd_prop_aux.Cd"><span class="id" title="variable">Cd</span></a>: <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#canonic"><span class="id" title="definition">canonic</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.d"><span class="id" title="variable">d</span></a>.<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="Odd_prop_aux.Hu"><span class="id" title="variable">Hu</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_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a>) <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.u"><span class="id" title="variable">u</span></a>).<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="Odd_prop_aux.Cu"><span class="id" title="variable">Cu</span></a>: <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#canonic"><span class="id" title="definition">canonic</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.u"><span class="id" title="variable">u</span></a>.<br/>
<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="Odd_prop_aux.xPos"><span class="id" title="variable">xPos</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.Appli.Fappli_rnd_odd.html#Odd_prop_aux.x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Let</span> <a name="Odd_prop_aux.m"><span class="id" title="variable">m</span></a>:= (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0c0207ff801f7c795ce431f130ae670a"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.d"><span class="id" title="variable">d</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a><a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.u"><span class="id" title="variable">u</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0c0207ff801f7c795ce431f130ae670a"><span class="id" title="notation">)/</span></a>2)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="d_eq"><span class="id" title="lemma">d_eq</span></a>: <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.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_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Core.Fcore_Raux.html#Zfloor"><span class="id" title="definition">Zfloor</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="u_eq"><span class="id" title="lemma">u_eq</span></a>: <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.u"><span class="id" title="variable">u</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_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Core.Fcore_Raux.html#Zceil"><span class="id" title="definition">Zceil</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="d_ge_0"><span class="id" title="lemma">d_ge_0</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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.d"><span class="id" title="variable">d</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="ln_beta_d"><span class="id" title="lemma">ln_beta_d</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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.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.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.d"><span class="id" title="variable">d</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</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/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="Fexp_d"><span class="id" title="lemma">Fexp_d</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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.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> <a class="idref" href="Flocq.Core.Fcore_defs.html#Fexp"><span class="id" title="projection">Fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.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.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.x"><span class="id" title="variable">x</span></a>).<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="format_bpow_x"><span class="id" title="lemma">format_bpow_x</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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.d"><span class="id" title="variable">d</span></a>)%<span class="id" title="var">R</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> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.x"><span class="id" title="variable">x</span></a>)).<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="format_bpow_d"><span class="id" title="lemma">format_bpow_d</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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.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_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.d"><span class="id" title="variable">d</span></a>))).<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="d_le_m"><span class="id" title="lemma">d_le_m</span></a>: (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.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.Appli.Fappli_rnd_odd.html#Odd_prop_aux.m"><span class="id" title="variable">m</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="m_le_u"><span class="id" title="lemma">m_le_u</span></a>: (<a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.m"><span class="id" title="variable">m</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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.u"><span class="id" title="variable">u</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="ln_beta_m"><span class="id" title="lemma">ln_beta_m</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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.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> <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_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a><a class="idref" href="Flocq.Core.Fcore_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.d"><span class="id" title="variable">d</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</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/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="ln_beta_m_0"><span class="id" title="lemma">ln_beta_m_0</span></a>: (0 <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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.d"><span class="id" title="variable">d</span></a>)%<span class="id" title="var">R</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> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a><a class="idref" href="Flocq.Core.Fcore_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.u"><span class="id" title="variable">u</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a>1<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="u'_eq"><span class="id" title="lemma">u'_eq</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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.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> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">f</span>:<a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Fexp"><span class="id" title="projection">Fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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_defs.html#Fexp"><span class="id" title="projection">Fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.d"><span class="id" title="variable">d</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="m_eq"><span class="id" title="lemma">m_eq</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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.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> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">f</span>:<a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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.Appli.Fappli_rnd_odd.html#Odd_prop_aux.m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Fexp"><span class="id" title="projection">Fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a>1)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="m_eq_0"><span class="id" title="lemma">m_eq_0</span></a>: (0 <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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.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> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">f</span>:<a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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.Appli.Fappli_rnd_odd.html#Odd_prop_aux.m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Fexp"><span class="id" title="projection">Fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.u"><span class="id" title="variable">u</span></a>)) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a>1)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="fexp_m_eq_0"><span class="id" title="lemma">fexp_m_eq_0</span></a>: (0 <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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.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.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.u"><span class="id" title="variable">u</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a>1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#ln_beta"><span class="id" title="definition">ln_beta</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.u"><span class="id" title="variable">u</span></a>))<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a>1)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="Fm"><span class="id" title="lemma">Fm</span></a>: <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexpe"><span class="id" title="variable">fexpe</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.m"><span class="id" title="variable">m</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="Zm"><span class="id" title="lemma">Zm</span></a>:<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">g</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#canonic"><span class="id" title="definition">canonic</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexpe"><span class="id" title="variable">fexpe</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Fnum"><span class="id" title="projection">Fnum</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="DN_odd_d_aux"><span class="id" title="lemma">DN_odd_d_aux</span></a>: <span class="id" title="keyword">∀</span> <span class="id" title="var">z</span>, (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.d"><span class="id" title="variable">d</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#ed7870e49208be293c8dbcf28a708f81"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#ed7870e49208be293c8dbcf28a708f81"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.u"><span class="id" title="variable">u</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_DN_pt"><span class="id" title="definition">Rnd_DN_pt</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a>) <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#z"><span class="id" title="variable">z</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.d"><span class="id" title="variable">d</span></a>).<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="UP_odd_d_aux"><span class="id" title="lemma">UP_odd_d_aux</span></a>: <span class="id" title="keyword">∀</span> <span class="id" title="var">z</span>, (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.d"><span class="id" title="variable">d</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#eef1acbd63cc280f97a2bde070d0def7"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#eef1acbd63cc280f97a2bde070d0def7"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.u"><span class="id" title="variable">u</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_UP_pt"><span class="id" title="definition">Rnd_UP_pt</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a>) <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#z"><span class="id" title="variable">z</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.u"><span class="id" title="variable">u</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="round_odd_prop_pos"><span class="id" title="lemma">round_odd_prop_pos</span></a>:<br/>
<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.choice"><span class="id" title="variable">choice</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexpe"><span class="id" title="variable">fexpe</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Zrnd_odd"><span class="id" title="definition">Zrnd_odd</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.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><br/>
<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux.x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop_aux"><span class="id" title="section">Odd_prop_aux</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Odd_prop"><span class="id" title="section">Odd_prop</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <span class="id" title="keyword">beta</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix"><span class="id" title="record">radix</span></a>.<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="Odd_prop.Even_beta"><span class="id" title="variable">Even_beta</span></a>: <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix_val"><span class="id" title="projection">radix_val</span></a> <span class="id" title="keyword">beta</span>)<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.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Odd_prop.fexp"><span class="id" title="variable">fexp</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</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.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<span class="id" title="keyword">Variable</span> <a name="Odd_prop.fexpe"><span class="id" title="variable">fexpe</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</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.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<span class="id" title="keyword">Variable</span> <a name="Odd_prop.choice"><span class="id" title="variable">choice</span></a>:<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</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.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/>
<br/>
<span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_exp</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_exp"><span class="id" title="class">Valid_exp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop.fexp"><span class="id" title="variable">fexp</span></a> }.<br/>
<span class="id" title="keyword">Context</span> { <span class="id" title="var">exists_NE_</span> : <a class="idref" href="Flocq.Core.Fcore_rnd_ne.html#Exists_NE"><span class="id" title="class">Exists_NE</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop.fexp"><span class="id" title="variable">fexp</span></a> }. <span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_expe</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_exp"><span class="id" title="class">Valid_exp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop.fexpe"><span class="id" title="variable">fexpe</span></a> }.<br/>
<span class="id" title="keyword">Context</span> { <span class="id" title="var">exists_NE_e</span> : <a class="idref" href="Flocq.Core.Fcore_rnd_ne.html#Exists_NE"><span class="id" title="class">Exists_NE</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop.fexpe"><span class="id" title="variable">fexpe</span></a> }.
<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="Odd_prop.fexpe_fexp"><span class="id" title="variable">fexpe_fexp</span></a>: <span class="id" title="keyword">∀</span> <span class="id" title="var">e</span>, (<a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop.fexpe"><span class="id" title="variable">fexpe</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a>2)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="canonizer"><span class="id" title="lemma">canonizer</span></a>: <span class="id" title="keyword">∀</span> <span class="id" title="var">f</span>, <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#f"><span class="id" title="variable">f</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> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">g</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#canonic"><span class="id" title="definition">canonic</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#g"><span class="id" title="variable">g</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="round_odd_prop"><span class="id" title="lemma">round_odd_prop</span></a>: <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop.choice"><span class="id" title="variable">choice</span></a>) (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop.fexpe"><span class="id" title="variable">fexpe</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Zrnd_odd"><span class="id" title="definition">Zrnd_odd</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.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><br/>
<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop.choice"><span class="id" title="variable">choice</span></a>) <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Appli.Fappli_rnd_odd.html#Odd_prop"><span class="id" title="section">Odd_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
>
75
