diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.ssreflect.binomial.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.ssreflect.binomial.html | 320 |
1 files changed, 0 insertions, 320 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.binomial.html b/docs/htmldoc/mathcomp.ssreflect.binomial.html deleted file mode 100644 index b6be0dc..0000000 --- a/docs/htmldoc/mathcomp.ssreflect.binomial.html +++ /dev/null @@ -1,320 +0,0 @@ -<!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">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><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 > 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#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">`!</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><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#fb85b56582e20c3ab47a4e55b1f6f111"><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#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">`!</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#b46f4e825b398c0eb860f658bff447f6"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#b46f4e825b398c0eb860f658bff447f6"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#b46f4e825b398c0eb860f658bff447f6"><span class="id" title="notation">(</span></a>1 <a class="idref" href="mathcomp.ssreflect.bigop.html#b46f4e825b398c0eb860f658bff447f6"><span class="id" title="notation">≤</span></a> <span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#b46f4e825b398c0eb860f658bff447f6"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#b46f4e825b398c0eb860f658bff447f6"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">`!</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><span class="id" title="notation">(</span></a>1 <a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><span class="id" title="notation">≤</span></a> <span class="id" title="var">k</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><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#2242f6721707980eca939ec29164eab3"><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#81fd94e251a61ee523cdd7855774ae7c"><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#7f2a7ef2c63af7359b22787a9daf336e"><span class="id" title="notation">></span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#fb85b56582e20c3ab47a4e55b1f6f111"><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#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">)`!</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">).+1</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><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#ea2ff3d561159081cea6fb2e8113cc54"><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#f953bf7095e0da1cb644443fd0e17d6d"><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/V8.9.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="a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">"</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/> - (<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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">_</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#ea2ff3d561159081cea6fb2e8113cc54"><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#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">_</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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#ea2ff3d561159081cea6fb2e8113cc54"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a>0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#cb53cf0ee22c036a03b4a9281c68b5a3"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#fb85b56582e20c3ab47a4e55b1f6f111"><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#cb53cf0ee22c036a03b4a9281c68b5a3"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#fb85b56582e20c3ab47a4e55b1f6f111"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">)`!</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#fb85b56582e20c3ab47a4e55b1f6f111"><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#cb53cf0ee22c036a03b4a9281c68b5a3"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">`!</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#2242f6721707980eca939ec29164eab3"><span class="id" title="notation">%/</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#fb85b56582e20c3ab47a4e55b1f6f111"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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#fb85b56582e20c3ab47a4e55b1f6f111"><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/> - <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/> - | <span class="id" title="var">n'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>, <span class="id" title="var">m'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><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#0dacc1786c5ba797d47dd85006231633"><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/> - | <span class="id" title="var">_</span>, 0 ⇒ 1<br/> - | 0, <span class="id" title="var">_</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> ⇒ 0<br/> - <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/V8.9.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="95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">"</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/> - (<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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">,</span></a> 0<a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">(</span></a>0<a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">,</span></a> 1<a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a>0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#cb53cf0ee22c036a03b4a9281c68b5a3"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#cb53cf0ee22c036a03b4a9281c68b5a3"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#cb53cf0ee22c036a03b4a9281c68b5a3"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><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#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">`!</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#fb85b56582e20c3ab47a4e55b1f6f111"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">)`!</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#fb85b56582e20c3ab47a4e55b1f6f111"><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#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">`!</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#2242f6721707980eca939ec29164eab3"><span class="id" title="notation">%/</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#2242f6721707980eca939ec29164eab3"><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#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">`!</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#fb85b56582e20c3ab47a4e55b1f6f111"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">)`!</span></a><a class="idref" href="mathcomp.ssreflect.div.html#2242f6721707980eca939ec29164eab3"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><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#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">`!</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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#2242f6721707980eca939ec29164eab3"><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#fb85b56582e20c3ab47a4e55b1f6f111"><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#cb53cf0ee22c036a03b4a9281c68b5a3"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">,</span></a> 2<a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#1ecb2ec20b22101a31d2177b576c9a81"><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#ea2ff3d561159081cea6fb2e8113cc54"><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#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1ecb2ec20b22101a31d2177b576c9a81"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">,</span></a> 2<a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#ea2ff3d561159081cea6fb2e8113cc54"><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#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1ecb2ec20b22101a31d2177b576c9a81"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> 0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cf4676be165a6295cd8b63fc45b45d8a"><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#cf4676be165a6295cd8b63fc45b45d8a"><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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#c0980ea1654f471922ad26f5837d48da"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><span class="id" title="notation">(</span></a>0 <a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><span class="id" title="notation">≤</span></a> <span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><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.bigop.html#c0980ea1654f471922ad26f5837d48da"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">,</span></a> 2<a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#c0980ea1654f471922ad26f5837d48da"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><span class="id" title="notation">(</span></a>0 <a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><span class="id" title="notation">≤</span></a> <span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#c0980ea1654f471922ad26f5837d48da"><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.bigop.html#c0980ea1654f471922ad26f5837d48da"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">,</span></a> 2<a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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/> - <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><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#0dacc1786c5ba797d47dd85006231633"><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#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><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#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><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#81fd94e251a61ee523cdd7855774ae7c"><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#ea2ff3d561159081cea6fb2e8113cc54"><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/> - <a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">(</span></a><span class="id" title="var">j</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#0dacc1786c5ba797d47dd85006231633"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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/> - <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#81fd94e251a61ee523cdd7855774ae7c"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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#81fd94e251a61ee523cdd7855774ae7c"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><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#7825ccc99f23b0d30c9d40c317ba7af0"><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#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><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.bigop.html#e383fcd76deb34dd09a423262c4c7429"><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#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><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#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7825ccc99f23b0d30c9d40c317ba7af0"><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#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><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#81fd94e251a61ee523cdd7855774ae7c"><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#ea2ff3d561159081cea6fb2e8113cc54"><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#f953bf7095e0da1cb644443fd0e17d6d"><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#81fd94e251a61ee523cdd7855774ae7c"><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#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">).-1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#e383fcd76deb34dd09a423262c4c7429"><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.bigop.html#e383fcd76deb34dd09a423262c4c7429"><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#81fd94e251a61ee523cdd7855774ae7c"><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#ea2ff3d561159081cea6fb2e8113cc54"><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#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><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#81fd94e251a61ee523cdd7855774ae7c"><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#f953bf7095e0da1cb644443fd0e17d6d"><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/V8.9.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/> - <a class="idref" href="mathcomp.ssreflect.bigop.html#f9660601caed2f1f92279ff134c53c8a"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#f9660601caed2f1f92279ff134c53c8a"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#f9660601caed2f1f92279ff134c53c8a"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#f9660601caed2f1f92279ff134c53c8a"><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.bigop.html#f9660601caed2f1f92279ff134c53c8a"><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#f9660601caed2f1f92279ff134c53c8a"><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#e3d79e08e7e529cc9ef532e000103386"><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#2b944e40a56cb605c3460196c2ed9ac4"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#f9660601caed2f1f92279ff134c53c8a"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#f9660601caed2f1f92279ff134c53c8a"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#f9660601caed2f1f92279ff134c53c8a"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#f9660601caed2f1f92279ff134c53c8a"><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.bigop.html#f9660601caed2f1f92279ff134c53c8a"><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#f9660601caed2f1f92279ff134c53c8a"><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#2b944e40a56cb605c3460196c2ed9ac4"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.div.html#2b944e40a56cb605c3460196c2ed9ac4"><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#2b944e40a56cb605c3460196c2ed9ac4"><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/V8.9.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/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><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#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><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#3e9d12914c7607378976c499a50a47c7"><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#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">&</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#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><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/V8.9.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/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#5aaa2ecf7f1dd075658db9a82cd529e3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#5aaa2ecf7f1dd075658db9a82cd529e3"><span class="id" title="notation">set</span></a> <span class="id" title="var">f</span> <a class="idref" href="mathcomp.ssreflect.finset.html#5aaa2ecf7f1dd075658db9a82cd529e3"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#5aaa2ecf7f1dd075658db9a82cd529e3"><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#5aaa2ecf7f1dd075658db9a82cd529e3"><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#5aaa2ecf7f1dd075658db9a82cd529e3"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><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/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">set</span></a> <span class="id" title="var">f</span> <a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><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#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#a4b4211b62fc5f6a3d047747e223cb60"><span class="id" title="notation">_</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) <span class="id" title="var">k</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">set</span></a> <span class="id" title="var">A</span> <a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><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#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><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#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">set</span></a> <span class="id" title="var">A</span> <a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><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#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><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#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><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#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><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#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><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#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#0dacc1786c5ba797d47dd85006231633"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><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#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#3c5ded5149162c47f03c637c983c78c4"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#3c5ded5149162c47f03c637c983c78c4"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#3c5ded5149162c47f03c637c983c78c4"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#3c5ded5149162c47f03c637c983c78c4"><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.bigop.html#3c5ded5149162c47f03c637c983c78c4"><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#cb53cf0ee22c036a03b4a9281c68b5a3"><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#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#0dacc1786c5ba797d47dd85006231633"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#3c5ded5149162c47f03c637c983c78c4"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#3c5ded5149162c47f03c637c983c78c4"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#3c5ded5149162c47f03c637c983c78c4"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#3c5ded5149162c47f03c637c983c78c4"><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.bigop.html#3c5ded5149162c47f03c637c983c78c4"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><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#6ac1c202d9451e0a66d4fc93e5d9b44b"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#95129fba25b300adee91ca933fa2fcdc"><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#0dacc1786c5ba797d47dd85006231633"><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#95129fba25b300adee91ca933fa2fcdc"><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#95129fba25b300adee91ca933fa2fcdc"><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/> -</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 |