<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<title>Flocq.Core.Fcore_Zaux</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library Flocq.Core.Fcore_Zaux</h1>
<div class="code">
</div>
<div class="doc">
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
<div class="paragraph"> </div>
Copyright (C) 2011-2013 Sylvie Boldo
<br />
Copyright (C) 2011-2013 Guillaume Melquiond
<div class="paragraph"> </div>
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
<div class="paragraph"> </div>
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.ZArith.html#"><span class="id" title="library">ZArith</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zquot.html#"><span class="id" title="library">Zquot</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Zmissing"><span class="id" title="section">Zmissing</span></a>.<br/>
<br/>
</div>
<div class="doc">
About Z
</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a name="Zopp_le_cancel"><span class="id" title="lemma">Zopp_le_cancel</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>,<br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zle"><span class="id" title="abbreviation">Zle</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zgt_not_eq"><span class="id" title="lemma">Zgt_not_eq</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>,<br/>
(<a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zmissing"><span class="id" title="section">Zmissing</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Proof_Irrelevance"><span class="id" title="section">Proof_Irrelevance</span></a>.<br/>
<br/>
<span class="id" title="keyword">Scheme</span> <a name="eq_dep_elim"><span class="id" title="definition">eq_dep_elim</span></a> := <span class="id" title="keyword">Induction</span> <span class="id" title="keyword">for</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#eq"><span class="id" title="inductive">eq</span></a> <span class="id" title="keyword">Sort</span> <span class="id" title="keyword">Type</span>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="eqbool_dep"><span class="id" title="definition">eqbool_dep</span></a> <span class="id" title="var">P</span> (<span class="id" title="var">h1</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>) <span class="id" title="var">b</span> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <span class="id" title="keyword">return</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> ⇒ <span class="id" title="keyword">fun</span> (<span class="id" title="var">h2</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>) ⇒ <a class="idref" href="Flocq.Core.Fcore_Zaux.html#h1"><span class="id" title="variable">h1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#h2"><span class="id" title="variable">h2</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> ⇒ <span class="id" title="keyword">fun</span> (<span class="id" title="var">h2</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>) ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#False"><span class="id" title="inductive">False</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="eqbool_irrelevance"><span class="id" title="lemma">eqbool_irrelevance</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">b</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>) (<span class="id" title="var">h1</span> <span class="id" title="var">h2</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>), <a class="idref" href="Flocq.Core.Fcore_Zaux.html#h1"><span class="id" title="variable">h1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#h2"><span class="id" title="variable">h2</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Proof_Irrelevance"><span class="id" title="section">Proof_Irrelevance</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Even_Odd"><span class="id" title="section">Even_Odd</span></a>.<br/>
<br/>
</div>
<div class="doc">
Zeven, used for rounding to nearest, ties to even
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a name="Zeven"><span class="id" title="definition">Zeven</span></a> (<span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>) :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xO"><span class="id" title="constructor">xO</span></a> <span class="id" title="var">_</span>) ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zneg"><span class="id" title="constructor">Zneg</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xO"><span class="id" title="constructor">xO</span></a> <span class="id" title="var">_</span>) ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><br/>
| <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zeven_mult"><span class="id" title="lemma">Zeven_mult</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#orb"><span class="id" title="definition">orb</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zeven_opp"><span class="id" title="lemma">Zeven_opp</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zeven_ex"><span class="id" title="lemma">Zeven_ex</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">p</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <span class="id" title="keyword">if</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">then</span> 0 <span class="id" title="keyword">else</span> 1)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zeven_2xp1"><span class="id" title="lemma">Zeven_2xp1</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span>, <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> (2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zeven_plus"><span class="id" title="lemma">Zeven_plus</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Bool.Bool.html#eqb"><span class="id" title="definition">Bool.eqb</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>).<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Even_Odd"><span class="id" title="section">Even_Odd</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Zpower"><span class="id" title="section">Zpower</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zpower_plus"><span class="id" title="lemma">Zpower_plus</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k1</span> <span class="id" title="var">k2</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#k1"><span class="id" title="variable">k1</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#k2"><span class="id" title="variable">k2</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#k1"><span class="id" title="variable">k1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#k2"><span class="id" title="variable">k2</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#k1"><span class="id" title="variable">k1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#k2"><span class="id" title="variable">k2</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zpower_Zpower_nat"><span class="id" title="lemma">Zpower_Zpower_nat</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">b</span> <span class="id" title="var">e</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e"><span class="id" title="variable">e</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpower.html#Zpower_nat"><span class="id" title="definition">Zpower_nat</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zabs_nat"><span class="id" title="abbreviation">Zabs_nat</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e"><span class="id" title="variable">e</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zpower_nat_S"><span class="id" title="lemma">Zpower_nat_S</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">b</span> <span class="id" title="var">e</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpower.html#Zpower_nat"><span class="id" title="definition">Zpower_nat</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e"><span class="id" title="variable">e</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpower.html#Zpower_nat"><span class="id" title="definition">Zpower_nat</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e"><span class="id" title="variable">e</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zpower_pos_gt_0"><span class="id" title="lemma">Zpower_pos_gt_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">b</span> <span class="id" title="var">p</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower_pos"><span class="id" title="abbreviation">Zpower_pos</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#p"><span class="id" title="variable">p</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zeven_Zpower"><span class="id" title="lemma">Zeven_Zpower</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">b</span> <span class="id" title="var">e</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e"><span class="id" title="variable">e</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e"><span class="id" title="variable">e</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zeven_Zpower_odd"><span class="id" title="lemma">Zeven_Zpower_odd</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">b</span> <span class="id" title="var">e</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e"><span class="id" title="variable">e</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeven"><span class="id" title="definition">Zeven</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e"><span class="id" title="variable">e</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<br/>
</div>
<div class="doc">
The radix must be greater than 1
</div>
<div class="code">
<span class="id" title="keyword">Record</span> <a name="radix"><span class="id" title="record">radix</span></a> := { <a name="radix_val"><span class="id" title="projection">radix_val</span></a> :> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> ; <a name="radix_prop"><span class="id" title="projection">radix_prop</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zle_bool"><span class="id" title="abbreviation">Zle_bool</span></a> 2 <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix_val"><span class="id" title="method">radix_val</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> }.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="radix_val_inj"><span class="id" title="lemma">radix_val_inj</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">r1</span> <span class="id" title="var">r2</span>, <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix_val"><span class="id" title="projection">radix_val</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#r1"><span class="id" title="variable">r1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix_val"><span class="id" title="projection">radix_val</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#r2"><span class="id" title="variable">r2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#r1"><span class="id" title="variable">r1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#r2"><span class="id" title="variable">r2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="radix2"><span class="id" title="definition">radix2</span></a> := <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Build_radix"><span class="id" title="constructor">Build_radix</span></a> 2 (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#refl_equal"><span class="id" title="abbreviation">refl_equal</span></a> <span class="id" title="var">_</span>).<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Zpower.r"><span class="id" title="variable">r</span></a> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix"><span class="id" title="record">radix</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="radix_gt_0"><span class="id" title="lemma">radix_gt_0</span></a> : (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpower.r"><span class="id" title="variable">r</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="radix_gt_1"><span class="id" title="lemma">radix_gt_1</span></a> : (1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpower.r"><span class="id" title="variable">r</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zpower_gt_1"><span class="id" title="lemma">Zpower_gt_1</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">p</span>,<br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#p"><span class="id" title="variable">p</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(1 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpower.r"><span class="id" title="variable">r</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#p"><span class="id" title="variable">p</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zpower_gt_0"><span class="id" title="lemma">Zpower_gt_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">p</span>,<br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#p"><span class="id" title="variable">p</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpower.r"><span class="id" title="variable">r</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#p"><span class="id" title="variable">p</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zpower_ge_0"><span class="id" title="lemma">Zpower_ge_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">e</span>,<br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpower.r"><span class="id" title="variable">r</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e"><span class="id" title="variable">e</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zpower_le"><span class="id" title="lemma">Zpower_le</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">e1</span> <span class="id" title="var">e2</span>, (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#e1"><span class="id" title="variable">e1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e2"><span class="id" title="variable">e2</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpower.r"><span class="id" title="variable">r</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e1"><span class="id" title="variable">e1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpower.r"><span class="id" title="variable">r</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e2"><span class="id" title="variable">e2</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zpower_lt"><span class="id" title="lemma">Zpower_lt</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">e1</span> <span class="id" title="var">e2</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e2"><span class="id" title="variable">e2</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#e1"><span class="id" title="variable">e1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e2"><span class="id" title="variable">e2</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpower.r"><span class="id" title="variable">r</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e1"><span class="id" title="variable">e1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpower.r"><span class="id" title="variable">r</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e2"><span class="id" title="variable">e2</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zpower_lt_Zpower"><span class="id" title="lemma">Zpower_lt_Zpower</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">e1</span> <span class="id" title="var">e2</span>,<br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpower.r"><span class="id" title="variable">r</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#e1"><span class="id" title="variable">e1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpower.r"><span class="id" title="variable">r</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e2"><span class="id" title="variable">e2</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="Flocq.Core.Fcore_Zaux.html#e1"><span class="id" title="variable">e1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e2"><span class="id" title="variable">e2</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpower"><span class="id" title="section">Zpower</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Div_Mod"><span class="id" title="section">Div_Mod</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zmod_mod_mult"><span class="id" title="lemma">Zmod_mod_mult</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zmod"><span class="id" title="abbreviation">Zmod</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zmod"><span class="id" title="abbreviation">Zmod</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>)) <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zmod"><span class="id" title="abbreviation">Zmod</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="ZOmod_eq"><span class="id" title="lemma">ZOmod_eq</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.rem"><span class="id" title="definition">Z.rem</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.quot"><span class="id" title="definition">Z.quot</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="ZOmod_mod_mult"><span class="id" title="lemma">ZOmod_mod_mult</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.rem"><span class="id" title="definition">Z.rem</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.rem"><span class="id" title="definition">Z.rem</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>)) <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.rem"><span class="id" title="definition">Z.rem</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdiv_mod_mult"><span class="id" title="lemma">Zdiv_mod_mult</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zdiv"><span class="id" title="abbreviation">Zdiv</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zmod"><span class="id" title="abbreviation">Zmod</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>)) <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zmod"><span class="id" title="abbreviation">Zmod</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zdiv"><span class="id" title="abbreviation">Zdiv</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a>) <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="ZOdiv_mod_mult"><span class="id" title="lemma">ZOdiv_mod_mult</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.quot"><span class="id" title="definition">Z.quot</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.rem"><span class="id" title="definition">Z.rem</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>)) <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.rem"><span class="id" title="definition">Z.rem</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.quot"><span class="id" title="definition">Z.quot</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a>) <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="ZOdiv_small_abs"><span class="id" title="lemma">ZOdiv_small_abs</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>,<br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zabs"><span class="id" title="abbreviation">Zabs</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.quot"><span class="id" title="definition">Z.quot</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="ZOmod_small_abs"><span class="id" title="lemma">ZOmod_small_abs</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>,<br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zabs"><span class="id" title="abbreviation">Zabs</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.rem"><span class="id" title="definition">Z.rem</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="ZOdiv_plus"><span class="id" title="lemma">ZOdiv_plus</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">c</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.quot"><span class="id" title="definition">Z.quot</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>) <a class="idref" href="Flocq.Core.Fcore_Zaux.html#c"><span class="id" title="variable">c</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.quot"><span class="id" title="definition">Z.quot</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#c"><span class="id" title="variable">c</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.quot"><span class="id" title="definition">Z.quot</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#c"><span class="id" title="variable">c</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.quot"><span class="id" title="definition">Z.quot</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.rem"><span class="id" title="definition">Z.rem</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#c"><span class="id" title="variable">c</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.rem"><span class="id" title="definition">Z.rem</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#c"><span class="id" title="variable">c</span></a>) <a class="idref" href="Flocq.Core.Fcore_Zaux.html#c"><span class="id" title="variable">c</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Div_Mod"><span class="id" title="section">Div_Mod</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Same_sign"><span class="id" title="section">Same_sign</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zsame_sign_trans"><span class="id" title="lemma">Zsame_sign_trans</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">v</span> <span class="id" title="var">u</span> <span class="id" title="var">w</span>, <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#w"><span class="id" title="variable">w</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#w"><span class="id" title="variable">w</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zsame_sign_trans_weak"><span class="id" title="lemma">Zsame_sign_trans_weak</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">v</span> <span class="id" title="var">u</span> <span class="id" title="var">w</span>, <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#w"><span class="id" title="variable">w</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#w"><span class="id" title="variable">w</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#w"><span class="id" title="variable">w</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zsame_sign_imp"><span class="id" title="lemma">Zsame_sign_imp</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">u</span> <span class="id" title="var">v</span>,<br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zsame_sign_odiv"><span class="id" title="lemma">Zsame_sign_odiv</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">u</span> <span class="id" title="var">v</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.quot"><span class="id" title="definition">Z.quot</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Same_sign"><span class="id" title="section">Same_sign</span></a>.<br/>
<br/>
</div>
<div class="doc">
Boolean comparisons
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Section</span> <a name="Zeq_bool"><span class="id" title="section">Zeq_bool</span></a>.<br/>
<br/>
<span class="id" title="keyword">Inductive</span> <a name="Zeq_bool_prop"><span class="id" title="inductive">Zeq_bool_prop</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
| <a name="Zeq_bool_true_"><span class="id" title="constructor">Zeq_bool_true_</span></a> : <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeq_bool_prop"><span class="id" title="inductive">Zeq_bool_prop</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><br/>
| <a name="Zeq_bool_false_"><span class="id" title="constructor">Zeq_bool_false_</span></a> : <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeq_bool_prop"><span class="id" title="inductive">Zeq_bool_prop</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zeq_bool_spec"><span class="id" title="lemma">Zeq_bool_spec</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeq_bool_prop"><span class="id" title="inductive">Zeq_bool_prop</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zeq_bool"><span class="id" title="definition">Zeq_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zeq_bool_true"><span class="id" title="lemma">Zeq_bool_true</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zeq_bool"><span class="id" title="definition">Zeq_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zeq_bool_false"><span class="id" title="lemma">Zeq_bool_false</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zeq_bool"><span class="id" title="definition">Zeq_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zeq_bool"><span class="id" title="section">Zeq_bool</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Zle_bool"><span class="id" title="section">Zle_bool</span></a>.<br/>
<br/>
<span class="id" title="keyword">Inductive</span> <a name="Zle_bool_prop"><span class="id" title="inductive">Zle_bool_prop</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
| <a name="Zle_bool_true_"><span class="id" title="constructor">Zle_bool_true_</span></a> : (<span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <span class="id" title="var">y</span>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zle_bool_prop"><span class="id" title="inductive">Zle_bool_prop</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><br/>
| <a name="Zle_bool_false_"><span class="id" title="constructor">Zle_bool_false_</span></a> : (<span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <span class="id" title="var">x</span>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zle_bool_prop"><span class="id" title="inductive">Zle_bool_prop</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zle_bool_spec"><span class="id" title="lemma">Zle_bool_spec</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zle_bool_prop"><span class="id" title="inductive">Zle_bool_prop</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zle_bool"><span class="id" title="abbreviation">Zle_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zle_bool_true"><span class="id" title="lemma">Zle_bool_true</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>,<br/>
(<a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zle_bool"><span class="id" title="abbreviation">Zle_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zle_bool_false"><span class="id" title="lemma">Zle_bool_false</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>,<br/>
(<a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zle_bool"><span class="id" title="abbreviation">Zle_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zle_bool"><span class="id" title="section">Zle_bool</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Zlt_bool"><span class="id" title="section">Zlt_bool</span></a>.<br/>
<br/>
<span class="id" title="keyword">Inductive</span> <a name="Zlt_bool_prop"><span class="id" title="inductive">Zlt_bool_prop</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
| <a name="Zlt_bool_true_"><span class="id" title="constructor">Zlt_bool_true_</span></a> : (<span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <span class="id" title="var">y</span>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zlt_bool_prop"><span class="id" title="inductive">Zlt_bool_prop</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><br/>
| <a name="Zlt_bool_false_"><span class="id" title="constructor">Zlt_bool_false_</span></a> : (<span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <span class="id" title="var">x</span>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zlt_bool_prop"><span class="id" title="inductive">Zlt_bool_prop</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zlt_bool_spec"><span class="id" title="lemma">Zlt_bool_spec</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zlt_bool_prop"><span class="id" title="inductive">Zlt_bool_prop</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zlt_bool"><span class="id" title="abbreviation">Zlt_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zlt_bool_true"><span class="id" title="lemma">Zlt_bool_true</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>,<br/>
(<a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zlt_bool"><span class="id" title="abbreviation">Zlt_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zlt_bool_false"><span class="id" title="lemma">Zlt_bool_false</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>,<br/>
(<a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zlt_bool"><span class="id" title="abbreviation">Zlt_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="negb_Zle_bool"><span class="id" title="lemma">negb_Zle_bool</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#negb"><span class="id" title="definition">negb</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zle_bool"><span class="id" title="abbreviation">Zle_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zlt_bool"><span class="id" title="abbreviation">Zlt_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="negb_Zlt_bool"><span class="id" title="lemma">negb_Zlt_bool</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#negb"><span class="id" title="definition">negb</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zlt_bool"><span class="id" title="abbreviation">Zlt_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zle_bool"><span class="id" title="abbreviation">Zle_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zlt_bool"><span class="id" title="section">Zlt_bool</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Zcompare"><span class="id" title="section">Zcompare</span></a>.<br/>
<br/>
<span class="id" title="keyword">Inductive</span> <a name="Zcompare_prop"><span class="id" title="inductive">Zcompare_prop</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#comparison"><span class="id" title="inductive">comparison</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
| <a name="Zcompare_Lt_"><span class="id" title="constructor">Zcompare_Lt_</span></a> : (<span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <span class="id" title="var">y</span>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zcompare_prop"><span class="id" title="inductive">Zcompare_prop</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a><br/>
| <a name="Zcompare_Eq_"><span class="id" title="constructor">Zcompare_Eq_</span></a> : <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zcompare_prop"><span class="id" title="inductive">Zcompare_prop</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Eq"><span class="id" title="constructor">Eq</span></a><br/>
| <a name="Zcompare_Gt_"><span class="id" title="constructor">Zcompare_Gt_</span></a> : (<span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <span class="id" title="var">x</span>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zcompare_prop"><span class="id" title="inductive">Zcompare_prop</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Gt"><span class="id" title="constructor">Gt</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zcompare_spec"><span class="id" title="lemma">Zcompare_spec</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zcompare_prop"><span class="id" title="inductive">Zcompare_prop</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zcompare"><span class="id" title="abbreviation">Zcompare</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zcompare_Lt"><span class="id" title="lemma">Zcompare_Lt</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/>
(<a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zcompare"><span class="id" title="abbreviation">Zcompare</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zcompare_Eq"><span class="id" title="lemma">Zcompare_Eq</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/>
(<a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zcompare"><span class="id" title="abbreviation">Zcompare</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Eq"><span class="id" title="constructor">Eq</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zcompare_Gt"><span class="id" title="lemma">Zcompare_Gt</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/>
(<a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zcompare"><span class="id" title="abbreviation">Zcompare</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Gt"><span class="id" title="constructor">Gt</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zcompare"><span class="id" title="section">Zcompare</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="cond_Zopp"><span class="id" title="section">cond_Zopp</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="cond_Zopp"><span class="id" title="definition">cond_Zopp</span></a> (<span class="id" title="var">b</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>) <span class="id" title="var">m</span> := <span class="id" title="keyword">if</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zopp"><span class="id" title="abbreviation">Zopp</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#m"><span class="id" title="variable">m</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#m"><span class="id" title="variable">m</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="abs_cond_Zopp"><span class="id" title="lemma">abs_cond_Zopp</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">b</span> <span class="id" title="var">m</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zabs"><span class="id" title="abbreviation">Zabs</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#cond_Zopp"><span class="id" title="definition">cond_Zopp</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#m"><span class="id" title="variable">m</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zabs"><span class="id" title="abbreviation">Zabs</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#m"><span class="id" title="variable">m</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="cond_Zopp_Zlt_bool"><span class="id" title="lemma">cond_Zopp_Zlt_bool</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_Zaux.html#cond_Zopp"><span class="id" title="definition">cond_Zopp</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zlt_bool"><span class="id" title="abbreviation">Zlt_bool</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#m"><span class="id" title="variable">m</span></a> 0) <a class="idref" href="Flocq.Core.Fcore_Zaux.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zabs"><span class="id" title="abbreviation">Zabs</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#m"><span class="id" title="variable">m</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#cond_Zopp"><span class="id" title="section">cond_Zopp</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="fast_pow_pos"><span class="id" title="section">fast_pow_pos</span></a>.<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a name="Zfast_pow_pos"><span class="id" title="definition">Zfast_pow_pos</span></a> (<span class="id" title="var">v</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>) (<span class="id" title="var">e</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#positive"><span class="id" title="inductive">positive</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</span></a> ⇒ <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xO"><span class="id" title="constructor">xO</span></a> <span class="id" title="var">e'</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.square"><span class="id" title="definition">Z.square</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zfast_pow_pos"><span class="id" title="definition">Zfast_pow_pos</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a> <span class="id" title="var">e'</span>)<br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xI"><span class="id" title="constructor">xI</span></a> <span class="id" title="var">e'</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zmult"><span class="id" title="abbreviation">Zmult</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.square"><span class="id" title="definition">Z.square</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zfast_pow_pos"><span class="id" title="definition">Zfast_pow_pos</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a> <span class="id" title="var">e'</span>))<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zfast_pow_pos_correct"><span class="id" title="lemma">Zfast_pow_pos_correct</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">v</span> <span class="id" title="var">e</span>, <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zfast_pow_pos"><span class="id" title="definition">Zfast_pow_pos</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower_pos"><span class="id" title="abbreviation">Zpower_pos</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#e"><span class="id" title="variable">e</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#fast_pow_pos"><span class="id" title="section">fast_pow_pos</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="faster_div"><span class="id" title="section">faster_div</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="Zdiv_eucl_unique"><span class="id" title="lemma">Zdiv_eucl_unique</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zdiv_eucl"><span class="id" title="abbreviation">Zdiv_eucl</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zdiv"><span class="id" title="abbreviation">Zdiv</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zmod"><span class="id" title="abbreviation">Zmod</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a name="Zpos_div_eucl_aux1"><span class="id" title="definition">Zpos_div_eucl_aux1</span></a> (<span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#positive"><span class="id" title="inductive">positive</span></a>) {<span class="id" title="keyword">struct</span> <span class="id" title="var">b</span>} :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xO"><span class="id" title="constructor">xO</span></a> <span class="id" title="var">b'</span> ⇒<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xO"><span class="id" title="constructor">xO</span></a> <span class="id" title="var">a'</span> ⇒ <span class="id" title="keyword">let</span> (<span class="id" title="var">q</span>, <span class="id" title="var">r</span>) := <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpos_div_eucl_aux1"><span class="id" title="definition">Zpos_div_eucl_aux1</span></a> <span class="id" title="var">a'</span> <span class="id" title="var">b'</span> <span class="id" title="keyword">in</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> 2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#r"><span class="id" title="variable">r</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xI"><span class="id" title="constructor">xI</span></a> <span class="id" title="var">a'</span> ⇒ <span class="id" title="keyword">let</span> (<span class="id" title="var">q</span>, <span class="id" title="var">r</span>) := <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpos_div_eucl_aux1"><span class="id" title="definition">Zpos_div_eucl_aux1</span></a> <span class="id" title="var">a'</span> <span class="id" title="var">b'</span> <span class="id" title="keyword">in</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> 2 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/>
<span class="id" title="keyword">end</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xI"><span class="id" title="constructor">xI</span></a> <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.pos_div_eucl"><span class="id" title="definition">Z.pos_div_eucl</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>)<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="Zpos_div_eucl_aux1_correct"><span class="id" title="lemma">Zpos_div_eucl_aux1_correct</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpos_div_eucl_aux1"><span class="id" title="definition">Zpos_div_eucl_aux1</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.pos_div_eucl"><span class="id" title="definition">Z.pos_div_eucl</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="Zpos_div_eucl_aux"><span class="id" title="definition">Zpos_div_eucl_aux</span></a> (<span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#positive"><span class="id" title="inductive">positive</span></a>) :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.PArith.BinPos.html#Pos.compare"><span class="id" title="definition">Pos.compare</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Lt"><span class="id" title="constructor">Lt</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Eq"><span class="id" title="constructor">Eq</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a>1%<span class="id" title="var">Z</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#Gt"><span class="id" title="constructor">Gt</span></a> ⇒ <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpos_div_eucl_aux1"><span class="id" title="definition">Zpos_div_eucl_aux1</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="Zpos_div_eucl_aux_correct"><span class="id" title="lemma">Zpos_div_eucl_aux_correct</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpos_div_eucl_aux"><span class="id" title="definition">Zpos_div_eucl_aux</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z.pos_div_eucl"><span class="id" title="definition">Z.pos_div_eucl</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="Zfast_div_eucl"><span class="id" title="definition">Zfast_div_eucl</span></a> (<span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>) :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a>0<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">a'</span> ⇒<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a>0<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">b'</span> ⇒ <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpos_div_eucl_aux"><span class="id" title="definition">Zpos_div_eucl_aux</span></a> <span class="id" title="var">a'</span> <span class="id" title="var">b'</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zneg"><span class="id" title="constructor">Zneg</span></a> <span class="id" title="var">b'</span> ⇒<br/>
<span class="id" title="keyword">let</span> (<span class="id" title="var">q</span>, <span class="id" title="var">r</span>) := <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpos_div_eucl_aux"><span class="id" title="definition">Zpos_div_eucl_aux</span></a> <span class="id" title="var">a'</span> <span class="id" title="var">b'</span> <span class="id" title="keyword">in</span><br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#r"><span class="id" title="variable">r</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-(</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#r"><span class="id" title="variable">r</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">))</span></a>%<span class="id" title="var">Z</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zneg"><span class="id" title="constructor">Zneg</span></a> <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-(</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#r"><span class="id" title="variable">r</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">))</span></a>%<span class="id" title="var">Z</span><br/>
<span class="id" title="keyword">end</span><br/>
<span class="id" title="keyword">end</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zneg"><span class="id" title="constructor">Zneg</span></a> <span class="id" title="var">a'</span> ⇒<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a>0<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">b'</span> ⇒<br/>
<span class="id" title="keyword">let</span> (<span class="id" title="var">q</span>, <span class="id" title="var">r</span>) := <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpos_div_eucl_aux"><span class="id" title="definition">Zpos_div_eucl_aux</span></a> <span class="id" title="var">a'</span> <span class="id" title="var">b'</span> <span class="id" title="keyword">in</span><br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#r"><span class="id" title="variable">r</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z0"><span class="id" title="constructor">Z0</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-(</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#r"><span class="id" title="variable">r</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">))</span></a>%<span class="id" title="var">Z</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zneg"><span class="id" title="constructor">Zneg</span></a> <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-(</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#r"><span class="id" title="variable">r</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">))</span></a>%<span class="id" title="var">Z</span><br/>
<span class="id" title="keyword">end</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zneg"><span class="id" title="constructor">Zneg</span></a> <span class="id" title="var">b'</span> ⇒ <span class="id" title="keyword">let</span> (<span class="id" title="var">q</span>, <span class="id" title="var">r</span>) := <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zpos_div_eucl_aux"><span class="id" title="definition">Zpos_div_eucl_aux</span></a> <span class="id" title="var">a'</span> <span class="id" title="var">b'</span> <span class="id" title="keyword">in</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_Zaux.html#r"><span class="id" title="variable">r</span></a>)%<span class="id" title="var">Z</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/>
<span class="id" title="keyword">end</span><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zfast_div_eucl_correct"><span class="id" title="lemma">Zfast_div_eucl_correct</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>,<br/>
<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Zfast_div_eucl"><span class="id" title="definition">Zfast_div_eucl</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zdiv_eucl"><span class="id" title="abbreviation">Zdiv_eucl</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#b"><span class="id" title="variable">b</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#faster_div"><span class="id" title="section">faster_div</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Iter"><span class="id" title="section">Iter</span></a>.<br/>
<br/>
<span class="id" title="keyword">Context</span> {<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>}.<br/>
<span class="id" title="keyword">Variable</span> (<a name="Iter.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter.A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter.A"><span class="id" title="variable">A</span></a>).<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a name="iter_nat"><span class="id" title="definition">iter_nat</span></a> (<span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<span class="id" title="var">x</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter.A"><span class="id" title="variable">A</span></a>) {<span class="id" title="keyword">struct</span> <span class="id" title="var">n</span>} : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter.A"><span class="id" title="variable">A</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">n'</span> ⇒ <a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_nat"><span class="id" title="definition">iter_nat</span></a> <span class="id" title="var">n'</span> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter.f"><span class="id" title="variable">f</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>)<br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> ⇒ <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="iter_nat_plus"><span class="id" title="lemma">iter_nat_plus</span></a> :<br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<span class="id" title="var">x</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter.A"><span class="id" title="variable">A</span></a>),<br/>
<a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_nat"><span class="id" title="definition">iter_nat</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Peano.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#q"><span class="id" title="variable">q</span></a>) <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_nat"><span class="id" title="definition">iter_nat</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#p"><span class="id" title="variable">p</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_nat"><span class="id" title="definition">iter_nat</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>).<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="iter_nat_S"><span class="id" title="lemma">iter_nat_S</span></a> :<br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<span class="id" title="var">x</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter.A"><span class="id" title="variable">A</span></a>),<br/>
<a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_nat"><span class="id" title="definition">iter_nat</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter.f"><span class="id" title="variable">f</span></a> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_nat"><span class="id" title="definition">iter_nat</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>).<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a name="iter_pos"><span class="id" title="definition">iter_pos</span></a> (<span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#positive"><span class="id" title="inductive">positive</span></a>) (<span class="id" title="var">x</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter.A"><span class="id" title="variable">A</span></a>) {<span class="id" title="keyword">struct</span> <span class="id" title="var">n</span>} : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter.A"><span class="id" title="variable">A</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xI"><span class="id" title="constructor">xI</span></a> <span class="id" title="var">n'</span> ⇒ <a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_pos"><span class="id" title="definition">iter_pos</span></a> <span class="id" title="var">n'</span> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_pos"><span class="id" title="definition">iter_pos</span></a> <span class="id" title="var">n'</span> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter.f"><span class="id" title="variable">f</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>))<br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xO"><span class="id" title="constructor">xO</span></a> <span class="id" title="var">n'</span> ⇒ <a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_pos"><span class="id" title="definition">iter_pos</span></a> <span class="id" title="var">n'</span> (<a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_pos"><span class="id" title="definition">iter_pos</span></a> <span class="id" title="var">n'</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>)<br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</span></a> ⇒ <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter.f"><span class="id" title="variable">f</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="iter_pos_nat"><span class="id" title="lemma">iter_pos_nat</span></a> :<br/>
<span class="id" title="keyword">∀</span> (<span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#positive"><span class="id" title="inductive">positive</span></a>) (<span class="id" title="var">x</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter.A"><span class="id" title="variable">A</span></a>),<br/>
<a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_pos"><span class="id" title="definition">iter_pos</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#iter_nat"><span class="id" title="definition">iter_nat</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.PArith.BinPos.html#Pos.to_nat"><span class="id" title="definition">Pos.to_nat</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="Flocq.Core.Fcore_Zaux.html#x"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#Iter"><span class="id" title="section">Iter</span></a>.<br/>
</div>
</div>
<div id="footer">
<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>
distrib
>
Mageia
>
6
>
armv5tl
>
media
>
core-release
>
by-pkgid
>
3c7997fe0e8405f6d7b5563e63d17a78
>
files
>
88
