diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.algebra.interval.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.algebra.interval.html | 425 |
1 files changed, 425 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.algebra.interval.html b/docs/htmldoc/mathcomp.algebra.interval.html new file mode 100644 index 0000000..d10a18d --- /dev/null +++ b/docs/htmldoc/mathcomp.algebra.interval.html @@ -0,0 +1,425 @@ +<!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">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> + Distributed under the terms of CeCILL-B. *)</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 <= y ?< 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> & <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> & <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/> + <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/> + <span class="id" title="keyword">match</span> <span class="id" title="var">l</span> <span class="id" title="keyword">with</span><br/> + | <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"><</span></a> <a class="idref" href="mathcomp.algebra.interval.html#x"><span class="id" title="variable">x</span></a><br/> + | <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/> + | <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/> + <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">&&</span></a><br/> + <span class="id" title="keyword">match</span> <span class="id" title="var">u</span> <span class="id" title="keyword">with</span><br/> + | <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"><</span></a> <span class="id" title="var">b</span><br/> + | <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/> + | <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/> + <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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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/> + <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/> + (<span class="id" title="keyword">match</span> <span class="id" title="var">l</span> <span class="id" title="keyword">with</span><br/> + | <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"><</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/> + | <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"><</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/> + | <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/> + <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/> + <span class="id" title="keyword">match</span> <span class="id" title="var">u</span> <span class="id" title="keyword">with</span><br/> + | <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"><</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/> + | <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"><</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/> + | <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/> + <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/> + <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/> + | <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/> + <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"><</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/> + | <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/> + <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"><</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/> + <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/> + | <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/> + <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"><</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/> + <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/> + | <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/> + <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"><</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/> + <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/> + | <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/> + <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/> + <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/> + (<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/> + | <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/> + | <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"><</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/> + | <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/> + <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/> + <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/> + | <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/> + | <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"><</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/> + | <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/> + <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/> + <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"><</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">?<</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/> + <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">?<</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">?<</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">?<</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">?<</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">?<</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">?<</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"><</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">?<</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">?<</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"><</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">?<</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/> + <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/> + | <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">?<</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">&&</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/> + | <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/> + | <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/> + <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/> + <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/> + | <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">?<</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">&&</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/> + | <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/> + | <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/> + <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/> + <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/> + <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">&&</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/> + <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">==></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/> + <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">==></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/> + <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/> + <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">?<</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/> + <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/> + <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/> + <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/> + <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/> + <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/> + <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/> + | <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">&&</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/> + <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/> + <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/> + <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/> + <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/> + <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/> + <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">?<</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/> + <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"><</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/> + <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"><</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/> + <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">&&</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/> + <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">?<</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">?<</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/> + <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/> + <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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</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/> + (<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">"</span></a>x <= y ?< '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/> + (<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/> + <span class="id" title="var">format</span> "x '[hv' <= y '/' ?< '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">?<</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">?<</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/> + <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/> + <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/> + <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/> + <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/> + <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/> + <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">?<</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/> + <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"><</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>
\ No newline at end of file |