-
Notifications
You must be signed in to change notification settings - Fork 11
Expand file tree
/
Copy pathCombi.Combi.multinomial.html
More file actions
118 lines (82 loc) · 29.2 KB
/
Copy pathCombi.Combi.multinomial.html
File metadata and controls
118 lines (82 loc) · 29.2 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
<!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=iso-8859-1" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<title>Combi.Combi.multinomial: Multinomial Coefficients</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library Combi.Combi.multinomial: Multinomial Coefficients</h1>
<div class="code">
</div>
<div class="doc">
</div>
<div class="code">
</div>
<div class="doc">
<a id="lab57"></a><h1 class="section">Multinomial Coefficients</h1>
<div class="paragraph"> </div>
We define:
<ul class="doclist">
<li> 'C<span class="inlinecode"><span class="id" title="var">s</span></span> == the multinomial coefficient associated to the sequence <span class="inlinecode"><span class="id" title="var">s</span></span>.
</li>
</ul>
<div class="paragraph"> </div>
The main expression is Lemma <span class="inlinecode"><span class="id" title="var">multinomial_factd</span></span>:
<div class="paragraph"> </div>
<span class="inlinecode"></span> <span class="inlinecode">'<span class="id" title="var">C</span>[<span class="id" title="var">s</span>]</span> <span class="inlinecode">=</span> <span class="inlinecode">(<span class="id" title="var">sumn</span></span> <span class="inlinecode"><span class="id" title="var">s</span>)`!</span> <span class="inlinecode">%/</span> <span class="inlinecode">\<span class="id" title="var">prod_</span>(<span class="id" title="var">i</span></span> <span class="inlinecode"><-</span> <span class="inlinecode"><span class="id" title="var">s</span>)</span> <span class="inlinecode"><span class="id" title="var">i</span>`!.</span> <span class="inlinecode"></span>
<div class="paragraph"> </div>
</div>
<div class="code">
<span class="id" title="keyword">From</span> <span class="id" title="var">Corelib</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Setoids.Setoid.html#"><span class="id" title="library">Setoid</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">mathcomp</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">ssreflect</span> <span class="id" title="library">ssrbool</span> <span class="id" title="library">ssrfun</span> <span class="id" title="library">ssrnat</span> <span class="id" title="library">eqtype</span> <span class="id" title="library">fintype</span> <span class="id" title="library">choice</span> <span class="id" title="library">seq</span>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">mathcomp</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">bigop</span> <span class="id" title="library">div</span> <span class="id" title="library">binomial</span>.<br/>
<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Combi.SSRcomplements.tools.html#"><span class="id" title="library">tools</span></a>.<br/>
<br/>
<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
<br/>
<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> (<span class="id" title="var">i</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<span class="id" title="var">s</span> <span class="id" title="var">t</span> : <span class="id" title="abbreviation">seq</span> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/>
<br/>
<span class="id" title="keyword">Fixpoint</span> <a id="multinomial_rec" class="idref" href="#multinomial_rec"><span class="id" title="definition">multinomial_rec</span></a> <a id="s:1" class="idref" href="#s:1"><span class="id" title="binder">s</span></a> :=<br/>
<span class="id" title="keyword">if</span> <a class="idref" href="Combi.Combi.multinomial.html#s:1"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">i</span> <span class="id" title="notation">::</span> <span class="id" title="var">s'</span> <span class="id" title="keyword">then</span> <span class="id" title="notation">'</span><span class="id" title="notation">C</span><span class="id" title="notation">(</span><span class="id" title="definition">sumn</span> <a class="idref" href="Combi.Combi.multinomial.html#s:1"><span class="id" title="variable">s</span></a><span class="id" title="notation">,</span> <span class="id" title="var">i</span><span class="id" title="notation">)</span> <span class="id" title="notation">*</span> <span class="id" title="notation">(</span><a class="idref" href="Combi.Combi.multinomial.html#multinomial_rec:2"><span class="id" title="definition">multinomial_rec</span></a> <span class="id" title="var">s'</span><span class="id" title="notation">)</span> <span class="id" title="keyword">else</span> 1.<br/>
<span class="id" title="keyword">Arguments</span> <a class="idref" href="Combi.Combi.multinomial.html#multinomial_rec"><span class="id" title="definition">multinomial_rec</span></a> : <span class="id" title="tactic">simpl</span> <span class="id" title="var">nomatch</span>.<br/>
<span class="id" title="keyword">Definition</span> <a id="multinomial" class="idref" href="#multinomial"><span class="id" title="definition">multinomial</span></a> := <a class="idref" href="Combi.Combi.multinomial.html#multinomial_rec"><span class="id" title="definition">multinomial_rec</span></a>.<br/>
<span class="id" title="keyword">Arguments</span> <a class="idref" href="Combi.Combi.multinomial.html#multinomial"><span class="id" title="definition">multinomial</span></a> : <span class="id" title="tactic">simpl</span> <span class="id" title="var">never</span>.<br/>
<span class="id" title="keyword">Notation</span> <a id="1fe8f419670f016387192cea55d3d07e" class="idref" href="#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">"</span></a>''C' [ s ]" := (<a class="idref" href="Combi.Combi.multinomial.html#multinomial"><span class="id" title="definition">multinomial</span></a> <span class="id" title="var">s</span>)<br/>
(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "''C' [ s ]") : <span class="id" title="var">nat_scope</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="multinomial0" class="idref" href="#multinomial0"><span class="id" title="lemma">multinomial0</span></a> : <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><span class="id" title="notation">[::]</span><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1.<br/>
<span class="id" title="keyword">Lemma</span> <a id="multinomial1" class="idref" href="#multinomial1"><span class="id" title="lemma">multinomial1</span></a> <a id="i:4" class="idref" href="#i:4"><span class="id" title="binder">i</span></a> : <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><span class="id" title="notation">[::</span> <a class="idref" href="Combi.Combi.multinomial.html#i:4"><span class="id" title="variable">i</span></a><span class="id" title="notation">]</span><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1.<br/>
<span class="id" title="keyword">Lemma</span> <a id="multinomialE" class="idref" href="#multinomialE"><span class="id" title="lemma">multinomialE</span></a> <a id="i:5" class="idref" href="#i:5"><span class="id" title="binder">i</span></a> <a id="s:6" class="idref" href="#s:6"><span class="id" title="binder">s</span></a> : <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><a class="idref" href="Combi.Combi.multinomial.html#i:5"><span class="id" title="variable">i</span></a> <span class="id" title="notation">::</span> <a class="idref" href="Combi.Combi.multinomial.html#s:6"><span class="id" title="variable">s</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="notation">'</span><span class="id" title="notation">C</span><span class="id" title="notation">(</span><a class="idref" href="Combi.Combi.multinomial.html#i:5"><span class="id" title="variable">i</span></a> <span class="id" title="notation">+</span> <span class="id" title="definition">sumn</span> <a class="idref" href="Combi.Combi.multinomial.html#s:6"><span class="id" title="variable">s</span></a><span class="id" title="notation">,</span> <a class="idref" href="Combi.Combi.multinomial.html#i:5"><span class="id" title="variable">i</span></a><span class="id" title="notation">)</span> <span class="id" title="notation">*</span> <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><a class="idref" href="Combi.Combi.multinomial.html#s:6"><span class="id" title="variable">s</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Lemma</span> <a id="multinomial2" class="idref" href="#multinomial2"><span class="id" title="lemma">multinomial2</span></a> <a id="a:7" class="idref" href="#a:7"><span class="id" title="binder">a</span></a> <a id="b:8" class="idref" href="#b:8"><span class="id" title="binder">b</span></a> : <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><span class="id" title="notation">[::</span> <a class="idref" href="Combi.Combi.multinomial.html#a:7"><span class="id" title="variable">a</span></a><span class="id" title="notation">;</span> <a class="idref" href="Combi.Combi.multinomial.html#b:8"><span class="id" title="variable">b</span></a><span class="id" title="notation">]</span><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="notation">'</span><span class="id" title="notation">C</span><span class="id" title="notation">(</span><a class="idref" href="Combi.Combi.multinomial.html#a:7"><span class="id" title="variable">a</span></a> <span class="id" title="notation">+</span> <a class="idref" href="Combi.Combi.multinomial.html#b:8"><span class="id" title="variable">b</span></a><span class="id" title="notation">,</span> <a class="idref" href="Combi.Combi.multinomial.html#a:7"><span class="id" title="variable">a</span></a><span class="id" title="notation">)</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="multinomial_fact" class="idref" href="#multinomial_fact"><span class="id" title="lemma">multinomial_fact</span></a> <a id="s:9" class="idref" href="#s:9"><span class="id" title="binder">s</span></a> : <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><a class="idref" href="Combi.Combi.multinomial.html#s:9"><span class="id" title="variable">s</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a> <span class="id" title="notation">*</span> <span class="id" title="notation">\</span><span class="id" title="notation">prod_</span><span class="id" title="notation">(</span><a id="i:10" class="idref" href="#i:10"><span class="id" title="binder"><span id="i:11" class="id"><span id="i:12" class="id">i</span></span></span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Combi.Combi.multinomial.html#s:9"><span class="id" title="variable">s</span></a><span class="id" title="notation">)</span> <a class="idref" href="Combi.Combi.multinomial.html#i:10"><span class="id" title="variable">i</span></a><span class="id" title="notation">`!</span> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="notation">(</span><span class="id" title="definition">sumn</span> <a class="idref" href="Combi.Combi.multinomial.html#s:9"><span class="id" title="variable">s</span></a><span class="id" title="notation">)`!</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="multinomial_nseq" class="idref" href="#multinomial_nseq"><span class="id" title="lemma">multinomial_nseq</span></a> <a id="n:13" class="idref" href="#n:13"><span class="id" title="binder">n</span></a> <a id="a:14" class="idref" href="#a:14"><span class="id" title="binder">a</span></a> : <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><span class="id" title="definition">nseq</span> <a class="idref" href="Combi.Combi.multinomial.html#n:13"><span class="id" title="variable">n</span></a> <a class="idref" href="Combi.Combi.multinomial.html#a:14"><span class="id" title="variable">a</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a> <span class="id" title="notation">*</span> <span class="id" title="notation">(</span><a class="idref" href="Combi.Combi.multinomial.html#a:14"><span class="id" title="variable">a</span></a><span class="id" title="notation">`!</span> <span class="id" title="notation">^</span> <a class="idref" href="Combi.Combi.multinomial.html#n:13"><span class="id" title="variable">n</span></a><span class="id" title="notation">)</span> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="notation">(</span><a class="idref" href="Combi.Combi.multinomial.html#a:14"><span class="id" title="variable">a</span></a> <span class="id" title="notation">*</span> <a class="idref" href="Combi.Combi.multinomial.html#n:13"><span class="id" title="variable">n</span></a><span class="id" title="notation">)`!</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="multinomial_nseq1" class="idref" href="#multinomial_nseq1"><span class="id" title="lemma">multinomial_nseq1</span></a> <a id="n:15" class="idref" href="#n:15"><span class="id" title="binder">n</span></a> : <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><span class="id" title="definition">nseq</span> <a class="idref" href="Combi.Combi.multinomial.html#n:15"><span class="id" title="variable">n</span></a> 1<a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Combi.Combi.multinomial.html#n:15"><span class="id" title="variable">n</span></a><span class="id" title="notation">`!</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="dvdn_prodfact" class="idref" href="#dvdn_prodfact"><span class="id" title="lemma">dvdn_prodfact</span></a> <a id="s:16" class="idref" href="#s:16"><span class="id" title="binder">s</span></a> : <span class="id" title="notation">\</span><span class="id" title="notation">prod_</span><span class="id" title="notation">(</span><a id="i:17" class="idref" href="#i:17"><span class="id" title="binder"><span id="i:18" class="id"><span id="i:19" class="id">i</span></span></span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Combi.Combi.multinomial.html#s:16"><span class="id" title="variable">s</span></a><span class="id" title="notation">)</span> <a class="idref" href="Combi.Combi.multinomial.html#i:17"><span class="id" title="variable">i</span></a><span class="id" title="notation">`!</span> <span class="id" title="notation">%|</span> <span class="id" title="notation">(</span><span class="id" title="definition">sumn</span> <a class="idref" href="Combi.Combi.multinomial.html#s:16"><span class="id" title="variable">s</span></a><span class="id" title="notation">)`!</span> .<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="multinomial_factd" class="idref" href="#multinomial_factd"><span class="id" title="lemma">multinomial_factd</span></a> <a id="s:20" class="idref" href="#s:20"><span class="id" title="binder">s</span></a> : <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><a class="idref" href="Combi.Combi.multinomial.html#s:20"><span class="id" title="variable">s</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="notation">(</span><span class="id" title="definition">sumn</span> <a class="idref" href="Combi.Combi.multinomial.html#s:20"><span class="id" title="variable">s</span></a><span class="id" title="notation">)`!</span> <span class="id" title="notation">%/</span> <span class="id" title="notation">\</span><span class="id" title="notation">prod_</span><span class="id" title="notation">(</span><a id="i:21" class="idref" href="#i:21"><span class="id" title="binder"><span id="i:22" class="id"><span id="i:23" class="id">i</span></span></span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Combi.Combi.multinomial.html#s:20"><span class="id" title="variable">s</span></a><span class="id" title="notation">)</span> <a class="idref" href="Combi.Combi.multinomial.html#i:21"><span class="id" title="variable">i</span></a><span class="id" title="notation">`!</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="multinomial_cat" class="idref" href="#multinomial_cat"><span class="id" title="lemma">multinomial_cat</span></a> <a id="s:24" class="idref" href="#s:24"><span class="id" title="binder">s</span></a> <a id="t:25" class="idref" href="#t:25"><span class="id" title="binder">t</span></a> :<br/>
<a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><a class="idref" href="Combi.Combi.multinomial.html#s:24"><span class="id" title="variable">s</span></a> <span class="id" title="notation">++</span> <a class="idref" href="Combi.Combi.multinomial.html#t:25"><span class="id" title="variable">t</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="notation">'</span><span class="id" title="notation">C</span><span class="id" title="notation">(</span><span class="id" title="definition">sumn</span> <a class="idref" href="Combi.Combi.multinomial.html#s:24"><span class="id" title="variable">s</span></a> <span class="id" title="notation">+</span> <span class="id" title="definition">sumn</span> <a class="idref" href="Combi.Combi.multinomial.html#t:25"><span class="id" title="variable">t</span></a><span class="id" title="notation">,</span> <span class="id" title="definition">sumn</span> <a class="idref" href="Combi.Combi.multinomial.html#s:24"><span class="id" title="variable">s</span></a><span class="id" title="notation">)</span> <span class="id" title="notation">*</span> <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><a class="idref" href="Combi.Combi.multinomial.html#s:24"><span class="id" title="variable">s</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a> <span class="id" title="notation">*</span> <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><a class="idref" href="Combi.Combi.multinomial.html#t:25"><span class="id" title="variable">t</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="perm_multinomial" class="idref" href="#perm_multinomial"><span class="id" title="lemma">perm_multinomial</span></a> <a id="s:26" class="idref" href="#s:26"><span class="id" title="binder">s</span></a> <a id="t:27" class="idref" href="#t:27"><span class="id" title="binder">t</span></a> : <span class="id" title="definition">perm_eq</span> <a class="idref" href="Combi.Combi.multinomial.html#s:26"><span class="id" title="variable">s</span></a> <a class="idref" href="Combi.Combi.multinomial.html#t:27"><span class="id" title="variable">t</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><a class="idref" href="Combi.Combi.multinomial.html#s:26"><span class="id" title="variable">s</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><a class="idref" href="Combi.Combi.multinomial.html#t:27"><span class="id" title="variable">t</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="multinomial_filter_neq0" class="idref" href="#multinomial_filter_neq0"><span class="id" title="lemma">multinomial_filter_neq0</span></a> <a id="s:28" class="idref" href="#s:28"><span class="id" title="binder">s</span></a> : <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><span class="id" title="notation">[</span><span class="id" title="notation">seq</span> <a id="i:29" class="idref" href="#i:29"><span class="id" title="binder">i</span></a> <span class="id" title="notation"><-</span> <a class="idref" href="Combi.Combi.multinomial.html#s:28"><span class="id" title="variable">s</span></a> <span class="id" title="notation">|</span> <a class="idref" href="Combi.Combi.multinomial.html#i:29"><span class="id" title="variable">i</span></a> <span class="id" title="notation">!=</span> 0<span class="id" title="notation">]</span><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">'</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">C</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">[</span></a><a class="idref" href="Combi.Combi.multinomial.html#s:28"><span class="id" title="variable">s</span></a><a class="idref" href="Combi.Combi.multinomial.html#1fe8f419670f016387192cea55d3d07e"><span class="id" title="notation">]</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://rocq-prover.org/">coqdoc</a>
</div>
</div>
</body>
</html>