<!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.Calc.Fcalc_bracket</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library Flocq.Calc.Fcalc_bracket</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="lab12"></a><h1 class="section">Locations: where a real number is positioned with respect to its rounded-down value in an arbitrary format.</h1>
</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_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/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore_float_prop.html#"><span class="id" title="library">Fcore_float_prop</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fcalc_bracket"><span class="id" title="section">Fcalc_bracket</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fcalc_bracket.d"><span class="id" title="variable">d</span></a> <a name="Fcalc_bracket.u"><span class="id" title="variable">u</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">Hypothesis</span> <a name="Fcalc_bracket.Hdu"><span class="id" title="variable">Hdu</span></a> : (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.d"><span class="id" title="variable">d</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.Calc.Fcalc_bracket.html#Fcalc_bracket.u"><span class="id" title="variable">u</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Inductive</span> <a name="location"><span class="id" title="inductive">location</span></a> := <a name="loc_Exact"><span class="id" title="constructor">loc_Exact</span></a> | <a name="loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#comparison"><span class="id" title="inductive">comparison</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.Calc.Fcalc_bracket.html#location"><span class="id" title="inductive">location</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fcalc_bracket.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">Definition</span> <a name="inbetween_loc"><span class="id" title="definition">inbetween_loc</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_Raux.html#Rcompare"><span class="id" title="definition">Rcompare</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.d"><span class="id" title="variable">d</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#Gt"><span class="id" title="constructor">Gt</span></a> ⇒ <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> (<a class="idref" href="Flocq.Core.Fcore_Raux.html#Rcompare"><span class="id" title="definition">Rcompare</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.x"><span class="id" title="variable">x</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.Calc.Fcalc_bracket.html#Fcalc_bracket.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.Calc.Fcalc_bracket.html#Fcalc_bracket.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> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0c0207ff801f7c795ce431f130ae670a"><span class="id" title="notation">/</span></a> 2))<br/>
| <span class="id" title="var">_</span> ⇒ <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Exact"><span class="id" title="constructor">loc_Exact</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
</div>
<div class="doc">
Locates a real number with respect to the middle of two other numbers.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Inductive</span> <a name="inbetween"><span class="id" title="inductive">inbetween</span></a> : <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#location"><span class="id" title="inductive">location</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="inbetween_Exact"><span class="id" title="constructor">inbetween_Exact</span></a> : <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.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.Calc.Fcalc_bracket.html#Fcalc_bracket.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.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Exact"><span class="id" title="constructor">loc_Exact</span></a><br/>
| <a name="inbetween_Inexact"><span class="id" title="constructor">inbetween_Inexact</span></a> <span class="id" title="var">l</span> : (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7c35b2a93856d788d8a50a85631cf07a"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7c35b2a93856d788d8a50a85631cf07a"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.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> <a class="idref" href="Flocq.Core.Fcore_Raux.html#Rcompare"><span class="id" title="definition">Rcompare</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.x"><span class="id" title="variable">x</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.Calc.Fcalc_bracket.html#Fcalc_bracket.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.Calc.Fcalc_bracket.html#Fcalc_bracket.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> <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> <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.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_spec"><span class="id" title="lemma">inbetween_spec</span></a> :<br/>
(<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.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.Calc.Fcalc_bracket.html#Fcalc_bracket.x"><span class="id" title="variable">x</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.Calc.Fcalc_bracket.html#Fcalc_bracket.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> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween_loc"><span class="id" title="definition">inbetween_loc</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_unique"><span class="id" title="lemma">inbetween_unique</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">l</span> <span class="id" title="var">l'</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l'"><span class="id" title="variable">l'</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.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#l'"><span class="id" title="variable">l'</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fcalc_bracket.Fcalc_bracket_any"><span class="id" title="section">Fcalc_bracket_any</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fcalc_bracket.Fcalc_bracket_any.l"><span class="id" title="variable">l</span></a> : <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#location"><span class="id" title="inductive">location</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_bounds"><span class="id" title="lemma">inbetween_bounds</span></a> :<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.Fcalc_bracket_any.l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#Fcalc_bracket.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.Calc.Fcalc_bracket.html#Fcalc_bracket.x"><span class="id" title="variable">x</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.Calc.Fcalc_bracket.html#Fcalc_bracket.u"><span class="id" title="variable">u</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_bounds_not_Eq"><span class="id" title="lemma">inbetween_bounds_not_Eq</span></a> :<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.Fcalc_bracket_any.l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#Fcalc_bracket.Fcalc_bracket_any.l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#loc_Exact"><span class="id" title="constructor">loc_Exact</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.Calc.Fcalc_bracket.html#Fcalc_bracket.d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7c35b2a93856d788d8a50a85631cf07a"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7c35b2a93856d788d8a50a85631cf07a"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.u"><span class="id" title="variable">u</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.Fcalc_bracket_any"><span class="id" title="section">Fcalc_bracket_any</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_distance_inexact"><span class="id" title="lemma">inbetween_distance_inexact</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">l</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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_Raux.html#Rcompare"><span class="id" title="definition">Rcompare</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.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.Calc.Fcalc_bracket.html#Fcalc_bracket.d"><span class="id" title="variable">d</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket.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.Calc.Fcalc_bracket.html#Fcalc_bracket.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.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_distance_inexact_abs"><span class="id" title="lemma">inbetween_distance_inexact_abs</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">l</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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_Raux.html#Rcompare"><span class="id" title="definition">Rcompare</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.Calc.Fcalc_bracket.html#Fcalc_bracket.d"><span class="id" title="variable">d</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.Calc.Fcalc_bracket.html#Fcalc_bracket.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.Calc.Fcalc_bracket.html#Fcalc_bracket.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.Calc.Fcalc_bracket.html#Fcalc_bracket.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.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket"><span class="id" title="section">Fcalc_bracket</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_ex"><span class="id" title="lemma">inbetween_ex</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">d</span> <span class="id" title="var">u</span> <span class="id" title="var">l</span>,<br/>
(<a class="idref" href="Flocq.Calc.Fcalc_bracket.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#1cc22ba6849531267d3b25ca7b262449"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#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="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">x</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.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fcalc_bracket_step"><span class="id" title="section">Fcalc_bracket_step</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fcalc_bracket_step.start"><span class="id" title="variable">start</span></a> <a name="Fcalc_bracket_step.step"><span class="id" title="variable">step</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">Variable</span> <a name="Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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="Fcalc_bracket_step.Hstep"><span class="id" title="variable">Hstep</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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="ordered_steps"><span class="id" title="lemma">ordered_steps</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">k</span>,<br/>
(<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="middle_range"><span class="id" title="lemma">middle_range</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">k</span>,<br/>
(<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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</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="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0c0207ff801f7c795ce431f130ae670a"><span class="id" title="notation">)</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 <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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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="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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</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>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Hypothesis</span> (<a name="Fcalc_bracket_step.Hnb_steps"><span class="id" title="variable">Hnb_steps</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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</span></a>)%<span class="id" title="var">Z</span>).<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="inbetween_step_not_Eq"><span class="id" title="lemma">inbetween_step_not_Eq</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">k</span> <span class="id" title="var">l</span> <span class="id" title="var">l'</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.ZArith.BinInt.html#0ae6347154955be5e4fdfa755ff4a025"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0ae6347154955be5e4fdfa755ff4a025"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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><br/>
<a class="idref" href="Flocq.Core.Fcore_Raux.html#Rcompare"><span class="id" title="definition">Rcompare</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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="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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</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>)%<span class="id" title="var">R</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="Flocq.Calc.Fcalc_bracket.html#l'"><span class="id" title="variable">l'</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.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l'"><span class="id" title="variable">l'</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_step_Lo"><span class="id" title="lemma">inbetween_step_Lo</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">k</span> <span class="id" title="var">l</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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> (2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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 <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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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><br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_step_Hi"><span class="id" title="lemma">inbetween_step_Hi</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">k</span> <span class="id" title="var">l</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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> 2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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><br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Gt"><span class="id" title="constructor">Gt</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_step_Lo_not_Eq"><span class="id" title="lemma">inbetween_step_Lo_not_Eq</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">l</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#loc_Exact"><span class="id" title="constructor">loc_Exact</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.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a>).<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="middle_odd"><span class="id" title="lemma">middle_odd</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">k</span>,<br/>
(2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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 <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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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><br/>
(<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="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</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="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</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="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0c0207ff801f7c795ce431f130ae670a"><span class="id" title="notation">)/</span></a>2 <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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_step_any_Mi_odd"><span class="id" title="lemma">inbetween_step_any_Mi_odd</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">k</span> <span class="id" title="var">l</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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/>
(2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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 <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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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><br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_step_Lo_Mi_Eq_odd"><span class="id" title="lemma">inbetween_step_Lo_Mi_Eq_odd</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">k</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Exact"><span class="id" title="constructor">loc_Exact</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/>
(2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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 <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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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><br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_step_Hi_Mi_even"><span class="id" title="lemma">inbetween_step_Hi_Mi_even</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">k</span> <span class="id" title="var">l</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#loc_Exact"><span class="id" title="constructor">loc_Exact</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/>
(2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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><br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Gt"><span class="id" title="constructor">Gt</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_step_Mi_Mi_even"><span class="id" title="lemma">inbetween_step_Mi_Mi_even</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">k</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Exact"><span class="id" title="constructor">loc_Exact</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/>
(2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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><br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Eq"><span class="id" title="constructor">Eq</span></a>).<br/>
<br/>
</div>
<div class="doc">
Computes a new location when the interval containing a real
number is split into nb_steps subintervals and the real is
in the k-th one. (Even radix.)
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="new_location_even"><span class="id" title="definition">new_location_even</span></a> <span class="id" title="var">k</span> <span class="id" title="var">l</span> :=<br/>
<span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zeq_bool"><span class="id" title="definition">Zeq_bool</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> 0 <span class="id" title="keyword">then</span><br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Exact"><span class="id" title="constructor">loc_Exact</span></a> ⇒ <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a> | <span class="id" title="var">_</span> ⇒ <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a> <span class="id" title="keyword">end</span><br/>
<span class="id" title="keyword">else</span><br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a><br/>
<span class="id" title="keyword">match</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zcompare"><span class="id" title="abbreviation">Zcompare</span></a> (2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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#Lt"><span class="id" title="constructor">Lt</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Eq"><span class="id" title="constructor">Eq</span></a> ⇒ <span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Exact"><span class="id" title="constructor">loc_Exact</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Eq"><span class="id" title="constructor">Eq</span></a> | <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Gt"><span class="id" title="constructor">Gt</span></a> <span class="id" title="keyword">end</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Gt"><span class="id" title="constructor">Gt</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Gt"><span class="id" title="constructor">Gt</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="new_location_even_correct"><span class="id" title="lemma">new_location_even_correct</span></a> :<br/>
<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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> <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">k</span> <span class="id" title="var">l</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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><br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#new_location_even"><span class="id" title="definition">new_location_even</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>).<br/>
<br/>
</div>
<div class="doc">
Computes a new location when the interval containing a real
number is split into nb_steps subintervals and the real is
in the k-th one. (Odd radix.)
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="new_location_odd"><span class="id" title="definition">new_location_odd</span></a> <span class="id" title="var">k</span> <span class="id" title="var">l</span> :=<br/>
<span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zeq_bool"><span class="id" title="definition">Zeq_bool</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> 0 <span class="id" title="keyword">then</span><br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Exact"><span class="id" title="constructor">loc_Exact</span></a> ⇒ <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a> | <span class="id" title="var">_</span> ⇒ <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a> <span class="id" title="keyword">end</span><br/>
<span class="id" title="keyword">else</span><br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a><br/>
<span class="id" title="keyword">match</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zcompare"><span class="id" title="abbreviation">Zcompare</span></a> (2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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#Lt"><span class="id" title="constructor">Lt</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Eq"><span class="id" title="constructor">Eq</span></a> ⇒ <span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Inexact"><span class="id" title="constructor">loc_Inexact</span></a> <span class="id" title="var">l</span> ⇒ <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a> | <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Exact"><span class="id" title="constructor">loc_Exact</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a> <span class="id" title="keyword">end</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Gt"><span class="id" title="constructor">Gt</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Gt"><span class="id" title="constructor">Gt</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="new_location_odd_correct"><span class="id" title="lemma">new_location_odd_correct</span></a> :<br/>
<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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#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">k</span> <span class="id" title="var">l</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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><br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#new_location_odd"><span class="id" title="definition">new_location_odd</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="new_location"><span class="id" title="definition">new_location</span></a> :=<br/>
<span class="id" title="keyword">if</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#new_location_even"><span class="id" title="definition">new_location_even</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#new_location_odd"><span class="id" title="definition">new_location_odd</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="new_location_correct"><span class="id" title="lemma">new_location_correct</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">k</span> <span class="id" title="var">l</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</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><br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.start"><span class="id" title="variable">start</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_Raux.html#Z2R"><span class="id" title="definition">Z2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.nb_steps"><span class="id" title="variable">nb_steps</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step.step"><span class="id" title="variable">step</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#new_location"><span class="id" title="definition">new_location</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>).<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_step"><span class="id" title="section">Fcalc_bracket_step</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fcalc_bracket_scale"><span class="id" title="section">Fcalc_bracket_scale</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="inbetween_mult_aux"><span class="id" title="lemma">inbetween_mult_aux</span></a> :<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">s</span>,<br/>
(<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.Calc.Fcalc_bracket.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#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#s"><span class="id" title="variable">s</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.Calc.Fcalc_bracket.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#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#s"><span class="id" title="variable">s</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="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0c0207ff801f7c795ce431f130ae670a"><span class="id" title="notation">/</span></a> 2 <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#0c0207ff801f7c795ce431f130ae670a"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Calc.Fcalc_bracket.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#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.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#0c0207ff801f7c795ce431f130ae670a"><span class="id" title="notation">)</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 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#s"><span class="id" title="variable">s</span></a>)%<span class="id" title="var">R</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_mult_compat"><span class="id" title="lemma">inbetween_mult_compat</span></a> :<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">l</span> <span class="id" title="var">s</span>,<br/>
(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.Calc.Fcalc_bracket.html#s"><span class="id" title="variable">s</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.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.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#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#s"><span class="id" title="variable">s</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.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#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#s"><span class="id" title="variable">s</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.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#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#s"><span class="id" title="variable">s</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_mult_reg"><span class="id" title="lemma">inbetween_mult_reg</span></a> :<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">l</span> <span class="id" title="var">s</span>,<br/>
(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.Calc.Fcalc_bracket.html#s"><span class="id" title="variable">s</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.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.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#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#s"><span class="id" title="variable">s</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.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#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#s"><span class="id" title="variable">s</span></a>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.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#361afbb9b173fae6251865f2da226003"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#s"><span class="id" title="variable">s</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_scale"><span class="id" title="section">Fcalc_bracket_scale</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fcalc_bracket_generic"><span class="id" title="section">Fcalc_bracket_generic</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">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/>
</div>
<div class="doc">
Specialization of inbetween for two consecutive floating-point numbers.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="inbetween_float"><span class="id" title="definition">inbetween_float</span></a> <span class="id" title="var">m</span> <span class="id" title="var">e</span> <span class="id" title="var">x</span> <span class="id" title="var">l</span> :=<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</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.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#e"><span class="id" title="variable">e</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.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</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) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#e"><span class="id" title="variable">e</span></a>)) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_float_bounds"><span class="id" title="lemma">inbetween_float_bounds</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">m</span> <span class="id" title="var">e</span> <span class="id" title="var">l</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween_float"><span class="id" title="definition">inbetween_float</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#e"><span class="id" title="variable">e</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.Calc.Fcalc_bracket.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#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.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</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) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#e"><span class="id" title="variable">e</span></a>))%<span class="id" title="var">R</span>.<br/>
<br/>
</div>
<div class="doc">
Specialization of inbetween for two consecutive integers.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="inbetween_int"><span class="id" title="definition">inbetween_int</span></a> <span class="id" title="var">m</span> <span class="id" title="var">x</span> <span class="id" title="var">l</span> :=<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween"><span class="id" title="inductive">inbetween</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.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</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.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</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)) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_float_new_location"><span class="id" title="lemma">inbetween_float_new_location</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">m</span> <span class="id" title="var">e</span> <span class="id" title="var">l</span> <span class="id" title="var">k</span>,<br/>
(0 <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.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</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><br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween_float"><span class="id" title="definition">inbetween_float</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#inbetween_float"><span class="id" title="definition">inbetween_float</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zdiv"><span class="id" title="abbreviation">Zdiv</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a>)) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.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#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#new_location"><span class="id" title="definition">new_location</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zmod"><span class="id" title="abbreviation">Zmod</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#k"><span class="id" title="variable">k</span></a>)) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_float_new_location_single"><span class="id" title="lemma">inbetween_float_new_location_single</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">m</span> <span class="id" title="var">e</span> <span class="id" title="var">l</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween_float"><span class="id" title="definition">inbetween_float</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#inbetween_float"><span class="id" title="definition">inbetween_float</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zdiv"><span class="id" title="abbreviation">Zdiv</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</span></a> <span class="id" title="keyword">beta</span>) (<a class="idref" href="Flocq.Calc.Fcalc_bracket.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#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#new_location"><span class="id" title="definition">new_location</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zmod"><span class="id" title="abbreviation">Zmod</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</span></a> <span class="id" title="keyword">beta</span>) <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_float_ex"><span class="id" title="lemma">inbetween_float_ex</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span> <span class="id" title="var">e</span> <span class="id" title="var">l</span>,<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">x</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.Calc.Fcalc_bracket.html#inbetween_float"><span class="id" title="definition">inbetween_float</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="inbetween_float_unique"><span class="id" title="lemma">inbetween_float_unique</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">e</span> <span class="id" title="var">m</span> <span class="id" title="var">l</span> <span class="id" title="var">m'</span> <span class="id" title="var">l'</span>,<br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween_float"><span class="id" title="definition">inbetween_float</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#inbetween_float"><span class="id" title="definition">inbetween_float</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#m'"><span class="id" title="variable">m'</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#l'"><span class="id" title="variable">l'</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.Calc.Fcalc_bracket.html#m"><span class="id" title="variable">m</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.Calc.Fcalc_bracket.html#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.Calc.Fcalc_bracket.html#l"><span class="id" title="variable">l</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.Calc.Fcalc_bracket.html#l'"><span class="id" title="variable">l'</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#Fcalc_bracket_generic"><span class="id" title="section">Fcalc_bracket_generic</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
>
76
