generate the documentation for 1.7

author: Enrico Tassi 2018-04-20 10:54:22 +0200
committer: Enrico Tassi 2018-04-20 10:54:22 +0200
commit: ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree: e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.ssreflect.binomial.html
parent: 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)
1 files changed, 323 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.binomial.html b/docs/htmldoc/mathcomp.ssreflect.binomial.html
new file mode 100644
index 0000000..085a24d
--- /dev/null
+++ b/docs/htmldoc/mathcomp.ssreflect.binomial.html
@@ -0,0 +1,323 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<title>mathcomp.ssreflect.binomial</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library mathcomp.ssreflect.binomial</h1>
+
+<div class="code">
+<span class="comment">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
+&nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ This files contains the definition of:                                     
+   'C(n, m) == the binomial coeficient n choose m.                          
+     n ^_ m == the falling (or lower) factorial of n with m terms, i.e.,    
+               the product n * (n - 1) * ... * (n - m + 1).                 
+               Note that n ^_ m = 0 if m &gt; n, and 'C(n, m) = n ^_ m %/ m/!. 
+
+<div class="paragraph"> </div>
+
+ In additions to the properties of these functions, we prove a few seminal  
+ results such as triangular_sum, Wilson and Pascal; their proofs are good   
+ examples of how to manipulate expressions with bigops.                      
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ More properties of the factorial * 
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="fact_smonotone"><span class="id" title="lemma">fact_smonotone</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> : 0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="fact_prod"><span class="id" title="lemma">fact_prod</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#a394fade46b35354f996bd50f29a270c"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#a394fade46b35354f996bd50f29a270c"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#a394fade46b35354f996bd50f29a270c"><span class="id" title="notation">(</span></a>1 <a class="idref" href="mathcomp.ssreflect.bigop.html#a394fade46b35354f996bd50f29a270c"><span class="id" title="notation">≤</span></a> <span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#a394fade46b35354f996bd50f29a270c"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#a394fade46b35354f996bd50f29a270c"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="logn_fact"><span class="id" title="lemma">logn_fact</span></a> <span class="id" title="var">p</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.prime.html#logn"><span class="id" title="definition">logn</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">(</span></a>1 <a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">≤</span></a> <span class="id" title="var">k</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#df17451da28eb630dbb51b12706ba39e"><span class="id" title="notation">%/</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Theorem</span> <a name="Wilson"><span class="id" title="lemma">Wilson</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#19ab5cfd7e4f60fa14f22b576013bd96"><span class="id" title="notation">&gt;</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">)`!</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">).+1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ The falling factorial  
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Fixpoint</span> <a name="ffact_rec"><span class="id" title="definition">ffact_rec</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> := <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">m'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ffact_rec"><span class="id" title="definition">ffact_rec</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a> <span class="id" title="var">m'</span> <span class="id" title="keyword">else</span> 1.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="falling_factorial"><span class="id" title="definition">falling_factorial</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#nosimpl"><span class="id" title="abbreviation">nosimpl</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ffact_rec"><span class="id" title="definition">ffact_rec</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">&quot;</span></a>n ^_ m" := (<a class="idref" href="mathcomp.ssreflect.binomial.html#falling_factorial"><span class="id" title="definition">falling_factorial</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>)<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 30, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>) : <span class="id" title="var">nat_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffactE"><span class="id" title="lemma">ffactE</span></a> : <a class="idref" href="mathcomp.ssreflect.binomial.html#falling_factorial"><span class="id" title="definition">falling_factorial</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ffact_rec"><span class="id" title="definition">ffact_rec</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffactn0"><span class="id" title="lemma">ffactn0</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffact0n"><span class="id" title="lemma">ffact0n</span></a> <span class="id" title="var">m</span> : 0 <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffactnS"><span class="id" title="lemma">ffactnS</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffactSS"><span class="id" title="lemma">ffactSS</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffactn1"><span class="id" title="lemma">ffactn1</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffactnSr"><span class="id" title="lemma">ffactnSr</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffact_gt0"><span class="id" title="lemma">ffact_gt0</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a>0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffact_small"><span class="id" title="lemma">ffact_small</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffactnn"><span class="id" title="lemma">ffactnn</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffact_fact"><span class="id" title="lemma">ffact_fact</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">)`!</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffact_factd"><span class="id" title="lemma">ffact_factd</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#df17451da28eb630dbb51b12706ba39e"><span class="id" title="notation">%/</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">)`!</span></a>.<br/>
+ 
+<br/>
+</div>
+
+<div class="doc">
+ Binomial coefficients  
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Fixpoint</span> <a name="binomial_rec"><span class="id" title="definition">binomial_rec</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a>, <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;| <span class="id" title="var">n'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>, <span class="id" title="var">m'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> ⇒ <a class="idref" href="mathcomp.ssreflect.binomial.html#binomial_rec"><span class="id" title="definition">binomial_rec</span></a> <span class="id" title="var">n'</span> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#binomial_rec"><span class="id" title="definition">binomial_rec</span></a> <span class="id" title="var">n'</span> <span class="id" title="var">m'</span><br/>
+&nbsp;&nbsp;| <span class="id" title="var">_</span>, 0 ⇒ 1<br/>
+&nbsp;&nbsp;| 0, <span class="id" title="var">_</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> ⇒ 0<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="binomial"><span class="id" title="definition">binomial</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#nosimpl"><span class="id" title="abbreviation">nosimpl</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#binomial_rec"><span class="id" title="definition">binomial_rec</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">&quot;</span></a>''C' ( n , m )" := (<a class="idref" href="mathcomp.ssreflect.binomial.html#binomial"><span class="id" title="definition">binomial</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>)<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">format</span> "''C' ( n ,  m )") : <span class="id" title="var">nat_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="binE"><span class="id" title="lemma">binE</span></a> : <a class="idref" href="mathcomp.ssreflect.binomial.html#binomial"><span class="id" title="definition">binomial</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#binomial_rec"><span class="id" title="definition">binomial_rec</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="bin0"><span class="id" title="lemma">bin0</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> 0<a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="bin0n"><span class="id" title="lemma">bin0n</span></a> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a>0<a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="binS"><span class="id" title="lemma">binS</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="bin1"><span class="id" title="lemma">bin1</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> 1<a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="bin_gt0"><span class="id" title="lemma">bin_gt0</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a>0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="leq_bin2l"><span class="id" title="lemma">leq_bin2l</span></a> <span class="id" title="var">n1</span> <span class="id" title="var">n2</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#n1"><span class="id" title="variable">n1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n2"><span class="id" title="variable">n2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n1"><span class="id" title="variable">n1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n2"><span class="id" title="variable">n2</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="bin_small"><span class="id" title="lemma">bin_small</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="binn"><span class="id" title="lemma">binn</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.<br/>
+ 
+<br/>
+</div>
+
+<div class="doc">
+ Multiply to move diagonally down and right in the Pascal triangle.  
+</div>
+<div class="code">
+<span class="id" title="keyword">Lemma</span> <a name="mul_bin_diag"><span class="id" title="lemma">mul_bin_diag</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="bin_fact"><span class="id" title="lemma">bin_fact</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">)`!</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ In fact the only exception for bin_factd is n = 0 and m = 1  
+</div>
+<div class="code">
+<span class="id" title="keyword">Lemma</span> <a name="bin_factd"><span class="id" title="lemma">bin_factd</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : 0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#df17451da28eb630dbb51b12706ba39e"><span class="id" title="notation">%/</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#df17451da28eb630dbb51b12706ba39e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">)`!</span></a><a class="idref" href="mathcomp.ssreflect.div.html#df17451da28eb630dbb51b12706ba39e"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="bin_ffact"><span class="id" title="lemma">bin_ffact</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="bin_ffactd"><span class="id" title="lemma">bin_ffactd</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#df17451da28eb630dbb51b12706ba39e"><span class="id" title="notation">%/</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="bin_sub"><span class="id" title="lemma">bin_sub</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Multiply to move down in the Pascal triangle.  
+</div>
+<div class="code">
+<span class="id" title="keyword">Lemma</span> <a name="mul_bin_down"><span class="id" title="lemma">mul_bin_down</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Multiply to move left in the Pascal triangle.  
+</div>
+<div class="code">
+<span class="id" title="keyword">Lemma</span> <a name="mul_bin_left"><span class="id" title="lemma">mul_bin_left</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="binSn"><span class="id" title="lemma">binSn</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="bin2"><span class="id" title="lemma">bin2</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> 2<a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#87e393a316922a3ff9e9f709674e598e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#87e393a316922a3ff9e9f709674e598e"><span class="id" title="notation">)./2</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="bin2odd"><span class="id" title="lemma">bin2odd</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> 2<a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#87e393a316922a3ff9e9f709674e598e"><span class="id" title="notation">./2</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="prime_dvd_bin"><span class="id" title="lemma">prime_dvd_bin</span></a> <span class="id" title="var">k</span> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> 0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#432e31800fc09abd260feb634dbbd1af"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#432e31800fc09abd260feb634dbbd1af"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="triangular_sum"><span class="id" title="lemma">triangular_sum</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">(</span></a>0 <a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">≤</span></a> <span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> 2<a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="textbook_triangular_sum"><span class="id" title="lemma">textbook_triangular_sum</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">(</span></a>0 <a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">≤</span></a> <span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#01dc18dd2300d727116181d8b66f2939"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> 2<a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Theorem</span> <a name="Pascal"><span class="id" title="lemma">Pascal</span></a> <span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">n</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="expnDn"><span class="id" title="definition">expnDn</span></a> := <a class="idref" href="mathcomp.ssreflect.binomial.html#Pascal"><span class="id" title="lemma">Pascal</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="Vandermonde"><span class="id" title="lemma">Vandermonde</span></a> <span class="id" title="var">k</span> <span class="id" title="var">l</span> <span class="id" title="var">i</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">(</span></a><span class="id" title="var">j</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#j"><span class="id" title="variable">j</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#l"><span class="id" title="variable">l</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#j"><span class="id" title="variable">j</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#l"><span class="id" title="variable">l</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="subn_exp"><span class="id" title="lemma">subn_exp</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> <span class="id" title="var">k</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9482aae3d3b06e249765c1225dbb8cbb"><span class="id" title="notation">-</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="predn_exp"><span class="id" title="lemma">predn_exp</span></a> <span class="id" title="var">m</span> <span class="id" title="var">k</span> : <a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">).-1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">&lt;</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#61f81dc9ba2725ea9fb474df7def3848"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="dvdn_pred_predX"><span class="id" title="lemma">dvdn_pred_predX</span></a> <span class="id" title="var">n</span> <span class="id" title="var">e</span> : (<a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">).-1</span></a>)%<span class="id" title="var">N</span>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="modn_summ"><span class="id" title="lemma">modn_summ</span></a> <span class="id" title="var">I</span> <span class="id" title="var">r</span> (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#I"><span class="id" title="variable">I</span></a>) <span class="id" title="var">F</span> <span class="id" title="var">d</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.bigop.html#ea7e35bae15685d5cd3430a8e48be02b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#ea7e35bae15685d5cd3430a8e48be02b"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#ea7e35bae15685d5cd3430a8e48be02b"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#ea7e35bae15685d5cd3430a8e48be02b"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#ea7e35bae15685d5cd3430a8e48be02b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#ea7e35bae15685d5cd3430a8e48be02b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#2179ac53e82aa7c0b2f2f5a16b5510ea"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#20229f50700a74daa1cbc50e0281abb6"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#ea7e35bae15685d5cd3430a8e48be02b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#ea7e35bae15685d5cd3430a8e48be02b"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#ea7e35bae15685d5cd3430a8e48be02b"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#ea7e35bae15685d5cd3430a8e48be02b"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#ea7e35bae15685d5cd3430a8e48be02b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#ea7e35bae15685d5cd3430a8e48be02b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#20229f50700a74daa1cbc50e0281abb6"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.div.html#20229f50700a74daa1cbc50e0281abb6"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#d"><span class="id" title="variable">d</span></a><a class="idref" href="mathcomp.ssreflect.div.html#20229f50700a74daa1cbc50e0281abb6"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Combinatorial characterizations.  
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="Combinations"><span class="id" title="section">Combinations</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">T</span> <span class="id" title="var">D</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_uniq_tuples"><span class="id" title="lemma">card_uniq_tuples</span></a> <span class="id" title="var">T</span> <span class="id" title="var">n</span> (<span class="id" title="var">A</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#T"><span class="id" title="variable">T</span></a>) :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_inj_ffuns_on"><span class="id" title="lemma">card_inj_ffuns_on</span></a> <span class="id" title="var">D</span> <span class="id" title="var">T</span> (<span class="id" title="var">R</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#T"><span class="id" title="variable">T</span></a>) :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#e6ed8c730df9d279cb8b0aa48c1051d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#e6ed8c730df9d279cb8b0aa48c1051d8"><span class="id" title="notation">set</span></a> <span class="id" title="var">f</span> <a class="idref" href="mathcomp.ssreflect.finset.html#e6ed8c730df9d279cb8b0aa48c1051d8"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#e6ed8c730df9d279cb8b0aa48c1051d8"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#ffun_on"><span class="id" title="abbreviation">ffun_on</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#e6ed8c730df9d279cb8b0aa48c1051d8"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#injectiveb"><span class="id" title="definition">injectiveb</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f"><span class="id" title="variable">f</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#e6ed8c730df9d279cb8b0aa48c1051d8"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#D"><span class="id" title="variable">D</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_inj_ffuns"><span class="id" title="lemma">card_inj_ffuns</span></a> <span class="id" title="var">D</span> <span class="id" title="var">T</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">set</span></a> <span class="id" title="var">f</span> <a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#injectiveb"><span class="id" title="definition">injectiveb</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f"><span class="id" title="variable">f</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#ee4a5b37d4e0ed25312d896332934f0f"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#D"><span class="id" title="variable">D</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="cards_draws"><span class="id" title="lemma">cards_draws</span></a> <span class="id" title="var">T</span> (<span class="id" title="var">B</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) <span class="id" title="var">k</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">set</span></a> <span class="id" title="var">A</span> <a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_draws"><span class="id" title="lemma">card_draws</span></a> <span class="id" title="var">T</span> <span class="id" title="var">k</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">set</span></a> <span class="id" title="var">A</span> <a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_ltn_sorted_tuples"><span class="id" title="lemma">card_ltn_sorted_tuples</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ltn"><span class="id" title="definition">ltn</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#t"><span class="id" title="variable">t</span></a>)<a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_sorted_tuples"><span class="id" title="lemma">card_sorted_tuples</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#sorted"><span class="id" title="definition">sorted</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#leq"><span class="id" title="definition">leq</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#t"><span class="id" title="variable">t</span></a>)<a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_partial_ord_partitions"><span class="id" title="lemma">card_partial_ord_partitions</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#b37dc668e343eb17a55a9974b7f85ec0"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#b37dc668e343eb17a55a9974b7f85ec0"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#b37dc668e343eb17a55a9974b7f85ec0"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#b37dc668e343eb17a55a9974b7f85ec0"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#b37dc668e343eb17a55a9974b7f85ec0"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_ord_partitions"><span class="id" title="lemma">card_ord_partitions</span></a> <span class="id" title="var">m</span> <span class="id" title="var">n</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#b37dc668e343eb17a55a9974b7f85ec0"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#b37dc668e343eb17a55a9974b7f85ec0"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#b37dc668e343eb17a55a9974b7f85ec0"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#b37dc668e343eb17a55a9974b7f85ec0"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#b37dc668e343eb17a55a9974b7f85ec0"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d086f256e0c3de938a1d3ad3965b5d4b"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.binomial.html#Combinations"><span class="id" title="section">Combinations</span></a>.<br/>
+
+<br/>
+</div>
+</div>
+
+<div id="footer">
+<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
+</div>
+
+</div>
+
+</body>
+</html>
+\ No newline at end of file
author	Enrico Tassi	2018-04-20 10:54:22 +0200
committer	Enrico Tassi	2018-04-20 10:54:22 +0200
commit	ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree	e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.ssreflect.binomial.html
parent	3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)