<!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>mathcomp.algebra.interval</title>
</head>

<body>

<div id="page">

<div id="header">
</div>

<div id="main">

<h1 class="libtitle">Library mathcomp.algebra.interval</h1>

<div class="code">
<span class="comment">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/>

<br/>
</div>

<div class="doc">
 This file provide support for intervals in numerical and real domains.    
 The datatype (interval R) gives a formal characterization of an           
 interval, as the pair of its right and left bounds.                       
    interval R    == the type of formal intervals on R.                    
    x \in i       == when i is a formal interval on a numeric domain,      
                   \in can be used to test membership.                     
    itvP x_in_i   == where x_in_i has type x \in i, if i is ground,        
                   gives a set of rewrite rules that x_in_i imply.         
 x &lt;= y ?&lt; if c   == x is smaller than y, and strictly if c is true        

<div class="paragraph"> </div>

 We provide a set of notations to write intervals (see below)              
 ` [a, b], ` ]a, b], ..., ` ]-oo, a], ..., ` ]-oo, +oo[                        
 We also provide the lemma subitvP which computes the inequalities one     
 needs to prove when trying to prove the inclusion of intervals.           

<div class="paragraph"> </div>

 Remark that we cannot implement a boolean comparison test for intervals   
 on an arbitrary numeric domains, for this problem might be undecidable.   
 Note also that type (interval R) may contain several inhabitants coding   
 for the same interval. However, this pathological issues do nor arise     
 when R is a real domain: we could provide a specific theory for this      
 important case.                                                           

<div class="paragraph"> </div>

 See also ``Formal proofs in real algebraic geometry: from ordered fields  
 to quantifier elimination'', LMCS journal, 2012                           
 by Cyril Cohen and Assia Mahboubi                                         

<div class="paragraph"> </div>

 And "Formalized algebraic numbers: construction and first-order theory"   
 Cyril Cohen, PhD, 2012, section 4.3.                                       
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>

<br/>
<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">GRing.Theory</span> <span class="id" title="var">Num.Theory</span>.<br/>

<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="IntervalPo"><span class="id" title="section">IntervalPo</span></a>.<br/>

<br/>
<span class="id" title="keyword">CoInductive</span> <a name="itv_bound"><span class="id" title="inductive">itv_bound</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> := <a name="BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> &amp; <a class="idref" href="mathcomp.algebra.interval.html#T"><span class="id" title="variable">T</span></a> | <a name="BInfty"><span class="id" title="constructor">BInfty</span></a>.<br/>
<span class="id" title="keyword">Notation</span> <a name="BOpen"><span class="id" title="abbreviation">BOpen</span></a> := (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>).<br/>
<span class="id" title="keyword">Notation</span> <a name="BClose"><span class="id" title="abbreviation">BClose</span></a> := (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>).<br/>
<span class="id" title="keyword">CoInductive</span> <a name="interval"><span class="id" title="inductive">interval</span></a> (<span class="id" title="var">T</span> : <span class="id" title="keyword">Type</span>) := <a name="Interval"><span class="id" title="constructor">Interval</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.algebra.interval.html#itv_bound"><span class="id" title="inductive">itv_bound</span></a> <a class="idref" href="mathcomp.algebra.interval.html#T"><span class="id" title="variable">T</span></a> &amp; <a class="idref" href="mathcomp.algebra.interval.html#itv_bound"><span class="id" title="inductive">itv_bound</span></a> <a class="idref" href="mathcomp.algebra.interval.html#T"><span class="id" title="variable">T</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variable</span> (<a name="IntervalPo.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssrnum.html#Num.NumDomain.Exports.numDomainType"><span class="id" title="abbreviation">numDomainType</span></a>).<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="pred_of_itv"><span class="id" title="definition">pred_of_itv</span></a> (<span class="id" title="var">i</span> : <a class="idref" href="mathcomp.algebra.interval.html#interval"><span class="id" title="inductive">interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">pred</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">|</span></a> <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <span class="id" title="var">l</span> <span class="id" title="var">u</span> := <a class="idref" href="mathcomp.algebra.interval.html#i"><span class="id" title="variable">i</span></a> <span class="id" title="tactic">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <span class="id" title="var">l</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BOpen</span> <span class="id" title="var">a</span> ⇒ <span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BClose</span> <span class="id" title="var">a</span> ⇒ <span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <span class="id" title="var">u</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BOpen</span> <span class="id" title="var">b</span> ⇒ <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <span class="id" title="var">b</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BClose</span> <span class="id" title="var">b</span> ⇒ <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <span class="id" title="var">b</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="keyword">Structure</span> <span class="id" title="var">itvPredType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mkPredType"><span class="id" title="definition">mkPredType</span></a> <a class="idref" href="mathcomp.algebra.interval.html#pred_of_itv"><span class="id" title="definition">pred_of_itv</span></a>.<br/>

<br/>
</div>

<div class="doc">
 We provide the 9 following notations to help writing formal intervals  
</div>
<div class="code">
<span class="id" title="keyword">Notation</span> <a name="0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">&quot;</span></a>`[ a , b ]" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <span class="id" title="var">a</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <span class="id" title="var">b</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">a</span>, <span class="id" title="var">b</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`[ a ,  b ]") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">&quot;</span></a>`] a , b ]" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <span class="id" title="var">a</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <span class="id" title="var">b</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">a</span>, <span class="id" title="var">b</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`] a ,  b ]") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">&quot;</span></a>`[ a , b [" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <span class="id" title="var">a</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <span class="id" title="var">b</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">a</span>, <span class="id" title="var">b</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`[ a ,  b [") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="5d6177042cf2728bb3a48ad4d7fef36d"><span class="id" title="notation">&quot;</span></a>`] a , b [" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <span class="id" title="var">a</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <span class="id" title="var">b</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">a</span>, <span class="id" title="var">b</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`] a ,  b [") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="6d014c3c0583cf03ab0a7cdc9d80e6e4"><span class="id" title="notation">&quot;</span></a>`] '-oo' , b ]" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <span class="id" title="var">b</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">b</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`] '-oo' ,  b ]") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="f7d4545c39e6f558b751e487fae5aef4"><span class="id" title="notation">&quot;</span></a>`] '-oo' , b [" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <span class="id" title="var">b</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">b</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`] '-oo' ,  b [") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="84c6be04931432ed71a28392cd19d478"><span class="id" title="notation">&quot;</span></a>`[ a , '+oo' [" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <span class="id" title="var">a</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">a</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`[ a ,  '+oo' [") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="ddab974cd5332360c70b1aca114bd394"><span class="id" title="notation">&quot;</span></a>`] a , '+oo' [" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <span class="id" title="var">a</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">a</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`] a ,  '+oo' [") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="996170680ea33f9a35c3d01667d531c3"><span class="id" title="notation">&quot;</span></a>`] -oo , '+oo' [" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "`] -oo ,  '+oo' [") : <span class="id" title="var">ring_scope</span>.<br/>

<br/>
</div>

<div class="doc">
 we compute a set of rewrite rules associated to an interval  
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a name="itv_rewrite"><span class="id" title="definition">itv_rewrite</span></a> (<span class="id" title="var">i</span> : <a class="idref" href="mathcomp.algebra.interval.html#interval"><span class="id" title="inductive">interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>) <span class="id" title="var">x</span> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <span class="id" title="var">l</span> <span class="id" title="var">u</span> := <a class="idref" href="mathcomp.algebra.interval.html#i"><span class="id" title="variable">i</span></a> <span class="id" title="tactic">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="keyword">match</span> <span class="id" title="var">l</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BClose</span> <span class="id" title="var">a</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BOpen</span> <span class="id" title="var">a</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> ⇒ <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>, <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <span class="id" title="var">u</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BClose</span> <span class="id" title="var">b</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <span class="id" title="var">b</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">b</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BOpen</span> <span class="id" title="var">b</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <span class="id" title="var">b</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <span class="id" title="var">b</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">b</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> ⇒ <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>, <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <span class="id" title="var">l</span>, <span class="id" title="var">u</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BClose</span> <span class="id" title="var">a</span>, <span class="id" title="var">BClose</span> <span class="id" title="var">b</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <span class="id" title="var">b</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">b</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">`[</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">b</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">`[</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BClose</span> <span class="id" title="var">a</span>, <span class="id" title="var">BOpen</span> <span class="id" title="var">b</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <span class="id" title="var">b</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <span class="id" title="var">b</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">b</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">`[</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">`[</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">b</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">`[</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">b</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">`]</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BOpen</span> <span class="id" title="var">a</span>, <span class="id" title="var">BClose</span> <span class="id" title="var">b</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <span class="id" title="var">b</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <span class="id" title="var">b</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">b</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">`[</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">`[</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">b</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">`[</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">b</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">`]</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BOpen</span> <span class="id" title="var">a</span>, <span class="id" title="var">BOpen</span> <span class="id" title="var">b</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <span class="id" title="var">b</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <span class="id" title="var">b</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">b</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">`[</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">`[</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)*</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">b</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">`[</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="var">b</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">`]</span></a><span class="id" title="var">a</span><a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">,</span></a> <span class="id" title="var">b</span><a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>, <span class="id" title="var">_</span> ⇒ <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>, <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span>)%<span class="id" title="keyword">type</span>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="itv_decompose"><span class="id" title="definition">itv_decompose</span></a> (<span class="id" title="var">i</span> : <a class="idref" href="mathcomp.algebra.interval.html#interval"><span class="id" title="inductive">interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>) <span class="id" title="var">x</span> : <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <span class="id" title="var">l</span> <span class="id" title="var">u</span> := <a class="idref" href="mathcomp.algebra.interval.html#i"><span class="id" title="variable">i</span></a> <span class="id" title="tactic">in</span><br/>
&nbsp;&nbsp;(<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="keyword">match</span> <span class="id" title="var">l</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BClose</span> <span class="id" title="var">a</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">Prop</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BOpen</span> <span class="id" title="var">a</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">(</span></a><span class="id" title="var">a</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">Prop</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">Prop</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">(</span></a><span class="id" title="keyword">match</span> <span class="id" title="var">u</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BClose</span> <span class="id" title="var">b</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <span class="id" title="var">b</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">Prop</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">BOpen</span> <span class="id" title="var">b</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <span class="id" title="var">b</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">Prop</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0fffdc558ce71ab561d36c8a8094dbe5"><span class="id" title="notation">Prop</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">)</span></a>)%<span class="id" title="keyword">type</span>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="itv_dec"><span class="id" title="lemma">itv_dec</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>) (<span class="id" title="var">i</span> : <a class="idref" href="mathcomp.algebra.interval.html#interval"><span class="id" title="inductive">interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#itv_decompose"><span class="id" title="definition">itv_decompose</span></a> <a class="idref" href="mathcomp.algebra.interval.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#i"><span class="id" title="variable">i</span></a>).<br/>
 
<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="lersif"><span class="id" title="definition">lersif</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>) <span class="id" title="var">b</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a>.<br/>

<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="lersifxx"><span class="id" title="lemma">lersifxx</span></a> <span class="id" title="var">x</span> <span class="id" title="var">b</span>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="lersif_trans"><span class="id" title="lemma">lersif_trans</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> <span class="id" title="var">b1</span> <span class="id" title="var">b2</span> :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b1"><span class="id" title="variable">b1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b1"><span class="id" title="variable">b1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b2"><span class="id" title="variable">b2</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="lersifW"><span class="id" title="lemma">lersifW</span></a> <span class="id" title="var">b</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="lersifNF"><span class="id" title="lemma">lersifNF</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">b</span> : <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a>  <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="lersifS"><span class="id" title="lemma">lersifS</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">b</span> : <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="lersifT"><span class="id" title="lemma">lersifT</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.  <br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="lersifF"><span class="id" title="lemma">lersifF</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.  <br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="le_boundl"><span class="id" title="definition">le_boundl</span></a> <span class="id" title="var">b1</span> <span class="id" title="var">b2</span> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.algebra.interval.html#b1"><span class="id" title="variable">b1</span></a>, <a class="idref" href="mathcomp.algebra.interval.html#b2"><span class="id" title="variable">b2</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <span class="id" title="var">b1</span> <span class="id" title="var">x1</span>, <a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <span class="id" title="var">b2</span> <span class="id" title="var">x2</span> ⇒ <span class="id" title="var">x1</span> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <span class="id" title="var">x2</span> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b1"><span class="id" title="variable">b1</span></a><a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span>, <a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>, <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="le_boundr"><span class="id" title="definition">le_boundr</span></a> <span class="id" title="var">b1</span> <span class="id" title="var">b2</span> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.algebra.interval.html#b1"><span class="id" title="variable">b1</span></a>, <a class="idref" href="mathcomp.algebra.interval.html#b2"><span class="id" title="variable">b2</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <span class="id" title="var">b1</span> <span class="id" title="var">x1</span>, <a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <span class="id" title="var">b2</span> <span class="id" title="var">x2</span> ⇒ <span class="id" title="var">x1</span> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <span class="id" title="var">x2</span> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b1"><span class="id" title="variable">b1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b2"><span class="id" title="variable">b2</span></a><a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a>, <a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>, <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="itv_boundlr"><span class="id" title="lemma">itv_boundlr</span></a> <span class="id" title="var">bl</span> <span class="id" title="var">br</span> <span class="id" title="var">x</span> :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bl"><span class="id" title="variable">bl</span></a> <a class="idref" href="mathcomp.algebra.interval.html#br"><span class="id" title="variable">br</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#le_boundl"><span class="id" title="definition">le_boundl</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bl"><span class="id" title="variable">bl</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#le_boundr"><span class="id" title="definition">le_boundr</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.algebra.interval.html#br"><span class="id" title="variable">br</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="le_boundr_refl"><span class="id" title="lemma">le_boundr_refl</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflexive"><span class="id" title="definition">reflexive</span></a> <a class="idref" href="mathcomp.algebra.interval.html#le_boundr"><span class="id" title="definition">le_boundr</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">le_boundr_refl</span>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="le_boundl_refl"><span class="id" title="lemma">le_boundl_refl</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflexive"><span class="id" title="definition">reflexive</span></a> <a class="idref" href="mathcomp.algebra.interval.html#le_boundl"><span class="id" title="definition">le_boundl</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">le_boundl_refl</span>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="le_boundl_bb"><span class="id" title="lemma">le_boundl_bb</span></a> <span class="id" title="var">x</span> <span class="id" title="var">b1</span> <span class="id" title="var">b2</span> :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#le_boundl"><span class="id" title="definition">le_boundl</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b1"><span class="id" title="variable">b1</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#b1"><span class="id" title="variable">b1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#3b17cb5f3a16fa64a62421f68786f750"><span class="id" title="notation">==&gt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b2"><span class="id" title="variable">b2</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="le_boundr_bb"><span class="id" title="lemma">le_boundr_bb</span></a> <span class="id" title="var">x</span> <span class="id" title="var">b1</span> <span class="id" title="var">b2</span> :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#le_boundr"><span class="id" title="definition">le_boundr</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b1"><span class="id" title="variable">b1</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#3b17cb5f3a16fa64a62421f68786f750"><span class="id" title="notation">==&gt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b1"><span class="id" title="variable">b1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="itv_xx"><span class="id" title="lemma">itv_xx</span></a> <span class="id" title="var">x</span> <span class="id" title="var">bl</span> <span class="id" title="var">br</span> :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bl"><span class="id" title="variable">bl</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#br"><span class="id" title="variable">br</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">i</span></a> <br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#bl"><span class="id" title="variable">bl</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="mathcomp.algebra.interval.html#br"><span class="id" title="variable">br</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#pred1"><span class="id" title="definition">pred1</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred0"><span class="id" title="definition">pred0</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="itv_gte"><span class="id" title="lemma">itv_gte</span></a> <span class="id" title="var">ba</span> <span class="id" title="var">xa</span> <span class="id" title="var">bb</span> <span class="id" title="var">xb</span> :  <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#ba"><span class="id" title="variable">ba</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bb"><span class="id" title="variable">bb</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">)</span></a> <br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#ba"><span class="id" title="variable">ba</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bb"><span class="id" title="variable">bb</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred0"><span class="id" title="definition">pred0</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="boundl_in_itv"><span class="id" title="lemma">boundl_in_itv</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">ba</span> <span class="id" title="var">xa</span> <span class="id" title="var">b</span>,<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#ba"><span class="id" title="variable">ba</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a>) <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#ba"><span class="id" title="variable">ba</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.algebra.interval.html#le_boundr"><span class="id" title="definition">le_boundr</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a>) <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="boundr_in_itv"><span class="id" title="lemma">boundr_in_itv</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">bb</span> <span class="id" title="var">xb</span> <span class="id" title="var">a</span>,<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bb"><span class="id" title="variable">bb</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bb"><span class="id" title="variable">bb</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.algebra.interval.html#le_boundl"><span class="id" title="definition">le_boundl</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a>).<br/>
 
<br/>
<span class="id" title="keyword">Definition</span> <a name="bound_in_itv"><span class="id" title="definition">bound_in_itv</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#boundl_in_itv"><span class="id" title="lemma">boundl_in_itv</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.interval.html#boundr_in_itv"><span class="id" title="lemma">boundr_in_itv</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="itvP"><span class="id" title="lemma">itvP</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>) (<span class="id" title="var">i</span> : <a class="idref" href="mathcomp.algebra.interval.html#interval"><span class="id" title="inductive">interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>), <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.interval.html#itv_rewrite"><span class="id" title="definition">itv_rewrite</span></a> <a class="idref" href="mathcomp.algebra.interval.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a>.<br/>

<br/>
<span class="id" title="keyword">Hint Rewrite</span> <a class="idref" href="mathcomp.algebra.ssrint.html#intP"><span class="id" title="lemma">intP</span></a>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="subitv"><span class="id" title="definition">subitv</span></a> (<span class="id" title="var">i1</span> <span class="id" title="var">i2</span> : <a class="idref" href="mathcomp.algebra.interval.html#interval"><span class="id" title="inductive">interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.algebra.interval.html#i1"><span class="id" title="variable">i1</span></a>, <a class="idref" href="mathcomp.algebra.interval.html#i2"><span class="id" title="variable">i2</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <span class="id" title="var">a1</span> <span class="id" title="var">b1</span>, <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <span class="id" title="var">a2</span> <span class="id" title="var">b2</span> ⇒ <a class="idref" href="mathcomp.algebra.interval.html#le_boundl"><span class="id" title="definition">le_boundl</span></a> <span class="id" title="var">a2</span> <span class="id" title="var">a1</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#le_boundr"><span class="id" title="definition">le_boundr</span></a> <span class="id" title="var">b1</span> <span class="id" title="var">b2</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="subitvP"><span class="id" title="lemma">subitvP</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">i2</span> <span class="id" title="var">i1</span> : <a class="idref" href="mathcomp.algebra.interval.html#interval"><span class="id" title="inductive">interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>), <br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#subitv"><span class="id" title="definition">subitv</span></a> <a class="idref" href="mathcomp.algebra.interval.html#i1"><span class="id" title="variable">i1</span></a> <a class="idref" href="mathcomp.algebra.interval.html#i2"><span class="id" title="variable">i2</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.algebra.interval.html#i1"><span class="id" title="variable">i1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#i2"><span class="id" title="variable">i2</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">}</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="subitvPr"><span class="id" title="lemma">subitvPr</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">a</span> <span class="id" title="var">b1</span> <span class="id" title="var">b2</span> : <a class="idref" href="mathcomp.algebra.interval.html#itv_bound"><span class="id" title="inductive">itv_bound</span></a> <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#le_boundr"><span class="id" title="definition">le_boundr</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b1"><span class="id" title="variable">b1</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">subset</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b1"><span class="id" title="variable">b1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b2"><span class="id" title="variable">b2</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">)}</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="subitvPl"><span class="id" title="lemma">subitvPl</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">a1</span> <span class="id" title="var">a2</span> <span class="id" title="var">b</span> : <a class="idref" href="mathcomp.algebra.interval.html#itv_bound"><span class="id" title="inductive">itv_bound</span></a> <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#le_boundl"><span class="id" title="definition">le_boundl</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a2"><span class="id" title="variable">a2</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a1"><span class="id" title="variable">a1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">subset</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a1"><span class="id" title="variable">a1</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a2"><span class="id" title="variable">a2</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">)}</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="lersif_in_itv"><span class="id" title="lemma">lersif_in_itv</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">ba</span> <span class="id" title="var">bb</span> <span class="id" title="var">xa</span> <span class="id" title="var">xb</span> <span class="id" title="var">x</span>,<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#ba"><span class="id" title="variable">ba</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bb"><span class="id" title="variable">bb</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#ba"><span class="id" title="variable">ba</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bb"><span class="id" title="variable">bb</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="ltr_in_itv"><span class="id" title="lemma">ltr_in_itv</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">ba</span> <span class="id" title="var">bb</span> <span class="id" title="var">xa</span> <span class="id" title="var">xb</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.algebra.interval.html#ba"><span class="id" title="variable">ba</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bb"><span class="id" title="variable">bb</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#ba"><span class="id" title="variable">ba</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bb"><span class="id" title="variable">bb</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="ler_in_itv"><span class="id" title="lemma">ler_in_itv</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">ba</span> <span class="id" title="var">bb</span> <span class="id" title="var">xa</span> <span class="id" title="var">xb</span> <span class="id" title="var">x</span>,<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#ba"><span class="id" title="variable">ba</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bb"><span class="id" title="variable">bb</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="mem0_itvcc_xNx"><span class="id" title="lemma">mem0_itvcc_xNx</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a>0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">`[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a>0 <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="mem0_itvoo_xNx"><span class="id" title="lemma">mem0_itvoo_xNx</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#5d6177042cf2728bb3a48ad4d7fef36d"><span class="id" title="notation">`](</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.interval.html#5d6177042cf2728bb3a48ad4d7fef36d"><span class="id" title="notation">),</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.interval.html#5d6177042cf2728bb3a48ad4d7fef36d"><span class="id" title="notation">[</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a>0 <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="itv_splitI"><span class="id" title="lemma">itv_splitI</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>, <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>,<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>) <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="real_lersifN"><span class="id" title="lemma">real_lersifN</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">b</span> : <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#Num.real"><span class="id" title="abbreviation">Num.real</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#Num.real"><span class="id" title="abbreviation">Num.real</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a><a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1c796095ee2c250ae9d97f3c7d8c93ac"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="oppr_itv"><span class="id" title="lemma">oppr_itv</span></a> <span class="id" title="var">ba</span> <span class="id" title="var">bb</span> (<span class="id" title="var">xa</span> <span class="id" title="var">xb</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>) :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#ba"><span class="id" title="variable">ba</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bb"><span class="id" title="variable">bb</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bb"><span class="id" title="variable">bb</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a>)) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#ba"><span class="id" title="variable">ba</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a>))<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="oppr_itvoo"><span class="id" title="lemma">oppr_itvoo</span></a> (<span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#5d6177042cf2728bb3a48ad4d7fef36d"><span class="id" title="notation">`]</span></a><a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.algebra.interval.html#5d6177042cf2728bb3a48ad4d7fef36d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="mathcomp.algebra.interval.html#5d6177042cf2728bb3a48ad4d7fef36d"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#5d6177042cf2728bb3a48ad4d7fef36d"><span class="id" title="notation">`](</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="mathcomp.algebra.interval.html#5d6177042cf2728bb3a48ad4d7fef36d"><span class="id" title="notation">),</span></a> <a class="idref" href="mathcomp.algebra.interval.html#5d6177042cf2728bb3a48ad4d7fef36d"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.algebra.interval.html#5d6177042cf2728bb3a48ad4d7fef36d"><span class="id" title="notation">)[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="oppr_itvco"><span class="id" title="lemma">oppr_itvco</span></a> (<span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">`[</span></a><a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">`](</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">),</span></a> <a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">)]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="oppr_itvoc"><span class="id" title="lemma">oppr_itvoc</span></a> (<span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">`]</span></a><a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="mathcomp.algebra.interval.html#9776a398e1a32aa2aa525fec3dcf7a09"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">`[(</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">),</span></a> <a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.algebra.interval.html#e13694bd4c96b2ebd74cba5937d97bac"><span class="id" title="notation">)[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="oppr_itvcc"><span class="id" title="lemma">oppr_itvcc</span></a> (<span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo.R"><span class="id" title="variable">R</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">`[</span></a><a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">`[(</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">),</span></a> <a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.algebra.interval.html#0d2438566c38b95c9bc6204c40c6c9af"><span class="id" title="notation">)]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.interval.html#IntervalPo"><span class="id" title="section">IntervalPo</span></a>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="BOpen"><span class="id" title="abbreviation">BOpen</span></a> := (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>).<br/>
<span class="id" title="keyword">Notation</span> <a name="BClose"><span class="id" title="abbreviation">BClose</span></a> := (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>).<br/>
<span class="id" title="keyword">Notation</span> <a name="1b23dabf87b87c155f5c39a03cf252fd"><span class="id" title="notation">&quot;</span></a>`[ a , b ]" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <span class="id" title="var">a</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <span class="id" title="var">b</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">a</span>, <span class="id" title="var">b</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`[ a ,  b ]") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="cbbc44194330d5df3c5926da24c44c66"><span class="id" title="notation">&quot;</span></a>`] a , b ]" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <span class="id" title="var">a</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <span class="id" title="var">b</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">a</span>, <span class="id" title="var">b</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`] a ,  b ]") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="7f598a2ea63782d9411311b8a5b31ec4"><span class="id" title="notation">&quot;</span></a>`[ a , b [" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <span class="id" title="var">a</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <span class="id" title="var">b</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">a</span>, <span class="id" title="var">b</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`[ a ,  b [") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="2e8617f61b689dc49fc99a5898babaf3"><span class="id" title="notation">&quot;</span></a>`] a , b [" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <span class="id" title="var">a</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <span class="id" title="var">b</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">a</span>, <span class="id" title="var">b</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`] a ,  b [") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="f98d6dca6f228c955e58f5882c1f46dd"><span class="id" title="notation">&quot;</span></a>`] '-oo' , b ]" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <span class="id" title="var">b</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">b</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`] '-oo' ,  b ]") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="b76159d3095994358e02438cbda0e8dc"><span class="id" title="notation">&quot;</span></a>`] '-oo' , b [" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <span class="id" title="var">b</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">b</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`] '-oo' ,  b [") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="5c418f5a1d748d89694d4fdc12d0e150"><span class="id" title="notation">&quot;</span></a>`[ a , '+oo' [" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BClose"><span class="id" title="abbreviation">BClose</span></a> <span class="id" title="var">a</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">a</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`[ a ,  '+oo' [") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="e96e2d5a7b2075039ce29a159daa96fc"><span class="id" title="notation">&quot;</span></a>`] a , '+oo' [" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <span class="id" title="var">a</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">a</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9 , <span class="id" title="var">format</span> "`] a ,  '+oo' [") : <span class="id" title="var">ring_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="3495087d2de1936e210dc1e87cddee5f"><span class="id" title="notation">&quot;</span></a>`] -oo , '+oo' [" := (<a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="mathcomp.algebra.interval.html#BInfty"><span class="id" title="constructor">BInfty</span></a> <span class="id" title="var">_</span>))<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "`] -oo ,  '+oo' [") : <span class="id" title="var">ring_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="bec03331256891011ac5a0ab95580e68"><span class="id" title="notation">&quot;</span></a>x &lt;= y ?&lt; 'if' b" := (<a class="idref" href="mathcomp.algebra.interval.html#lersif"><span class="id" title="definition">lersif</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">b</span>)<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">y</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>,<br/>
&nbsp;&nbsp;<span class="id" title="var">format</span> "x '[hv'  &lt;=  y '/'  ?&lt;  'if'  b ']'") : <span class="id" title="var">ring_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="IntervalOrdered"><span class="id" title="section">IntervalOrdered</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variable</span> <a name="IntervalOrdered.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssrnum.html#Num.RealDomain.Exports.realDomainType"><span class="id" title="abbreviation">realDomainType</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="lersifN"><span class="id" title="lemma">lersifN</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalOrdered.R"><span class="id" title="variable">R</span></a>) <span class="id" title="var">b</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bec03331256891011ac5a0ab95580e68"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bec03331256891011ac5a0ab95580e68"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bec03331256891011ac5a0ab95580e68"><span class="id" title="notation">if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bec03331256891011ac5a0ab95580e68"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bec03331256891011ac5a0ab95580e68"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bec03331256891011ac5a0ab95580e68"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="itv_splitU"><span class="id" title="lemma">itv_splitU</span></a> (<span class="id" title="var">xc</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalOrdered.R"><span class="id" title="variable">R</span></a>) <span class="id" title="var">bc</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="mathcomp.algebra.interval.html#xc"><span class="id" title="variable">xc</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bc"><span class="id" title="variable">bc</span></a>) <a class="idref" href="mathcomp.algebra.interval.html#xc"><span class="id" title="variable">xc</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bc"><span class="id" title="variable">bc</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xc"><span class="id" title="variable">xc</span></a>) <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="itv_splitU2"><span class="id" title="lemma">itv_splitU2</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalOrdered.R"><span class="id" title="variable">R</span></a>) <span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#61dc88e70df6fc30a5b49c217ac7b79d"><span class="id" title="notation">[||</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#61dc88e70df6fc30a5b49c217ac7b79d"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> <a class="idref" href="mathcomp.algebra.interval.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#61dc88e70df6fc30a5b49c217ac7b79d"><span class="id" title="notation">),</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#61dc88e70df6fc30a5b49c217ac7b79d"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#61dc88e70df6fc30a5b49c217ac7b79d"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#61dc88e70df6fc30a5b49c217ac7b79d"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#61dc88e70df6fc30a5b49c217ac7b79d"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen"><span class="id" title="abbreviation">BOpen</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.algebra.interval.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#61dc88e70df6fc30a5b49c217ac7b79d"><span class="id" title="notation">)]</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.interval.html#IntervalOrdered"><span class="id" title="section">IntervalOrdered</span></a>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="IntervalField"><span class="id" title="section">IntervalField</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variable</span> <a name="IntervalField.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssrnum.html#Num.RealField.Exports.realFieldType"><span class="id" title="abbreviation">realFieldType</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="mid_in_itv"><span class="id" title="lemma">mid_in_itv</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">ba</span> <span class="id" title="var">bb</span> (<span class="id" title="var">xa</span> <span class="id" title="var">xb</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalField.R"><span class="id" title="variable">R</span></a>), <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bec03331256891011ac5a0ab95580e68"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bec03331256891011ac5a0ab95580e68"><span class="id" title="notation">?&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bec03331256891011ac5a0ab95580e68"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bec03331256891011ac5a0ab95580e68"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.interval.html#ba"><span class="id" title="variable">ba</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bb"><span class="id" title="variable">bb</span></a><a class="idref" href="mathcomp.algebra.interval.html#bec03331256891011ac5a0ab95580e68"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.interval.html#mid"><span class="id" title="abbreviation">mid</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#Interval"><span class="id" title="constructor">Interval</span></a> (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#ba"><span class="id" title="variable">ba</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a>) (<a class="idref" href="mathcomp.algebra.interval.html#BOpen_if"><span class="id" title="constructor">BOpen_if</span></a> <a class="idref" href="mathcomp.algebra.interval.html#bb"><span class="id" title="variable">bb</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a>).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="mid_in_itvoo"><span class="id" title="lemma">mid_in_itvoo</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">xa</span> <span class="id" title="var">xb</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalField.R"><span class="id" title="variable">R</span></a>), <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#388c172bf8d34ef0bf11898cd56f8d7b"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.interval.html#mid"><span class="id" title="abbreviation">mid</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#2e8617f61b689dc49fc99a5898babaf3"><span class="id" title="notation">`]</span></a><a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a><a class="idref" href="mathcomp.algebra.interval.html#2e8617f61b689dc49fc99a5898babaf3"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a><a class="idref" href="mathcomp.algebra.interval.html#2e8617f61b689dc49fc99a5898babaf3"><span class="id" title="notation">[</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="mid_in_itvcc"><span class="id" title="lemma">mid_in_itvcc</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">xa</span> <span class="id" title="var">xb</span> : <a class="idref" href="mathcomp.algebra.interval.html#IntervalField.R"><span class="id" title="variable">R</span></a>), <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#1065783963a393d1eafa2137291f2495"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.interval.html#mid"><span class="id" title="abbreviation">mid</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.interval.html#1b23dabf87b87c155f5c39a03cf252fd"><span class="id" title="notation">`[</span></a><a class="idref" href="mathcomp.algebra.interval.html#xa"><span class="id" title="variable">xa</span></a><a class="idref" href="mathcomp.algebra.interval.html#1b23dabf87b87c155f5c39a03cf252fd"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.interval.html#xb"><span class="id" title="variable">xb</span></a><a class="idref" href="mathcomp.algebra.interval.html#1b23dabf87b87c155f5c39a03cf252fd"><span class="id" title="notation">]</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.interval.html#IntervalField"><span class="id" title="section">IntervalField</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>