<!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_digits</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library Flocq.Core.Fcore_digits</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/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#"><span class="id" title="library">Fcore_Zaux</span></a>.<br/>
<br/>
</div>
<div class="doc">
Number of bits (radix 2) of a positive integer.
<div class="paragraph"> </div>
It serves as an upper bound on the number of digits to ensure termination.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Fixpoint</span> <a name="digits2_Pnat"><span class="id" title="definition">digits2_Pnat</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>) : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_digits.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#xH"><span class="id" title="constructor">xH</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</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">p</span> ⇒ <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_digits.html#digits2_Pnat"><span class="id" title="definition">digits2_Pnat</span></a> <span class="id" title="var">p</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">p</span> ⇒ <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_digits.html#digits2_Pnat"><span class="id" title="definition">digits2_Pnat</span></a> <span class="id" title="var">p</span>)<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="digits2_Pnat_correct"><span class="id" title="lemma">digits2_Pnat_correct</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span>,<br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">d</span> := <a class="idref" href="Flocq.Core.Fcore_digits.html#digits2_Pnat"><span class="id" title="definition">digits2_Pnat</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">in</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> 2 <a class="idref" href="Flocq.Core.Fcore_digits.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="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_digits.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#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><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> 2 (<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_digits.html#d"><span class="id" title="variable">d</span></a>))%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fcore_digits"><span class="id" title="section">Fcore_digits</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <span class="id" title="keyword">beta</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix"><span class="id" title="record">radix</span></a>.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="Zdigit"><span class="id" title="definition">Zdigit</span></a> <span class="id" title="var">n</span> <span class="id" title="var">k</span> := <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_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>)) <span class="id" title="keyword">beta</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigit_lt"><span class="id" title="lemma">Zdigit_lt</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span>,<br/>
(<a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> 0)%<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_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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="Zdigit_0"><span class="id" title="lemma">Zdigit_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">k</span>, <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> 0 <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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="Zdigit_opp"><span class="id" title="lemma">Zdigit_opp</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</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_digits.html#n"><span class="id" title="variable">n</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigit_ge_Zpower_pos"><span class="id" title="lemma">Zdigit_ge_Zpower_pos</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">e</span> <span class="id" title="var">n</span>,<br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.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/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">k</span>, (<a class="idref" href="Flocq.Core.Fcore_digits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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="Zdigit_ge_Zpower"><span class="id" title="lemma">Zdigit_ge_Zpower</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">e</span> <span class="id" title="var">n</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_digits.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#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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.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/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">k</span>, (<a class="idref" href="Flocq.Core.Fcore_digits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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="Zdigit_not_0_pos"><span class="id" title="lemma">Zdigit_not_0_pos</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">e</span> <span class="id" title="var">n</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_digits.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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><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> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_digits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<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_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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#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>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigit_not_0"><span class="id" title="lemma">Zdigit_not_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">e</span> <span class="id" title="var">n</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_digits.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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><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_digits.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#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><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> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_digits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1))%<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_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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#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>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigit_mul_pow"><span class="id" title="lemma">Zdigit_mul_pow</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span> <span class="id" title="var">k'</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_digits.html#k'"><span class="id" title="variable">k'</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.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#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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigit_div_pow"><span class="id" title="lemma">Zdigit_div_pow</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span> <span class="id" title="var">k'</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_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (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_digits.html#k'"><span class="id" title="variable">k'</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</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_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a>)) <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigit_mod_pow"><span class="id" title="lemma">Zdigit_mod_pow</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span> <span class="id" title="var">k'</span>, (<a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</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_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a>)) <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigit_mod_pow_out"><span class="id" title="lemma">Zdigit_mod_pow_out</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span> <span class="id" title="var">k'</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#5dda7752d319ac2ccefb830f12787952"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#5dda7752d319ac2ccefb830f12787952"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</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_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a>)) <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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">Fixpoint</span> <a name="Zsum_digit"><span class="id" title="definition">Zsum_digit</span></a> <span class="id" title="var">f</span> <span class="id" title="var">k</span> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</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#O"><span class="id" title="constructor">O</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/>
| <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">k</span> ⇒ (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zsum_digit"><span class="id" title="definition">Zsum_digit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#f"><span class="id" title="variable">f</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z_of_nat"><span class="id" title="abbreviation">Z_of_nat</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#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> <span class="id" title="keyword">beta</span> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z_of_nat"><span class="id" title="abbreviation">Z_of_nat</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>))%<span class="id" title="var">Z</span><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zsum_digit_digit"><span class="id" title="lemma">Zsum_digit_digit</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zsum_digit"><span class="id" title="definition">Zsum_digit</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z_of_nat"><span class="id" title="abbreviation">Z_of_nat</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>)).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zpower_gt_id"><span class="id" title="lemma">Zpower_gt_id</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span>, (<a class="idref" href="Flocq.Core.Fcore_digits.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#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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigit_ext"><span class="id" title="lemma">Zdigit_ext</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n1</span> <span class="id" title="var">n2</span>,<br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">k</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_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n1"><span class="id" title="variable">n1</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n2"><span class="id" title="variable">n2</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#n1"><span class="id" title="variable">n1</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_digits.html#n2"><span class="id" title="variable">n2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="ZOmod_plus_pow_digit"><span class="id" title="lemma">ZOmod_plus_pow_digit</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">u</span> <span class="id" title="var">v</span> <span class="id" title="var">n</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_digits.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_digits.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/>
<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">∀</span> <span class="id" title="var">k</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</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_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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/>
<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_digits.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#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#v"><span class="id" title="variable">v</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</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_digits.html#u"><span class="id" title="variable">u</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.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> <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_digits.html#v"><span class="id" title="variable">v</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a>))%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="ZOdiv_plus_pow_digit"><span class="id" title="lemma">ZOdiv_plus_pow_digit</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">u</span> <span class="id" title="var">v</span> <span class="id" title="var">n</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_digits.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_digits.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/>
<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">∀</span> <span class="id" title="var">k</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</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_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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/>
<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_digits.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#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#v"><span class="id" title="variable">v</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</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_digits.html#u"><span class="id" title="variable">u</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.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> <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_digits.html#v"><span class="id" title="variable">v</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a>))%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigit_plus"><span class="id" title="lemma">Zdigit_plus</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_digits.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_digits.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/>
<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">∀</span> <span class="id" title="var">k</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_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">k</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.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#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#v"><span class="id" title="variable">v</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
</div>
<div class="doc">
Left and right shifts
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="Zscale"><span class="id" title="definition">Zscale</span></a> <span class="id" title="var">n</span> <span class="id" title="var">k</span> :=<br/>
<span class="id" title="keyword">if</span> <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> 0 <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <span class="id" title="keyword">then</span> (<a class="idref" href="Flocq.Core.Fcore_digits.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#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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <span class="id" title="keyword">else</span> <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_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="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_digits.html#k"><span class="id" title="variable">k</span></a>)).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigit_scale"><span class="id" title="lemma">Zdigit_scale</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span> <span class="id" title="var">k'</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_digits.html#k'"><span class="id" title="variable">k'</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zscale"><span class="id" title="definition">Zscale</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zscale_0"><span class="id" title="lemma">Zscale_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">k</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zscale"><span class="id" title="definition">Zscale</span></a> 0 <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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="Zsame_sign_scale"><span class="id" title="lemma">Zsame_sign_scale</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span>,<br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zscale"><span class="id" title="definition">Zscale</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zscale_mul_pow"><span class="id" title="lemma">Zscale_mul_pow</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span> <span class="id" title="var">k'</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_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zscale"><span class="id" title="definition">Zscale</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.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#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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zscale"><span class="id" title="definition">Zscale</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zscale_scale"><span class="id" title="lemma">Zscale_scale</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span> <span class="id" title="var">k'</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_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zscale"><span class="id" title="definition">Zscale</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zscale"><span class="id" title="definition">Zscale</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zscale"><span class="id" title="definition">Zscale</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a>).<br/>
<br/>
</div>
<div class="doc">
Slice of an integer
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="Zslice"><span class="id" title="definition">Zslice</span></a> <span class="id" title="var">n</span> <span class="id" title="var">k1</span> <span class="id" title="var">k2</span> :=<br/>
<span class="id" title="keyword">if</span> <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> 0 <a class="idref" href="Flocq.Core.Fcore_digits.html#k2"><span class="id" title="variable">k2</span></a> <span class="id" title="keyword">then</span> <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_digits.html#Zscale"><span class="id" title="definition">Zscale</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><a class="idref" href="Flocq.Core.Fcore_digits.html#k1"><span class="id" title="variable">k1</span></a>)) (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#k2"><span class="id" title="variable">k2</span></a>) <span class="id" title="keyword">else</span> <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="Zdigit_slice"><span class="id" title="lemma">Zdigit_slice</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> <span class="id" title="var">k</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k1"><span class="id" title="variable">k1</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k2"><span class="id" title="variable">k2</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#k"><span class="id" title="variable">k</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigit_slice_out"><span class="id" title="lemma">Zdigit_slice_out</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> <span class="id" title="var">k</span>, (<a class="idref" href="Flocq.Core.Fcore_digits.html#k2"><span class="id" title="variable">k2</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_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k1"><span class="id" title="variable">k1</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k2"><span class="id" title="variable">k2</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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="Zslice_0"><span class="id" title="lemma">Zslice_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">k</span> <span class="id" title="var">k'</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> 0 <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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="Zsame_sign_slice"><span class="id" title="lemma">Zsame_sign_slice</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span> <span class="id" title="var">k'</span>,<br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k'"><span class="id" title="variable">k'</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zslice_slice"><span class="id" title="lemma">Zslice_slice</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> <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#5dda7752d319ac2ccefb830f12787952"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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#5dda7752d319ac2ccefb830f12787952"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k1"><span class="id" title="variable">k1</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k2"><span class="id" title="variable">k2</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k1'"><span class="id" title="variable">k1'</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.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_digits.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#Zmin"><span class="id" title="abbreviation">Zmin</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#k2"><span class="id" title="variable">k2</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_digits.html#k1'"><span class="id" title="variable">k1'</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k2'"><span class="id" title="variable">k2'</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zslice_mul_pow"><span class="id" title="lemma">Zslice_mul_pow</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</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_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.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#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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k1"><span class="id" title="variable">k1</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.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#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k2"><span class="id" title="variable">k2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zslice_div_pow"><span class="id" title="lemma">Zslice_div_pow</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</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_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> (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_digits.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><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</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_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>)) <a class="idref" href="Flocq.Core.Fcore_digits.html#k1"><span class="id" title="variable">k1</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#k"><span class="id" title="variable">k</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k2"><span class="id" title="variable">k2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zslice_scale"><span class="id" title="lemma">Zslice_scale</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</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_digits.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><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zscale"><span class="id" title="definition">Zscale</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k1"><span class="id" title="variable">k1</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.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#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#k2"><span class="id" title="variable">k2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zslice_div_pow_scale"><span class="id" title="lemma">Zslice_div_pow_scale</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</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_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</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_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>)) <a class="idref" href="Flocq.Core.Fcore_digits.html#k1"><span class="id" title="variable">k1</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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="Flocq.Core.Fcore_digits.html#Zscale"><span class="id" title="definition">Zscale</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#k2"><span class="id" title="variable">k2</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_digits.html#k1"><span class="id" title="variable">k1</span></a>).<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zplus_slice"><span class="id" title="lemma">Zplus_slice</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span> <span class="id" title="var">l1</span> <span class="id" title="var">l2</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_digits.html#l1"><span class="id" title="variable">l1</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_digits.html#l2"><span class="id" title="variable">l2</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_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#l1"><span class="id" title="variable">l1</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_digits.html#Zscale"><span class="id" title="definition">Zscale</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#l1"><span class="id" title="variable">l1</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#l2"><span class="id" title="variable">l2</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#l1"><span class="id" title="variable">l1</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#l1"><span class="id" title="variable">l1</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_digits.html#l2"><span class="id" title="variable">l2</span></a>).<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fcore_digits.digits_aux"><span class="id" title="section">digits_aux</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a name="Fcore_digits.digits_aux.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a name="Zdigits_aux"><span class="id" title="definition">Zdigits_aux</span></a> (<span class="id" title="var">nb</span> <span class="id" title="var">pow</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">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="keyword">struct</span> <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_digits.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#O"><span class="id" title="constructor">O</span></a> ⇒ <a class="idref" href="Flocq.Core.Fcore_digits.html#nb"><span class="id" title="variable">nb</span></a><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> ⇒ <span class="id" title="keyword">if</span> <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_digits.html#Fcore_digits.digits_aux.p"><span class="id" title="variable">p</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#pow"><span class="id" title="variable">pow</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#nb"><span class="id" title="variable">nb</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits_aux"><span class="id" title="definition">Zdigits_aux</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#nb"><span class="id" title="variable">nb</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#Zmult"><span class="id" title="abbreviation">Zmult</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#pow"><span class="id" title="variable">pow</span></a>) <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#Fcore_digits.digits_aux"><span class="id" title="section">digits_aux</span></a>.<br/>
<br/>
</div>
<div class="doc">
Number of digits of an integer
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="Zdigits"><span class="id" title="definition">Zdigits</span></a> <span class="id" title="var">n</span> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_digits.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#Z0"><span class="id" title="constructor">Z0</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/>
| <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">p</span> ⇒ <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits_aux"><span class="id" title="definition">Zdigits_aux</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> <span class="id" title="var">p</span>) 1 <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_digits.html#digits2_Pnat"><span class="id" title="definition">digits2_Pnat</span></a> <span class="id" title="var">p</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">p</span> ⇒ <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits_aux"><span class="id" title="definition">Zdigits_aux</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> 1 <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_digits.html#digits2_Pnat"><span class="id" title="definition">digits2_Pnat</span></a> <span class="id" title="var">p</span>)<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigits_correct"><span class="id" title="lemma">Zdigits_correct</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</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> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><span class="id" title="notation">≤</span></a> <a class="idref" href="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_digits.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#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><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> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a>))%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigits_unique"><span class="id" title="lemma">Zdigits_unique</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">d</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> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_digits.html#d"><span class="id" title="variable">d</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#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><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_digits.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#cb2fd1306e4fe5d333fd9fb7e2c4a1d2"><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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#d"><span class="id" title="variable">d</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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</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_digits.html#d"><span class="id" title="variable">d</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigits_abs"><span class="id" title="lemma">Zdigits_abs</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span>, <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</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_digits.html#n"><span class="id" title="variable">n</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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigits_gt_0"><span class="id" title="lemma">Zdigits_gt_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span>, <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</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> (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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigits_ge_0"><span class="id" title="lemma">Zdigits_ge_0</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigit_out"><span class="id" title="lemma">Zdigit_out</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span>, (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="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="Zdigit_digits"><span class="id" title="lemma">Zdigit_digits</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span>, <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</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/>
<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigit"><span class="id" title="definition">Zdigit</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1) <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>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigits_slice"><span class="id" title="lemma">Zdigits_slice</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span> <span class="id" title="var">l</span>, (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#l"><span class="id" title="variable">l</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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#Zslice"><span class="id" title="definition">Zslice</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#l"><span class="id" title="variable">l</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_digits.html#l"><span class="id" title="variable">l</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigits_mult_Zpower"><span class="id" title="lemma">Zdigits_mult_Zpower</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</span> <span class="id" title="var">e</span>,<br/>
<a class="idref" href="Flocq.Core.Fcore_digits.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#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> (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_digits.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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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="Zdigits_Zpower"><span class="id" title="lemma">Zdigits_Zpower</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="Flocq.Core.Fcore_digits.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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> 1)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigits_le"><span class="id" title="lemma">Zdigits_le</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</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_digits.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_digits.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_digits.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><br/>
(<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="lt_Zdigits"><span class="id" title="lemma">lt_Zdigits</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</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_digits.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><br/>
(<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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><br/>
(<a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zpower_le_Zdigits"><span class="id" title="lemma">Zpower_le_Zdigits</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">e</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Core.Fcore_digits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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><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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="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_digits.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigits_le_Zpower"><span class="id" title="lemma">Zdigits_le_Zpower</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">e</span> <span class="id" title="var">x</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_digits.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="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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_digits.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_gt_Zdigits"><span class="id" title="lemma">Zpower_gt_Zdigits</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">e</span> <span class="id" title="var">x</span>,<br/>
(<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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_digits.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.BinInt.html#Zabs"><span class="id" title="abbreviation">Zabs</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.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="Zdigits_gt_Zpower"><span class="id" title="lemma">Zdigits_gt_Zpower</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">e</span> <span class="id" title="var">x</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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="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_digits.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><br/>
(<a class="idref" href="Flocq.Core.Fcore_digits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
</div>
<div class="doc">
Number of digits of a product.
<div class="paragraph"> </div>
This strong version is needed for proofs of division and square root
algorithms, since they involve operation remainders.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigits_mult_strong"><span class="id" title="lemma">Zdigits_mult_strong</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</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_digits.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> (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_digits.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><br/>
(<a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.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_digits.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#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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_digits.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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigits_mult"><span class="id" title="lemma">Zdigits_mult</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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.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_digits.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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigits_mult_ge"><span class="id" title="lemma">Zdigits_mult_ge</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_digits.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> 0)%<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_digits.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#32263a1c8b01baecdff9deb038955bc9"><span class="id" title="notation">≠</span></a> 0)%<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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.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#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> 1 <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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#y"><span class="id" title="variable">y</span></a>))%<span class="id" title="var">Z</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zdigits_div_Zpower"><span class="id" title="lemma">Zdigits_div_Zpower</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</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="Flocq.Core.Fcore_digits.html#m"><span class="id" title="variable">m</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#5dda7752d319ac2ccefb830f12787952"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#e"><span class="id" title="variable">e</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#5dda7752d319ac2ccefb830f12787952"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#m"><span class="id" title="variable">m</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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#66073ffd934badf1f6e703023820601f"><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> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Core.Fcore_digits.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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#e"><span class="id" title="variable">e</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_digits.html#Fcore_digits"><span class="id" title="section">Fcore_digits</span></a>.<br/>
<br/>
</div>
<div class="doc">
Specialized version for computing the number of bits of an integer
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Section</span> <a name="Zdigits2"><span class="id" title="section">Zdigits2</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Z_of_nat_S_digits2_Pnat"><span class="id" title="lemma">Z_of_nat_S_digits2_Pnat</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</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/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Z_of_nat"><span class="id" title="abbreviation">Z_of_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_digits.html#digits2_Pnat"><span class="id" title="definition">digits2_Pnat</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#m"><span class="id" title="variable">m</span></a>)) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix2"><span class="id" title="definition">radix2</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_digits.html#m"><span class="id" title="variable">m</span></a>).<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a name="digits2_pos"><span class="id" title="definition">digits2_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>) : <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="Flocq.Core.Fcore_digits.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#xH"><span class="id" title="constructor">xH</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#xH"><span class="id" title="constructor">xH</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">p</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.PArith.BinPos.html#Psucc"><span class="id" title="abbreviation">Psucc</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#digits2_pos"><span class="id" title="definition">digits2_pos</span></a> <span class="id" title="var">p</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">p</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.PArith.BinPos.html#Psucc"><span class="id" title="abbreviation">Psucc</span></a> (<a class="idref" href="Flocq.Core.Fcore_digits.html#digits2_pos"><span class="id" title="definition">digits2_pos</span></a> <span class="id" title="var">p</span>)<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Zpos_digits2_pos"><span class="id" title="lemma">Zpos_digits2_pos</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">m</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/>
<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_digits.html#digits2_pos"><span class="id" title="definition">digits2_pos</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#m"><span class="id" title="variable">m</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix2"><span class="id" title="definition">radix2</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_digits.html#m"><span class="id" title="variable">m</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a name="Zdigits2"><span class="id" title="definition">Zdigits2</span></a> <span class="id" title="var">n</span> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Flocq.Core.Fcore_digits.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#Z0"><span class="id" title="constructor">Z0</span></a> ⇒ <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a><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">p</span> ⇒ <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_digits.html#digits2_pos"><span class="id" title="definition">digits2_pos</span></a> <span class="id" title="var">p</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">p</span> ⇒ <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_digits.html#digits2_pos"><span class="id" title="definition">digits2_pos</span></a> <span class="id" title="var">p</span>)<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="Zdigits2_Zdigits"><span class="id" title="lemma">Zdigits2_Zdigits</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">n</span>, <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits2"><span class="id" title="definition">Zdigits2</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix2"><span class="id" title="definition">radix2</span></a> <a class="idref" href="Flocq.Core.Fcore_digits.html#n"><span class="id" title="variable">n</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits2"><span class="id" title="section">Zdigits2</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
>
90
