| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (68863 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (985 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (44709 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (761 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1497 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (570 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11380 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (976 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (603 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (298 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (460 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (476 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (811 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1157 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4018 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (162 entries) |
P (binder)
PandQ:3 [in Coq.ssr.ssrfun]partition:229 [in Coq.FSets.FSetInterface]
partition:74 [in Coq.FSets.FSetBridge]
pat:107 [in Coq.micromega.Tauto]
pat:218 [in Coq.micromega.Tauto]
pat:222 [in Coq.micromega.Tauto]
pat:35 [in Coq.Init.Specif]
pat:36 [in Coq.Init.Specif]
pat:37 [in Coq.Init.Specif]
pat:38 [in Coq.Init.Specif]
pat:39 [in Coq.Init.Specif]
pat:40 [in Coq.Init.Specif]
pat:41 [in Coq.Init.Specif]
pat:42 [in Coq.Init.Specif]
pat:43 [in Coq.Init.Specif]
pat:44 [in Coq.Init.Specif]
pat:45 [in Coq.Init.Specif]
pat:46 [in Coq.Init.Specif]
pc:14 [in Coq.btauto.Reflect]
Pdec:210 [in Coq.FSets.FSetInterface]
Pdec:217 [in Coq.FSets.FSetInterface]
Pdec:222 [in Coq.FSets.FSetInterface]
Pdec:227 [in Coq.FSets.FSetInterface]
Pdec:51 [in Coq.FSets.FSetBridge]
Pdec:55 [in Coq.FSets.FSetBridge]
Pdec:58 [in Coq.FSets.FSetBridge]
Pdec:64 [in Coq.FSets.FSetBridge]
Pdec:68 [in Coq.FSets.FSetBridge]
Pdec:72 [in Coq.FSets.FSetBridge]
pen:108 [in Coq.Reals.Runcountable]
pen:113 [in Coq.Reals.Runcountable]
pen:39 [in Coq.Reals.Runcountable]
pen:47 [in Coq.Reals.Runcountable]
pen:61 [in Coq.Reals.Runcountable]
pen:77 [in Coq.Reals.Runcountable]
pen:93 [in Coq.Reals.Runcountable]
Peq:116 [in Coq.Init.Datatypes]
Peq:121 [in Coq.Init.Datatypes]
Peq:126 [in Coq.Init.Datatypes]
pe1:208 [in Coq.setoid_ring.Ncring_polynom]
pe1:358 [in Coq.setoid_ring.Ring_polynom]
pe1:372 [in Coq.micromega.EnvRing]
pe1:390 [in Coq.setoid_ring.Ring_polynom]
pe2:209 [in Coq.setoid_ring.Ncring_polynom]
pe2:359 [in Coq.setoid_ring.Ring_polynom]
pe2:373 [in Coq.micromega.EnvRing]
pe2:391 [in Coq.setoid_ring.Ring_polynom]
pe:150 [in Coq.setoid_ring.Ncring_polynom]
pe:186 [in Coq.setoid_ring.Field_theory]
pe:191 [in Coq.setoid_ring.Ncring_polynom]
pe:195 [in Coq.setoid_ring.Ncring_polynom]
pe:197 [in Coq.setoid_ring.Ncring_polynom]
pe:199 [in Coq.setoid_ring.Ncring_polynom]
pe:206 [in Coq.setoid_ring.Ncring_polynom]
pe:323 [in Coq.setoid_ring.Ring_polynom]
pe:337 [in Coq.micromega.EnvRing]
pe:351 [in Coq.setoid_ring.Ring_polynom]
pe:355 [in Coq.setoid_ring.Ring_polynom]
pe:356 [in Coq.setoid_ring.Ring_polynom]
pe:360 [in Coq.setoid_ring.Ring_polynom]
pe:362 [in Coq.setoid_ring.Ring_polynom]
pe:364 [in Coq.setoid_ring.Ring_polynom]
pe:365 [in Coq.micromega.EnvRing]
pe:369 [in Coq.micromega.EnvRing]
pe:370 [in Coq.micromega.EnvRing]
pe:374 [in Coq.micromega.EnvRing]
pe:376 [in Coq.micromega.EnvRing]
pe:386 [in Coq.setoid_ring.Ring_polynom]
pe:42 [in Coq.nsatz.NsatzTactic]
pe:507 [in Coq.setoid_ring.Ring_polynom]
pe:533 [in Coq.setoid_ring.Ring_polynom]
pe:91 [in Coq.Logic.ClassicalFacts]
pe:92 [in Coq.Logic.ClassicalFacts]
pfs:312 [in Coq.micromega.ZMicromega]
pf:13 [in Coq.Strings.Byte]
pf:14 [in Coq.Strings.Byte]
pf:18 [in Coq.omega.PreOmega]
pf:19 [in Coq.omega.PreOmega]
pf:21 [in Coq.omega.PreOmega]
pf:22 [in Coq.omega.PreOmega]
pf:303 [in Coq.micromega.ZMicromega]
pf:317 [in Coq.micromega.ZMicromega]
pf:320 [in Coq.micromega.ZMicromega]
pf:326 [in Coq.micromega.ZMicromega]
pf:328 [in Coq.micromega.ZMicromega]
pf:330 [in Coq.micromega.ZMicromega]
pf:332 [in Coq.micromega.ZMicromega]
Pf:570 [in Coq.ssr.ssrbool]
Pf:573 [in Coq.ssr.ssrbool]
Pgoal:113 [in Coq.ssr.ssreflect]
Pgoal:75 [in Coq.ssr.ssreflect]
Pgoal:78 [in Coq.ssr.ssreflect]
Pgoal:84 [in Coq.ssr.ssreflect]
Pgt:118 [in Coq.Init.Datatypes]
Pgt:123 [in Coq.Init.Datatypes]
Pgt:128 [in Coq.Init.Datatypes]
Phf:624 [in Coq.ssr.ssrbool]
Phf:626 [in Coq.ssr.ssrbool]
Phf:628 [in Coq.ssr.ssrbool]
phi1:245 [in Coq.Reals.RiemannInt]
phi2:246 [in Coq.Reals.RiemannInt]
phi:303 [in Coq.setoid_ring.Ring_theory]
phi:5 [in Coq.Reals.RiemannInt]
phP:544 [in Coq.ssr.ssrbool]
Ph:617 [in Coq.ssr.ssrbool]
Ph:618 [in Coq.ssr.ssrbool]
Ph:619 [in Coq.ssr.ssrbool]
Ph:625 [in Coq.ssr.ssrbool]
Ph:627 [in Coq.ssr.ssrbool]
Ph:629 [in Coq.ssr.ssrbool]
Ph:644 [in Coq.ssr.ssrbool]
Ph:649 [in Coq.ssr.ssrbool]
Ph:657 [in Coq.ssr.ssrbool]
Ph:665 [in Coq.ssr.ssrbool]
Plemma:112 [in Coq.ssr.ssreflect]
Plemma:74 [in Coq.ssr.ssreflect]
Plemma:79 [in Coq.ssr.ssreflect]
Plemma:83 [in Coq.ssr.ssreflect]
plow:40 [in Coq.Reals.Runcountable]
plow:48 [in Coq.Reals.Runcountable]
plow:62 [in Coq.Reals.Runcountable]
Plt:117 [in Coq.Init.Datatypes]
Plt:122 [in Coq.Init.Datatypes]
Plt:127 [in Coq.Init.Datatypes]
pl:10 [in Coq.btauto.Reflect]
pl:117 [in Coq.btauto.Algebra]
pl:12 [in Coq.btauto.Reflect]
pl:126 [in Coq.btauto.Algebra]
pl:131 [in Coq.btauto.Algebra]
pl:143 [in Coq.btauto.Algebra]
pl:147 [in Coq.btauto.Algebra]
pl:15 [in Coq.btauto.Reflect]
pl:35 [in Coq.btauto.Algebra]
pl:65 [in Coq.btauto.Algebra]
pl:84 [in Coq.btauto.Algebra]
pm:16 [in Coq.Floats.FloatOps]
pnemf:54 [in Coq.Numbers.DecimalQ]
pnemf:55 [in Coq.Numbers.DecimalQ]
pnemf:63 [in Coq.Numbers.HexadecimalQ]
pnemf:64 [in Coq.Numbers.HexadecimalQ]
polarity:134 [in Coq.micromega.Tauto]
pol:173 [in Coq.micromega.Tauto]
pol:193 [in Coq.micromega.Tauto]
pol:196 [in Coq.micromega.Tauto]
pol:207 [in Coq.micromega.Tauto]
pol:306 [in Coq.micromega.Tauto]
pol:91 [in Coq.micromega.Tauto]
post:311 [in Coq.micromega.ZMicromega]
posz:310 [in Coq.micromega.ZMicromega]
pos:222 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
PP':115 [in Coq.setoid_ring.Ring_polynom]
PP':117 [in Coq.micromega.EnvRing]
pp:396 [in Coq.ssr.ssrbool]
pp:399 [in Coq.ssr.ssrbool]
pqr:419 [in Coq.Init.Specif]
pqr:429 [in Coq.Init.Specif]
pqr:572 [in Coq.Init.Specif]
pqr:582 [in Coq.Init.Specif]
PQ':113 [in Coq.setoid_ring.Ring_polynom]
PQ':115 [in Coq.micromega.EnvRing]
pq:155 [in Coq.Init.Specif]
pq:162 [in Coq.Init.Specif]
pq:301 [in Coq.Init.Specif]
pq:308 [in Coq.Init.Specif]
pq:440 [in Coq.Init.Logic]
pq:483 [in Coq.Init.Logic]
Pratan:327 [in Coq.Reals.Ratan]
pred:84 [in Coq.MSets.MSetRBT]
preo:134 [in Coq.Classes.CRelationClasses]
preo:169 [in Coq.Classes.RelationClasses]
pres:70 [in Coq.MSets.MSetAVL]
pres:78 [in Coq.MSets.MSetAVL]
prf:14 [in Coq.micromega.Ztac]
prf:144 [in Coq.micromega.RingMicromega]
prf:147 [in Coq.micromega.RingMicromega]
Prf:263 [in Coq.Reals.Ranalysis5]
prf:301 [in Coq.micromega.ZMicromega]
Prf:313 [in Coq.Reals.Ranalysis5]
Prf:369 [in Coq.Reals.Ranalysis5]
Prf:412 [in Coq.Reals.Ranalysis5]
Prf:429 [in Coq.Reals.Ranalysis5]
prf:77 [in Coq.rtauto.Rtauto]
Prg_incr:314 [in Coq.Reals.Ranalysis5]
Prg_incr:265 [in Coq.Reals.Ranalysis5]
Prg:264 [in Coq.Reals.Ranalysis5]
Prg:370 [in Coq.Reals.Ranalysis5]
Prmymeta:328 [in Coq.Reals.Ratan]
property:90 [in Coq.ssr.ssrbool]
pr0:441 [in Coq.Reals.RiemannInt]
pr1:11 [in Coq.Reals.Ranalysis4]
pr1:112 [in Coq.Reals.NewtonInt]
pr1:134 [in Coq.Reals.SeqProp]
pr1:137 [in Coq.Reals.SeqProp]
pr1:150 [in Coq.Reals.MVT]
Pr1:184 [in Coq.Reals.Ranalysis5]
pr1:211 [in Coq.Reals.RiemannInt]
pr1:23 [in Coq.Reals.Ranalysis5]
Pr1:248 [in Coq.Reals.Ranalysis5]
pr1:260 [in Coq.Reals.RiemannInt]
pr1:303 [in Coq.Reals.RiemannInt]
pr1:31 [in Coq.Reals.Ranalysis3]
pr1:333 [in Coq.Reals.RiemannInt_SF]
pr1:342 [in Coq.Reals.RiemannInt]
pr1:362 [in Coq.Reals.Ranalysis1]
pr1:366 [in Coq.Reals.Ranalysis1]
pr1:369 [in Coq.Reals.Ranalysis1]
pr1:372 [in Coq.Reals.Ranalysis1]
pr1:375 [in Coq.Reals.Ranalysis1]
pr1:379 [in Coq.Reals.Ranalysis1]
pr1:381 [in Coq.Reals.RiemannInt]
pr1:384 [in Coq.Reals.Ranalysis1]
pr1:389 [in Coq.Reals.Ranalysis1]
pr1:420 [in Coq.Reals.RiemannInt]
pr1:428 [in Coq.Reals.Ranalysis1]
pr1:433 [in Coq.Reals.Ranalysis1]
pr1:466 [in Coq.Reals.RiemannInt]
pr1:501 [in Coq.Reals.RiemannInt]
pr1:6 [in Coq.Reals.Ranalysis4]
pr1:6 [in Coq.Reals.MVT]
pr1:62 [in Coq.Reals.NewtonInt]
pr1:66 [in Coq.Reals.RiemannInt]
Pr1:71 [in Coq.Reals.Ratan]
pr1:87 [in Coq.Reals.RiemannInt]
pr1:99 [in Coq.Reals.SeqProp]
pr2:100 [in Coq.Reals.SeqProp]
pr2:113 [in Coq.Reals.NewtonInt]
pr2:12 [in Coq.Reals.Ranalysis4]
pr2:135 [in Coq.Reals.SeqProp]
pr2:138 [in Coq.Reals.SeqProp]
pr2:151 [in Coq.Reals.MVT]
pr2:212 [in Coq.Reals.RiemannInt]
pr2:24 [in Coq.Reals.Ranalysis5]
pr2:261 [in Coq.Reals.RiemannInt]
pr2:304 [in Coq.Reals.RiemannInt]
pr2:32 [in Coq.Reals.Ranalysis3]
pr2:334 [in Coq.Reals.RiemannInt_SF]
pr2:344 [in Coq.Reals.RiemannInt]
pr2:363 [in Coq.Reals.Ranalysis1]
pr2:380 [in Coq.Reals.Ranalysis1]
pr2:382 [in Coq.Reals.RiemannInt]
pr2:385 [in Coq.Reals.Ranalysis1]
pr2:390 [in Coq.Reals.Ranalysis1]
pr2:421 [in Coq.Reals.RiemannInt]
pr2:429 [in Coq.Reals.Ranalysis1]
pr2:434 [in Coq.Reals.Ranalysis1]
pr2:467 [in Coq.Reals.RiemannInt]
pr2:502 [in Coq.Reals.RiemannInt]
pr2:52 [in Coq.Reals.Runcountable]
pr2:63 [in Coq.Reals.NewtonInt]
pr2:67 [in Coq.Reals.RiemannInt]
pr2:7 [in Coq.Reals.Ranalysis4]
pr2:8 [in Coq.Reals.MVT]
pr2:88 [in Coq.Reals.RiemannInt]
pr3:263 [in Coq.Reals.RiemannInt]
pr3:306 [in Coq.Reals.RiemannInt]
pr3:335 [in Coq.Reals.RiemannInt_SF]
pr3:468 [in Coq.Reals.RiemannInt]
pr3:503 [in Coq.Reals.RiemannInt]
pr:106 [in Coq.Reals.MVT]
pr:11 [in Coq.btauto.Reflect]
pr:110 [in Coq.Reals.MVT]
pr:118 [in Coq.btauto.Algebra]
pr:119 [in Coq.Reals.MVT]
pr:12 [in Coq.Reals.RiemannInt]
pr:127 [in Coq.Reals.Ranalysis1]
pr:127 [in Coq.btauto.Algebra]
pr:129 [in Coq.Reals.Ranalysis1]
pr:129 [in Coq.Reals.MVT]
pr:13 [in Coq.btauto.Reflect]
pr:132 [in Coq.btauto.Algebra]
pr:136 [in Coq.Reals.Ranalysis1]
pr:136 [in Coq.Reals.MVT]
pr:143 [in Coq.Reals.SeqProp]
pr:144 [in Coq.Reals.MVT]
pr:144 [in Coq.btauto.Algebra]
pr:146 [in Coq.Reals.SeqProp]
pr:148 [in Coq.btauto.Algebra]
pr:154 [in Coq.Reals.SeqProp]
pr:159 [in Coq.Reals.MVT]
pr:16 [in Coq.btauto.Reflect]
pr:172 [in Coq.Reals.SeqProp]
pr:173 [in Coq.Reals.Ranalysis1]
pr:177 [in Coq.Reals.Ranalysis1]
pr:18 [in Coq.Reals.RiemannInt]
pr:181 [in Coq.Reals.Ranalysis1]
pr:185 [in Coq.Reals.Ranalysis1]
pr:203 [in Coq.Reals.Ranalysis1]
pr:21 [in Coq.Reals.SeqProp]
pr:22 [in Coq.Reals.Ranalysis4]
pr:233 [in Coq.Reals.RiemannInt]
pr:24 [in Coq.Reals.SeqProp]
pr:28 [in Coq.Logic.ConstructiveEpsilon]
pr:29 [in Coq.Reals.NewtonInt]
pr:30 [in Coq.Reals.MVT]
pr:313 [in Coq.Reals.RiemannInt]
pr:33 [in Coq.Reals.SeqProp]
pr:338 [in Coq.Reals.Ratan]
pr:339 [in Coq.Reals.Ratan]
pr:36 [in Coq.btauto.Algebra]
pr:37 [in Coq.Reals.SeqProp]
pr:395 [in Coq.micromega.ZMicromega]
pr:396 [in Coq.Reals.Ranalysis1]
pr:397 [in Coq.micromega.ZMicromega]
pr:41 [in Coq.Reals.SeqProp]
pr:433 [in Coq.Reals.RiemannInt]
pr:439 [in Coq.Reals.Ranalysis1]
pr:440 [in Coq.Reals.RiemannInt]
pr:445 [in Coq.Reals.Ranalysis1]
pr:453 [in Coq.Reals.Ranalysis1]
pr:456 [in Coq.Reals.Ranalysis1]
pr:50 [in Coq.Reals.Runcountable]
pr:550 [in Coq.Reals.RiemannInt]
pr:556 [in Coq.Reals.RiemannInt]
pr:56 [in Coq.Reals.RiemannInt]
pr:67 [in Coq.Reals.SeqProp]
pr:68 [in Coq.btauto.Algebra]
pr:70 [in Coq.Reals.MVT]
pr:71 [in Coq.btauto.Algebra]
pr:74 [in Coq.Reals.Runcountable]
pr:76 [in Coq.Reals.Ratan]
pr:79 [in Coq.Reals.MVT]
pr:8 [in Coq.Reals.Sqrt_reg]
pr:8 [in Coq.Reals.NewtonInt]
pr:82 [in Coq.Reals.MVT]
pr:82 [in Coq.Reals.RiemannInt]
pr:86 [in Coq.Reals.MVT]
pr:87 [in Coq.btauto.Algebra]
pr:95 [in Coq.Reals.MVT]
pr:99 [in Coq.Reals.MVT]
psi1:213 [in Coq.Reals.RiemannInt]
psi1:216 [in Coq.Reals.RiemannInt]
psi1:247 [in Coq.Reals.RiemannInt]
psi1:274 [in Coq.Reals.RiemannInt]
psi1:277 [in Coq.Reals.RiemannInt]
psi1:316 [in Coq.Reals.RiemannInt]
psi1:321 [in Coq.Reals.RiemannInt]
psi1:386 [in Coq.Reals.RiemannInt]
psi1:391 [in Coq.Reals.RiemannInt]
psi1:471 [in Coq.Reals.RiemannInt]
psi1:474 [in Coq.Reals.RiemannInt]
psi2:219 [in Coq.Reals.RiemannInt]
psi2:222 [in Coq.Reals.RiemannInt]
psi2:248 [in Coq.Reals.RiemannInt]
psi2:282 [in Coq.Reals.RiemannInt]
psi2:285 [in Coq.Reals.RiemannInt]
psi2:361 [in Coq.Reals.RiemannInt]
psi2:364 [in Coq.Reals.RiemannInt]
psi2:367 [in Coq.Reals.RiemannInt]
psi2:370 [in Coq.Reals.RiemannInt]
psi2:406 [in Coq.Reals.RiemannInt]
psi2:409 [in Coq.Reals.RiemannInt]
psi2:479 [in Coq.Reals.RiemannInt]
psi2:482 [in Coq.Reals.RiemannInt]
psi3:290 [in Coq.Reals.RiemannInt]
psi3:293 [in Coq.Reals.RiemannInt]
psi3:353 [in Coq.Reals.RiemannInt]
psi3:356 [in Coq.Reals.RiemannInt]
psi3:487 [in Coq.Reals.RiemannInt]
psi3:490 [in Coq.Reals.RiemannInt]
psi:20 [in Coq.Reals.RiemannInt]
psi:6 [in Coq.Reals.RiemannInt]
PS:15 [in Coq.Vectors.Fin]
PS:19 [in Coq.Vectors.Fin]
PS:22 [in Coq.Vectors.Fin]
PS:29 [in Coq.Vectors.Fin]
PS:38 [in Coq.Vectors.Fin]
pT':260 [in Coq.ssr.ssrbool]
pT:258 [in Coq.ssr.ssrbool]
pT:355 [in Coq.ssr.ssrbool]
pT:395 [in Coq.ssr.ssrbool]
pT:397 [in Coq.ssr.ssrbool]
pt:408 [in Coq.micromega.ZMicromega]
pt:412 [in Coq.micromega.ZMicromega]
P_hprop:359 [in Coq.Init.Specif]
P_hprop:343 [in Coq.Init.Specif]
P_hprop:259 [in Coq.Init.Specif]
P_hprop:221 [in Coq.Init.Specif]
P_hprop:502 [in Coq.Init.Logic]
P_hprop:454 [in Coq.Init.Logic]
P'':106 [in Coq.setoid_ring.Ring_polynom]
P'':108 [in Coq.micromega.EnvRing]
p':11 [in Coq.Floats.FloatLemmas]
p':125 [in Coq.FSets.FMapInterface]
p':126 [in Coq.Structures.OrderedType]
p':128 [in Coq.Structures.OrderedType]
p':130 [in Coq.Structures.OrderedType]
P':130 [in Coq.setoid_ring.Ncring_polynom]
P':134 [in Coq.setoid_ring.Ncring_polynom]
p':137 [in Coq.FSets.FMapPositive]
p':139 [in Coq.FSets.FMapPositive]
p':141 [in Coq.FSets.FMapPositive]
P':174 [in Coq.Init.Specif]
p':195 [in Coq.Init.Specif]
P':197 [in Coq.micromega.EnvRing]
p':2 [in Coq.NArith.Ndec]
P':200 [in Coq.micromega.EnvRing]
p':204 [in Coq.Init.Specif]
P':210 [in Coq.setoid_ring.Ring_polynom]
P':212 [in Coq.setoid_ring.Ring_polynom]
p':219 [in Coq.NArith.BinNat]
p':225 [in Coq.NArith.BinNat]
p':231 [in Coq.NArith.BinNat]
p':237 [in Coq.NArith.BinNat]
P':241 [in Coq.setoid_ring.Ring_polynom]
P':244 [in Coq.micromega.EnvRing]
P':247 [in Coq.setoid_ring.Ring_polynom]
P':250 [in Coq.setoid_ring.Ring_polynom]
P':250 [in Coq.micromega.EnvRing]
P':252 [in Coq.setoid_ring.Ring_polynom]
P':253 [in Coq.micromega.EnvRing]
P':255 [in Coq.setoid_ring.Ring_polynom]
P':259 [in Coq.micromega.EnvRing]
P':262 [in Coq.setoid_ring.Ring_polynom]
P':262 [in Coq.micromega.EnvRing]
P':269 [in Coq.micromega.EnvRing]
P':28 [in Coq.NArith.BinNat]
p':284 [in Coq.Lists.SetoidList]
p':287 [in Coq.Lists.SetoidList]
p':289 [in Coq.Lists.SetoidList]
p':291 [in Coq.Lists.SetoidList]
p':293 [in Coq.Lists.SetoidList]
p':295 [in Coq.Lists.SetoidList]
p':3 [in Coq.Structures.DecidableType]
P':31 [in Coq.setoid_ring.Ring_polynom]
P':33 [in Coq.micromega.EnvRing]
P':35 [in Coq.nsatz.NsatzTactic]
P':38 [in Coq.setoid_ring.Ncring_polynom]
P':39 [in Coq.nsatz.NsatzTactic]
p':39 [in Coq.FSets.FMapInterface]
p':39 [in Coq.NArith.Ndigits]
p':4 [in Coq.NArith.Ndec]
p':41 [in Coq.FSets.FMapInterface]
P':42 [in Coq.NArith.BinNat]
P':44 [in Coq.nsatz.NsatzTactic]
p':45 [in Coq.NArith.Ndigits]
p':5 [in Coq.Structures.DecidableType]
p':51 [in Coq.NArith.Ndigits]
p':52 [in Coq.Numbers.HexadecimalPos]
p':52 [in Coq.Numbers.DecimalPos]
p':57 [in Coq.NArith.Ndigits]
p':6 [in Coq.NArith.Ndec]
p':615 [in Coq.FSets.FMapFacts]
p':617 [in Coq.FSets.FMapFacts]
p':623 [in Coq.FSets.FMapFacts]
p':625 [in Coq.FSets.FMapFacts]
p':67 [in Coq.Numbers.DecimalPos]
p':68 [in Coq.NArith.Ndigits]
P':7 [in Coq.Logic.ClassicalChoice]
p':71 [in Coq.Numbers.HexadecimalPos]
P':71 [in Coq.setoid_ring.Ncring_polynom]
p':74 [in Coq.PArith.BinPosDef]
p':76 [in Coq.PArith.BinPosDef]
P':81 [in Coq.setoid_ring.Ring_polynom]
P':83 [in Coq.micromega.EnvRing]
P':87 [in Coq.setoid_ring.Ring_polynom]
p':88 [in Coq.Program.Wf]
P':89 [in Coq.micromega.EnvRing]
p':9 [in Coq.Floats.FloatLemmas]
P':90 [in Coq.setoid_ring.Ncring_polynom]
p0:100 [in Coq.Vectors.VectorDef]
p0:162 [in Coq.FSets.FMapPositive]
p0:167 [in Coq.FSets.FMapPositive]
p0:20 [in Coq.Floats.FloatLemmas]
p0:21 [in Coq.Floats.FloatLemmas]
p0:22 [in Coq.Floats.FloatLemmas]
p0:23 [in Coq.Floats.FloatLemmas]
p0:38 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p0:41 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p0:44 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p0:47 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p1:102 [in Coq.micromega.ZifyClasses]
p1:105 [in Coq.Vectors.VectorSpec]
p1:110 [in Coq.Logic.Eqdep_dec]
p1:111 [in Coq.Vectors.VectorSpec]
p1:113 [in Coq.setoid_ring.Field_theory]
p1:116 [in Coq.setoid_ring.Field_theory]
P1:118 [in Coq.micromega.ZifyClasses]
P1:118 [in Coq.ssr.ssrbool]
p1:123 [in Coq.Logic.EqdepFacts]
P1:123 [in Coq.ssr.ssrbool]
p1:127 [in Coq.Logic.EqdepFacts]
P1:129 [in Coq.ssr.ssrbool]
P1:13 [in Coq.Vectors.Fin]
P1:133 [in Coq.micromega.ZifyClasses]
P1:136 [in Coq.ssr.ssrbool]
p1:139 [in Coq.Logic.Eqdep_dec]
P1:141 [in Coq.ssr.ssrbool]
P1:144 [in Coq.micromega.ZifyClasses]
p1:15 [in Coq.micromega.Ztac]
p1:151 [in Coq.Vectors.VectorSpec]
P1:155 [in Coq.micromega.EnvRing]
p1:159 [in Coq.Logic.EqdepFacts]
P1:160 [in Coq.setoid_ring.Ring_polynom]
p1:161 [in Coq.Vectors.VectorSpec]
P1:161 [in Coq.micromega.EnvRing]
p1:164 [in Coq.Logic.EqdepFacts]
P1:167 [in Coq.micromega.EnvRing]
P1:168 [in Coq.setoid_ring.Ring_polynom]
p1:17 [in Coq.micromega.Ztac]
P1:172 [in Coq.micromega.EnvRing]
P1:174 [in Coq.setoid_ring.Ring_polynom]
P1:177 [in Coq.micromega.EnvRing]
P1:179 [in Coq.setoid_ring.Ring_polynom]
P1:18 [in Coq.Vectors.Fin]
P1:182 [in Coq.micromega.EnvRing]
P1:184 [in Coq.setoid_ring.Ring_polynom]
P1:189 [in Coq.setoid_ring.Ring_polynom]
P1:189 [in Coq.setoid_ring.Ncring_polynom]
p1:2 [in Coq.Logic.ProofIrrelevance]
p1:2 [in Coq.Logic.ProofIrrelevanceFacts]
p1:20 [in Coq.Vectors.VectorSpec]
P1:21 [in Coq.Vectors.Fin]
p1:211 [in Coq.setoid_ring.Field_theory]
p1:215 [in Coq.setoid_ring.Field_theory]
p1:228 [in Coq.setoid_ring.Field_theory]
p1:232 [in Coq.setoid_ring.Field_theory]
p1:235 [in Coq.ssr.ssrbool]
p1:238 [in Coq.Logic.EqdepFacts]
p1:238 [in Coq.ssr.ssrbool]
p1:24 [in Coq.Logic.Eqdep_dec]
p1:241 [in Coq.ssr.ssrbool]
p1:246 [in Coq.ssr.ssrbool]
P1:26 [in Coq.Vectors.Fin]
p1:269 [in Coq.ssr.ssrbool]
p1:272 [in Coq.ssr.ssrbool]
p1:277 [in Coq.ssr.ssrbool]
P1:285 [in Coq.setoid_ring.Ring_polynom]
p1:29 [in Coq.micromega.Ztac]
p1:29 [in Coq.Logic.Classical_Prop]
P1:291 [in Coq.setoid_ring.Ring_polynom]
P1:296 [in Coq.setoid_ring.Ring_polynom]
P1:301 [in Coq.micromega.EnvRing]
P1:307 [in Coq.setoid_ring.Ring_polynom]
P1:307 [in Coq.micromega.EnvRing]
P1:311 [in Coq.setoid_ring.Ring_polynom]
P1:312 [in Coq.micromega.EnvRing]
P1:317 [in Coq.setoid_ring.Ring_polynom]
P1:323 [in Coq.micromega.EnvRing]
P1:327 [in Coq.micromega.EnvRing]
p1:33 [in Coq.micromega.Ztac]
P1:333 [in Coq.micromega.EnvRing]
P1:349 [in Coq.setoid_ring.Ring_polynom]
P1:35 [in Coq.Vectors.Fin]
P1:363 [in Coq.micromega.EnvRing]
p1:41 [in Coq.Logic.Eqdep_dec]
p1:49 [in Coq.micromega.ZifyClasses]
p1:5 [in Coq.Logic.PropExtensionality]
p1:56 [in Coq.micromega.ZifyClasses]
p1:64 [in Coq.Init.Datatypes]
P1:66 [in Coq.setoid_ring.Ncring_polynom]
P1:78 [in Coq.setoid_ring.Ncring_polynom]
p1:90 [in Coq.Logic.Eqdep_dec]
p1:97 [in Coq.micromega.ZifyClasses]
p1:99 [in Coq.Vectors.VectorSpec]
p2:100 [in Coq.Vectors.VectorSpec]
p2:106 [in Coq.Vectors.VectorSpec]
p2:111 [in Coq.Logic.Eqdep_dec]
p2:112 [in Coq.Vectors.VectorSpec]
p2:114 [in Coq.setoid_ring.Field_theory]
P2:115 [in Coq.setoid_ring.Ncring_polynom]
p2:117 [in Coq.setoid_ring.Field_theory]
P2:119 [in Coq.ssr.ssrbool]
P2:121 [in Coq.micromega.ZifyClasses]
P2:123 [in Coq.micromega.EnvRing]
p2:124 [in Coq.Logic.EqdepFacts]
P2:124 [in Coq.ssr.ssrbool]
P2:125 [in Coq.setoid_ring.Ncring_polynom]
P2:130 [in Coq.ssr.ssrbool]
P2:137 [in Coq.ssr.ssrbool]
p2:140 [in Coq.Logic.Eqdep_dec]
P2:142 [in Coq.ssr.ssrbool]
P2:147 [in Coq.micromega.ZifyClasses]
p2:152 [in Coq.Vectors.VectorSpec]
P2:157 [in Coq.micromega.EnvRing]
p2:16 [in Coq.micromega.Ztac]
p2:162 [in Coq.Vectors.VectorSpec]
P2:162 [in Coq.setoid_ring.Ring_polynom]
P2:163 [in Coq.micromega.EnvRing]
P2:169 [in Coq.micromega.EnvRing]
P2:170 [in Coq.setoid_ring.Ring_polynom]
P2:176 [in Coq.setoid_ring.Ring_polynom]
p2:18 [in Coq.micromega.Ztac]
P2:190 [in Coq.setoid_ring.Ncring_polynom]
p2:21 [in Coq.Vectors.VectorSpec]
p2:213 [in Coq.setoid_ring.Field_theory]
p2:217 [in Coq.setoid_ring.Field_theory]
p2:229 [in Coq.setoid_ring.Field_theory]
p2:234 [in Coq.setoid_ring.Field_theory]
p2:236 [in Coq.ssr.ssrbool]
p2:239 [in Coq.Logic.EqdepFacts]
p2:239 [in Coq.ssr.ssrbool]
p2:242 [in Coq.ssr.ssrbool]
p2:247 [in Coq.ssr.ssrbool]
p2:25 [in Coq.Logic.Eqdep_dec]
p2:270 [in Coq.ssr.ssrbool]
p2:273 [in Coq.ssr.ssrbool]
p2:278 [in Coq.ssr.ssrbool]
P2:287 [in Coq.setoid_ring.Ring_polynom]
P2:293 [in Coq.setoid_ring.Ring_polynom]
P2:298 [in Coq.setoid_ring.Ring_polynom]
p2:3 [in Coq.Logic.ProofIrrelevance]
p2:3 [in Coq.Logic.ProofIrrelevanceFacts]
p2:30 [in Coq.Logic.Classical_Prop]
P2:303 [in Coq.micromega.EnvRing]
P2:309 [in Coq.micromega.EnvRing]
p2:31 [in Coq.micromega.Ztac]
P2:312 [in Coq.setoid_ring.Ring_polynom]
P2:314 [in Coq.micromega.EnvRing]
P2:328 [in Coq.micromega.EnvRing]
p2:35 [in Coq.micromega.Ztac]
P2:350 [in Coq.setoid_ring.Ring_polynom]
P2:364 [in Coq.micromega.EnvRing]
p2:42 [in Coq.Logic.Eqdep_dec]
p2:50 [in Coq.micromega.ZifyClasses]
p2:6 [in Coq.Logic.PropExtensionality]
p2:65 [in Coq.Init.Datatypes]
P2:67 [in Coq.setoid_ring.Ncring_polynom]
P2:79 [in Coq.setoid_ring.Ncring_polynom]
p2:91 [in Coq.Logic.Eqdep_dec]
p2:98 [in Coq.micromega.ZifyClasses]
P3:120 [in Coq.ssr.ssrbool]
P3:125 [in Coq.ssr.ssrbool]
P3:131 [in Coq.ssr.ssrbool]
P3:138 [in Coq.ssr.ssrbool]
P3:143 [in Coq.ssr.ssrbool]
p3:163 [in Coq.Vectors.VectorSpec]
P3:288 [in Coq.setoid_ring.Ring_polynom]
P3:300 [in Coq.setoid_ring.Ring_polynom]
P3:304 [in Coq.micromega.EnvRing]
P3:316 [in Coq.micromega.EnvRing]
P4:126 [in Coq.ssr.ssrbool]
P4:132 [in Coq.ssr.ssrbool]
P4:144 [in Coq.ssr.ssrbool]
P5:133 [in Coq.ssr.ssrbool]
P:1 [in Coq.Logic.Decidable]
P:1 [in Coq.Arith.Div2]
P:1 [in Coq.Reals.Abstract.ConstructiveLUB]
P:1 [in Coq.FSets.FSetDecide]
P:1 [in Coq.ZArith.Zabs]
P:1 [in Coq.Logic.ProofIrrelevance]
p:1 [in Coq.PArith.Pnat]
P:1 [in Coq.Logic.PropExtensionality]
P:1 [in Coq.btauto.Algebra]
P:1 [in Coq.MSets.MSetDecide]
P:1 [in Coq.ssr.ssrfun]
P:1 [in Coq.Reals.Rpower]
p:1 [in Coq.rtauto.Bintree]
p:1 [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
p:1 [in Coq.NArith.Ndigits]
P:1 [in Coq.Logic.Berardi]
P:1 [in Coq.Logic.ProofIrrelevanceFacts]
P:1 [in Coq.Logic.HLevels]
P:1 [in Coq.Logic.ClassicalDescription]
P:1 [in Coq.Logic.Classical_Prop]
P:1 [in Coq.Classes.DecidableClass]
P:1 [in Coq.Logic.Diaconescu]
p:1 [in Coq.Numbers.NatInt.NZMulOrder]
P:1 [in Coq.Logic.WKL]
p:1 [in Coq.QArith.Qround]
P:1 [in Coq.Reals.ClassicalDedekindReals]
p:1 [in Coq.NArith.Ndec]
P:1 [in Coq.Logic.WeakFan]
P:10 [in Coq.Logic.Classical_Pred_Type]
p:10 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
p:10 [in Coq.Logic.EqdepFacts]
p:10 [in Coq.Floats.FloatLemmas]
P:10 [in Coq.Reals.MVT]
P:10 [in Coq.Logic.ClassicalEpsilon]
p:10 [in Coq.PArith.Pnat]
P:10 [in Coq.Init.Logic_Type]
p:10 [in Coq.Program.Equality]
p:10 [in Coq.extraction.ExtrOcamlBigIntConv]
p:10 [in Coq.Numbers.Natural.Abstract.NMulOrder]
P:10 [in Coq.Logic.PropExtensionalityFacts]
p:10 [in Coq.extraction.ExtrOcamlIntConv]
p:10 [in Coq.Numbers.Natural.Abstract.NAdd]
p:10 [in Coq.ZArith.Zcompare]
P:10 [in Coq.Logic.WeakFan]
p:100 [in Coq.Logic.Eqdep_dec]
P:100 [in Coq.Logic.EqdepFacts]
p:100 [in Coq.btauto.Algebra]
P:100 [in Coq.Logic.ChoiceFacts]
P:100 [in Coq.Init.Specif]
p:100 [in Coq.ZArith.Int]
p:100 [in Coq.ZArith.Zorder]
P:100 [in Coq.setoid_ring.Ncring_polynom]
P:101 [in Coq.setoid_ring.Ring_polynom]
P:101 [in Coq.ssr.ssrbool]
p:101 [in Coq.ZArith.Znat]
p:102 [in Coq.Reals.Abstract.ConstructiveReals]
p:102 [in Coq.Numbers.Integer.Abstract.ZAdd]
p:102 [in Coq.PArith.BinPos]
P:102 [in Coq.Arith.Wf_nat]
p:102 [in Coq.omega.OmegaLemmas]
p:102 [in Coq.ZArith.Int]
p:102 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
p:102 [in Coq.ZArith.Znat]
p:103 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
P:103 [in Coq.micromega.EnvRing]
p:103 [in Coq.btauto.Algebra]
p:103 [in Coq.Numbers.Integer.Abstract.ZLcm]
P:103 [in Coq.MSets.MSetList]
P:103 [in Coq.omega.OmegaLemmas]
p:103 [in Coq.ZArith.Zorder]
P:103 [in Coq.setoid_ring.Ncring_polynom]
P:104 [in Coq.MSets.MSetInterface]
P:104 [in Coq.Logic.Eqdep_dec]
p:104 [in Coq.Reals.Rtrigo1]
P:104 [in Coq.MSets.MSetProperties]
P:104 [in Coq.Init.Specif]
p:104 [in Coq.Logic.Hurkens]
p:104 [in Coq.micromega.OrderedRing]
p:104 [in Coq.Vectors.Fin]
P:104 [in Coq.FSets.FSetProperties]
p:105 [in Coq.Reals.Cauchy_prod]
p:105 [in Coq.Logic.Eqdep_dec]
P:105 [in Coq.setoid_ring.Ring_polynom]
P:105 [in Coq.Arith.Wf_nat]
p:105 [in Coq.btauto.Algebra]
p:105 [in Coq.setoid_ring.Field_theory]
P:105 [in Coq.ssr.ssrbool]
p:105 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
p:105 [in Coq.ZArith.Int]
p:105 [in Coq.Structures.GenericMinMax]
p:105 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
p:105 [in Coq.Reals.Abstract.ConstructiveMinMax]
p:106 [in Coq.Reals.Rtrigo1]
p:106 [in Coq.btauto.Algebra]
p:106 [in Coq.Numbers.Integer.Abstract.ZLcm]
p:106 [in Coq.setoid_ring.Field_theory]
P:106 [in Coq.MSets.MSetList]
p:106 [in Coq.Logic.Hurkens]
p:106 [in Coq.ZArith.Zorder]
P:106 [in Coq.MSets.MSetGenTree]
P:106 [in Coq.setoid_ring.Ncring_polynom]
p:106 [in Coq.Vectors.VectorDef]
p:107 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
P:107 [in Coq.MSets.MSetInterface]
p:107 [in Coq.Logic.EqdepFacts]
p:107 [in Coq.PArith.BinPos]
P:107 [in Coq.micromega.EnvRing]
P:107 [in Coq.Logic.ChoiceFacts]
P:107 [in Coq.ssr.ssrbool]
p:107 [in Coq.micromega.OrderedRing]
p:107 [in Coq.ZArith.Int]
p:107 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
p:108 [in Coq.Reals.Cauchy_prod]
p:108 [in Coq.Reals.Rtrigo1]
p:108 [in Coq.btauto.Algebra]
P:108 [in Coq.Init.Specif]
p:108 [in Coq.setoid_ring.Field_theory]
P:108 [in Coq.ssr.ssrbool]
P:108 [in Coq.setoid_ring.Ncring_polynom]
p:109 [in Coq.Numbers.Integer.Abstract.ZLcm]
P:109 [in Coq.ssr.ssrbool]
p:109 [in Coq.ZArith.Int]
p:109 [in Coq.ZArith.Zorder]
p:109 [in Coq.Vectors.Fin]
P:109 [in Coq.MSets.MSetGenTree]
p:109 [in Coq.Reals.Abstract.ConstructiveMinMax]
p:11 [in Coq.Arith.Minus]
p:11 [in Coq.Arith.Le]
p:11 [in Coq.Reals.Cauchy_prod]
p:11 [in Coq.setoid_ring.Ncring_initial]
p:11 [in Coq.Reals.Rminmax]
p:11 [in Coq.PArith.BinPos]
P:11 [in Coq.Logic.Epsilon]
p:11 [in Coq.PArith.Pnat]
P:11 [in Coq.Arith.Wf_nat]
P:11 [in Coq.ZArith.Wf_Z]
P:11 [in Coq.Init.Wf]
p:11 [in Coq.setoid_ring.InitialRing]
P:11 [in Coq.FSets.FSetInterface]
p:11 [in Coq.Arith.Plus]
p:11 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
p:11 [in Coq.Numbers.Natural.Abstract.NMaxMin]
p:11 [in Coq.Vectors.Fin]
P:11 [in Coq.Logic.ProofIrrelevanceFacts]
P:11 [in Coq.Logic.Classical_Prop]
P:11 [in Coq.Classes.DecidableClass]
p:11 [in Coq.Numbers.NatInt.NZMul]
p:11 [in Coq.Numbers.Natural.Abstract.NAdd]
p:11 [in Coq.QArith.Qreduction]
P:11 [in Coq.Logic.StrictProp]
p:110 [in Coq.Reals.Rtrigo1]
P:110 [in Coq.PArith.BinPos]
p:110 [in Coq.Arith.Wf_nat]
p:110 [in Coq.Init.Specif]
p:110 [in Coq.micromega.OrderedRing]
p:110 [in Coq.Vectors.Fin]
P:110 [in Coq.setoid_ring.Ncring_polynom]
p:111 [in Coq.Reals.Cauchy_prod]
p:111 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
P:111 [in Coq.FSets.FSetBridge]
p:111 [in Coq.Logic.EqdepFacts]
p:111 [in Coq.Arith.Wf_nat]
p:111 [in Coq.setoid_ring.Field_theory]
P:111 [in Coq.ssr.ssrbool]
p:111 [in Coq.ZArith.Int]
p:111 [in Coq.Vectors.VectorDef]
p:112 [in Coq.PArith.BinPos]
p:112 [in Coq.ZArith.BinInt]
p:112 [in Coq.Numbers.Integer.Abstract.ZLcm]
P:112 [in Coq.Init.Specif]
P:112 [in Coq.omega.OmegaLemmas]
p:112 [in Coq.ZArith.Zorder]
p:113 [in Coq.Logic.Eqdep_dec]
P:113 [in Coq.Arith.Wf_nat]
p:113 [in Coq.btauto.Algebra]
P:113 [in Coq.Logic.ChoiceFacts]
P:113 [in Coq.ssr.ssrbool]
p:113 [in Coq.Init.Nat]
p:113 [in Coq.ZArith.Zdiv]
p:113 [in Coq.ZArith.Int]
p:114 [in Coq.Reals.Cauchy_prod]
P:114 [in Coq.FSets.FSetBridge]
P:114 [in Coq.Logic.EqdepFacts]
p:114 [in Coq.PArith.BinPos]
p:114 [in Coq.Init.Specif]
p:114 [in Coq.Vectors.Fin]
P:115 [in Coq.Logic.Eqdep_dec]
p:115 [in Coq.Logic.EqdepFacts]
p:115 [in Coq.ZArith.Int]
p:115 [in Coq.ZArith.Zorder]
p:116 [in Coq.QArith.Qcanon]
p:116 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
p:116 [in Coq.Logic.Eqdep_dec]
P:116 [in Coq.Init.Specif]
P:116 [in Coq.ssr.ssrbool]
P:116 [in Coq.setoid_ring.Ncring_polynom]
p:116 [in Coq.PArith.BinPosDef]
p:117 [in Coq.Reals.Cauchy_prod]
p:117 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
P:117 [in Coq.Logic.Eqdep_dec]
p:117 [in Coq.Structures.GenericMinMax]
p:117 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
p:118 [in Coq.QArith.Qcanon]
p:118 [in Coq.Logic.Eqdep_dec]
P:118 [in Coq.Logic.EqdepFacts]
p:118 [in Coq.Arith.Wf_nat]
P:118 [in Coq.micromega.EnvRing]
P:118 [in Coq.ssr.ssreflect]
p:118 [in Coq.ZArith.Zorder]
p:118 [in Coq.NArith.Ndigits]
p:118 [in Coq.Vectors.Fin]
P:118 [in Coq.setoid_ring.Ncring_polynom]
p:119 [in Coq.Vectors.VectorSpec]
p:119 [in Coq.Logic.EqdepFacts]
P:119 [in Coq.PArith.BinPos]
p:119 [in Coq.Arith.Wf_nat]
p:119 [in Coq.setoid_ring.Field_theory]
P:119 [in Coq.omega.OmegaLemmas]
P:12 [in Coq.Logic.Decidable]
P:12 [in Coq.MSets.MSetEqProperties]
p:12 [in Coq.PArith.BinPos]
p:12 [in Coq.Floats.FloatLemmas]
P:12 [in Coq.Logic.ClassicalEpsilon]
p:12 [in Coq.PArith.Pnat]
p:12 [in Coq.QArith.Qminmax]
P:12 [in Coq.FSets.FSetEqProperties]
P:12 [in Coq.Vectors.Fin]
p:12 [in Coq.ZArith.ZArith_dec]
p:12 [in Coq.Logic.HLevels]
p:12 [in Coq.Structures.EqualitiesFacts]
P:12 [in Coq.Logic.Diaconescu]
p:12 [in Coq.Numbers.NatInt.NZMulOrder]
p:12 [in Coq.Arith.Mult]
p:12 [in Coq.Numbers.NatInt.NZAdd]
P:12 [in Coq.FSets.FSetCompat]
p:12 [in Coq.rtauto.Rtauto]
p:120 [in Coq.Reals.Cauchy_prod]
p:120 [in Coq.QArith.Qcanon]
p:120 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
p:120 [in Coq.PArith.BinPos]
p:120 [in Coq.Init.Specif]
p:120 [in Coq.Reals.Rbasic_fun]
p:120 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
P:120 [in Coq.Logic.ClassicalFacts]
p:120 [in Coq.Relations.Relation_Operators]
P:121 [in Coq.Logic.Eqdep_dec]
P:121 [in Coq.Arith.Wf_nat]
p:121 [in Coq.btauto.Algebra]
p:121 [in Coq.Init.Nat]
p:121 [in Coq.micromega.OrderedRing]
p:121 [in Coq.ZArith.Zorder]
p:122 [in Coq.ZArith.BinInt]
P:122 [in Coq.Init.Specif]
p:122 [in Coq.setoid_ring.Field_theory]
P:122 [in Coq.setoid_ring.Ncring_polynom]
p:1228 [in Coq.FSets.FMapAVL]
p:123 [in Coq.Logic.Eqdep_dec]
p:123 [in Coq.PArith.BinPos]
p:123 [in Coq.PArith.BinPosDef]
p:123 [in Coq.Relations.Relation_Operators]
p:124 [in Coq.ZArith.BinInt]
p:124 [in Coq.btauto.Algebra]
p:124 [in Coq.FSets.FMapInterface]
p:124 [in Coq.micromega.OrderedRing]
p:124 [in Coq.ZArith.Zorder]
p:124 [in Coq.ZArith.Znat]
p:124 [in Coq.Vectors.VectorDef]
p:125 [in Coq.NArith.Ndigits]
p:125 [in Coq.Structures.OrderedType]
P:125 [in Coq.Init.Logic]
P:126 [in Coq.Program.Wf]
P:126 [in Coq.PArith.BinPos]
p:126 [in Coq.Arith.Wf_nat]
p:126 [in Coq.Init.Specif]
P:126 [in Coq.omega.OmegaLemmas]
P:126 [in Coq.setoid_ring.Ncring_polynom]
p:126 [in Coq.ZArith.Znat]
P:127 [in Coq.setoid_ring.Ring_polynom]
p:127 [in Coq.Arith.Wf_nat]
p:127 [in Coq.micromega.OrderedRing]
p:127 [in Coq.ZArith.Zorder]
p:127 [in Coq.Structures.OrderedType]
p:128 [in Coq.PArith.BinPos]
P:128 [in Coq.Logic.ChoiceFacts]
P:128 [in Coq.Init.Specif]
p:128 [in Coq.Vectors.Fin]
p:128 [in Coq.PArith.BinPosDef]
p:129 [in Coq.Logic.Eqdep_dec]
p:129 [in Coq.Logic.EqdepFacts]
p:129 [in Coq.Structures.OrderedType]
P:129 [in Coq.Init.Logic]
p:13 [in Coq.Arith.Le]
P:13 [in Coq.Logic.Classical_Pred_Type]
p:13 [in Coq.PArith.BinPos]
p:13 [in Coq.Numbers.NatInt.NZAddOrder]
p:13 [in Coq.Sets.Finite_sets]
P:13 [in Coq.Init.Specif]
p:13 [in Coq.setoid_ring.Field_theory]
p:13 [in Coq.micromega.Env]
p:13 [in Coq.Numbers.NatInt.NZGcd]
p:13 [in Coq.Bool.Bvector]
p:13 [in Coq.Numbers.Natural.Abstract.NMulOrder]
P:13 [in Coq.Logic.Classical_Prop]
P:13 [in Coq.Classes.DecidableClass]
P:13 [in Coq.ZArith.Zcomplements]
p:13 [in Coq.QArith.Qreduction]
P:13 [in Coq.Logic.WeakFan]
p:130 [in Coq.PArith.BinPos]
P:130 [in Coq.ssr.ssreflect]
p:130 [in Coq.micromega.OrderedRing]
p:130 [in Coq.ZArith.Zorder]
P:130 [in Coq.MSets.MSetPositive]
p:130 [in Coq.Structures.GenericMinMax]
p:130 [in Coq.ZArith.Znat]
p:131 [in Coq.PArith.BinPos]
P:131 [in Coq.Logic.ChoiceFacts]
p:131 [in Coq.NArith.Ndigits]
P:131 [in Coq.setoid_ring.Ncring_polynom]
p:131 [in Coq.ZArith.Znumtheory]
P:132 [in Coq.Logic.EqdepFacts]
p:132 [in Coq.PArith.BinPos]
P:132 [in Coq.Init.Specif]
p:132 [in Coq.ZArith.Znat]
p:132 [in Coq.setoid_ring.Ncring]
P:133 [in Coq.Logic.Eqdep_dec]
p:133 [in Coq.Logic.EqdepFacts]
p:133 [in Coq.PArith.BinPos]
p:133 [in Coq.micromega.OrderedRing]
P:133 [in Coq.FSets.FSetPositive]
p:133 [in Coq.ZArith.Zorder]
P:133 [in Coq.MSets.MSetPositive]
p:133 [in Coq.Vectors.Fin]
p:133 [in Coq.Structures.GenericMinMax]
P:133 [in Coq.setoid_ring.Ncring_polynom]
P:133 [in Coq.Init.Logic]
p:133 [in Coq.PArith.BinPosDef]
p:133 [in Coq.setoid_ring.Ncring]
p:134 [in Coq.Logic.Eqdep_dec]
P:134 [in Coq.omega.OmegaLemmas]
P:135 [in Coq.Logic.EqdepFacts]
p:135 [in Coq.PArith.BinPos]
P:135 [in Coq.micromega.EnvRing]
p:135 [in Coq.btauto.Algebra]
p:135 [in Coq.setoid_ring.Ncring]
p:136 [in Coq.Logic.EqdepFacts]
P:136 [in Coq.Init.Specif]
P:136 [in Coq.FSets.FSetPositive]
p:136 [in Coq.ZArith.Zorder]
p:136 [in Coq.Vectors.Fin]
p:136 [in Coq.FSets.FMapPositive]
p:136 [in Coq.Structures.GenericMinMax]
P:136 [in Coq.setoid_ring.Ncring_polynom]
p:136 [in Coq.ZArith.Znumtheory]
P:137 [in Coq.Logic.EqdepFacts]
p:137 [in Coq.PArith.BinPos]
p:137 [in Coq.btauto.Algebra]
P:137 [in Coq.FSets.FSetInterface]
p:137 [in Coq.micromega.OrderedRing]
P:137 [in Coq.Init.Logic]
p:138 [in Coq.Vectors.Fin]
p:138 [in Coq.FSets.FMapPositive]
p:138 [in Coq.PArith.BinPosDef]
p:138 [in Coq.ZArith.Znumtheory]
p:139 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
p:139 [in Coq.PArith.BinPos]
P:139 [in Coq.setoid_ring.Ring_polynom]
p:139 [in Coq.ZArith.Zorder]
p:139 [in Coq.Structures.GenericMinMax]
p:14 [in Coq.setoid_ring.Ncring_initial]
p:14 [in Coq.Strings.OctalString]
p:14 [in Coq.Reals.Rminmax]
p:14 [in Coq.Logic.EqdepFacts]
p:14 [in Coq.PArith.BinPos]
p:14 [in Coq.Strings.HexString]
p:14 [in Coq.Floats.FloatLemmas]
p:14 [in Coq.ZArith.Zpow_facts]
p:14 [in Coq.PArith.Pnat]
P:14 [in Coq.ZArith.Wf_Z]
p:14 [in Coq.setoid_ring.InitialRing]
P:14 [in Coq.FSets.FSetInterface]
p:14 [in Coq.Arith.Plus]
p:14 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
P:14 [in Coq.Init.Logic_Type]
P:14 [in Coq.Arith.EqNat]
p:14 [in Coq.Strings.BinaryString]
p:14 [in Coq.Numbers.Natural.Abstract.NMaxMin]
p:14 [in Coq.Vectors.Fin]
p:14 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
p:14 [in Coq.Logic.ProofIrrelevanceFacts]
P:14 [in Coq.Reals.Ratan]
P:14 [in Coq.Logic.ClassicalDescription]
p:14 [in Coq.Numbers.NatInt.NZMul]
P:14 [in Coq.Logic.WKL]
P:14 [in Coq.Logic.StrictProp]
P:140 [in Coq.Logic.EqdepFacts]
p:140 [in Coq.btauto.Algebra]
p:140 [in Coq.Init.Specif]
P:140 [in Coq.FSets.FSetInterface]
P:140 [in Coq.omega.OmegaLemmas]
p:140 [in Coq.FSets.FMapPositive]
p:141 [in Coq.QArith.Qcanon]
p:141 [in Coq.Logic.EqdepFacts]
p:141 [in Coq.micromega.OrderedRing]
p:142 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
p:142 [in Coq.Logic.Eqdep_dec]
p:142 [in Coq.PArith.BinPos]
p:142 [in Coq.ZArith.Zorder]
p:142 [in Coq.Vectors.Fin]
p:142 [in Coq.Structures.GenericMinMax]
p:142 [in Coq.ZArith.Znumtheory]
p:142 [in Coq.QArith.QArith_base]
p:143 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
P:143 [in Coq.Init.Specif]
p:143 [in Coq.PArith.BinPosDef]
p:144 [in Coq.Reals.Cauchy_prod]
P:144 [in Coq.Logic.Eqdep_dec]
P:144 [in Coq.Reals.Rfunctions]
p:144 [in Coq.PArith.BinPosDef]
p:1440 [in Coq.FSets.FMapAVL]
p:145 [in Coq.Logic.Eqdep_dec]
P:145 [in Coq.Logic.EqdepFacts]
p:145 [in Coq.PArith.BinPos]
p:145 [in Coq.ZArith.BinInt]
p:145 [in Coq.NArith.BinNat]
p:145 [in Coq.micromega.OrderedRing]
p:145 [in Coq.ZArith.Zorder]
p:145 [in Coq.Structures.GenericMinMax]
p:145 [in Coq.PArith.BinPosDef]
P:146 [in Coq.Logic.Eqdep_dec]
p:146 [in Coq.Logic.EqdepFacts]
P:146 [in Coq.Arith.Wf_nat]
P:146 [in Coq.omega.OmegaLemmas]
p:146 [in Coq.ZArith.Znumtheory]
p:147 [in Coq.Reals.Cauchy_prod]
p:147 [in Coq.ZArith.BinInt]
p:147 [in Coq.Init.Specif]
p:147 [in Coq.NArith.BinNat]
p:147 [in Coq.Vectors.Fin]
p:148 [in Coq.Logic.Eqdep_dec]
p:148 [in Coq.PArith.BinPos]
p:148 [in Coq.ZArith.Zorder]
p:148 [in Coq.Structures.GenericMinMax]
p:148 [in Coq.PArith.BinPosDef]
p:148 [in Coq.ZArith.Znumtheory]
p:149 [in Coq.Logic.EqdepFacts]
P:149 [in Coq.Arith.Wf_nat]
P:149 [in Coq.Init.Specif]
p:149 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
p:15 [in Coq.PArith.BinPos]
p:15 [in Coq.Numbers.HexadecimalPos]
P:15 [in Coq.Logic.Epsilon]
P:15 [in Coq.Init.Wf]
P:15 [in Coq.Logic.Berardi]
p:15 [in Coq.setoid_ring.Ring_theory]
P:15 [in Coq.Logic.Classical_Prop]
p:15 [in Coq.Numbers.DecimalPos]
p:15 [in Coq.Numbers.NatInt.NZMulOrder]
p:15 [in Coq.Arith.Mult]
p:15 [in Coq.Numbers.Natural.Abstract.NGcd]
p:15 [in Coq.Numbers.NatInt.NZAdd]
p:15 [in Coq.Numbers.Integer.Abstract.ZMul]
p:150 [in Coq.Reals.Cauchy_prod]
P:150 [in Coq.Logic.Eqdep_dec]
P:150 [in Coq.Logic.EqdepFacts]
p:150 [in Coq.PArith.BinPos]
p:150 [in Coq.btauto.Algebra]
p:151 [in Coq.Logic.Eqdep_dec]
p:151 [in Coq.ZArith.Zorder]
p:151 [in Coq.Structures.GenericMinMax]
p:151 [in Coq.PArith.BinPosDef]
p:151 [in Coq.ZArith.Znumtheory]
p:152 [in Coq.PArith.BinPos]
P:152 [in Coq.omega.OmegaLemmas]
p:152 [in Coq.Vectors.Fin]
p:152 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
p:152 [in Coq.ZArith.Znumtheory]
p:153 [in Coq.Reals.Cauchy_prod]
P:153 [in Coq.Logic.EqdepFacts]
p:153 [in Coq.btauto.Algebra]
p:153 [in Coq.Numbers.Cyclic.Int31.Int31]
p:153 [in Coq.Vectors.VectorDef]
p:154 [in Coq.Logic.EqdepFacts]
p:154 [in Coq.Init.Specif]
p:154 [in Coq.ZArith.Zorder]
p:154 [in Coq.Structures.GenericMinMax]
p:154 [in Coq.setoid_ring.Ncring_polynom]
P:155 [in Coq.Logic.Eqdep_dec]
p:155 [in Coq.PArith.BinPos]
P:155 [in Coq.omega.OmegaLemmas]
p:155 [in Coq.ZArith.Znumtheory]
p:156 [in Coq.Reals.Cauchy_prod]
p:156 [in Coq.Logic.Eqdep_dec]
P:156 [in Coq.ssr.ssrfun]
p:156 [in Coq.Vectors.Fin]
p:156 [in Coq.ZArith.Znumtheory]
p:157 [in Coq.Reals.Cauchy_prod]
p:157 [in Coq.PArith.BinPos]
p:157 [in Coq.btauto.Algebra]
P:157 [in Coq.Init.Specif]
p:157 [in Coq.ZArith.Zorder]
p:157 [in Coq.Structures.GenericMinMax]
p:158 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:158 [in Coq.Reals.Cauchy_prod]
P:158 [in Coq.ssr.ssrbool]
P:158 [in Coq.omega.OmegaLemmas]
P:158 [in Coq.setoid_ring.Ncring_polynom]
p:159 [in Coq.Reals.Cauchy_prod]
p:159 [in Coq.btauto.Algebra]
P:159 [in Coq.ssr.ssrfun]
p:159 [in Coq.setoid_ring.Ncring_polynom]
p:159 [in Coq.ZArith.Znumtheory]
P:16 [in Coq.Logic.Classical_Pred_Type]
P:16 [in Coq.FSets.FSetDecide]
p:16 [in Coq.PArith.BinPos]
p:16 [in Coq.Numbers.NatInt.NZAddOrder]
p:16 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p:16 [in Coq.PArith.Pnat]
P:16 [in Coq.MSets.MSetDecide]
p:16 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
p:16 [in Coq.setoid_ring.Ring_theory]
p:160 [in Coq.PArith.BinPos]
p:160 [in Coq.Numbers.Cyclic.Int63.Int63]
p:160 [in Coq.ZArith.Zorder]
p:160 [in Coq.Structures.GenericMinMax]
p:160 [in Coq.PArith.BinPosDef]
p:161 [in Coq.btauto.Algebra]
p:161 [in Coq.Init.Specif]
p:161 [in Coq.Numbers.Cyclic.Int31.Int31]
p:161 [in Coq.FSets.FMapPositive]
P:161 [in Coq.Logic.ClassicalFacts]
p:161 [in Coq.ZArith.Znumtheory]
P:162 [in Coq.Reals.MVT]
P:162 [in Coq.omega.OmegaLemmas]
p:162 [in Coq.Vectors.Fin]
P:162 [in Coq.setoid_ring.Ncring_polynom]
p:163 [in Coq.PArith.BinPos]
P:163 [in Coq.micromega.RingMicromega]
p:163 [in Coq.ZArith.Zorder]
p:163 [in Coq.Structures.GenericMinMax]
P:163 [in Coq.FSets.FSetCompat]
P:164 [in Coq.Init.Specif]
p:164 [in Coq.Vectors.VectorDef]
P:165 [in Coq.ssr.ssrfun]
p:165 [in Coq.Vectors.Fin]
P:166 [in Coq.micromega.ZifyClasses]
p:166 [in Coq.PArith.BinPos]
P:166 [in Coq.omega.OmegaLemmas]
p:166 [in Coq.ZArith.Zorder]
p:166 [in Coq.FSets.FMapPositive]
p:166 [in Coq.QArith.QArith_base]
P:166 [in Coq.FSets.FSetCompat]
p:167 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
P:167 [in Coq.micromega.RingMicromega]
p:167 [in Coq.NArith.Ndigits]
p:167 [in Coq.PArith.BinPosDef]
p:167 [in Coq.Vectors.VectorDef]
P:168 [in Coq.micromega.ZifyClasses]
p:168 [in Coq.Logic.EqdepFacts]
p:168 [in Coq.ZArith.Znumtheory]
p:169 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:169 [in Coq.PArith.BinPos]
p:169 [in Coq.Init.Specif]
P:17 [in Coq.Reals.Abstract.ConstructiveLUB]
p:17 [in Coq.Reals.Rminmax]
p:17 [in Coq.PArith.BinPos]
p:17 [in Coq.Numbers.Integer.Abstract.ZGcd]
p:17 [in Coq.Arith.Plus]
p:17 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
p:17 [in Coq.Numbers.NatInt.NZDomain]
p:17 [in Coq.Numbers.Natural.Abstract.NMaxMin]
p:17 [in Coq.Numbers.Natural.Abstract.NMulOrder]
P:17 [in Coq.Vectors.Fin]
P:17 [in Coq.Logic.ProofIrrelevanceFacts]
P:17 [in Coq.Logic.HLevels]
P:17 [in Coq.Logic.ClassicalDescription]
P:17 [in Coq.Logic.Classical_Prop]
p:17 [in Coq.ZArith.Znat]
P:17 [in Coq.Logic.WKL]
p:17 [in Coq.QArith.Qreduction]
p:17 [in Coq.NArith.Ndec]
P:17 [in Coq.Logic.StrictProp]
P:17 [in Coq.Logic.WeakFan]
P:170 [in Coq.Logic.EqdepFacts]
P:170 [in Coq.omega.OmegaLemmas]
p:170 [in Coq.ZArith.Zorder]
p:170 [in Coq.NArith.Ndigits]
p:171 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:171 [in Coq.PArith.BinPos]
p:171 [in Coq.FSets.FMapPositive]
p:171 [in Coq.Structures.GenericMinMax]
p:171 [in Coq.setoid_ring.Ncring_polynom]
p:172 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:172 [in Coq.Reals.Cauchy_prod]
p:172 [in Coq.ZArith.BinInt]
p:172 [in Coq.NArith.Ndigits]
p:172 [in Coq.Vectors.Fin]
p:172 [in Coq.setoid_ring.Ncring_polynom]
P:173 [in Coq.Logic.EqdepFacts]
p:173 [in Coq.PArith.BinPos]
P:173 [in Coq.Init.Specif]
P:173 [in Coq.ssr.ssrfun]
p:174 [in Coq.Logic.EqdepFacts]
p:174 [in Coq.PArith.BinPos]
p:174 [in Coq.omega.OmegaLemmas]
p:174 [in Coq.ZArith.Zorder]
p:174 [in Coq.Structures.GenericMinMax]
p:175 [in Coq.Reals.Cauchy_prod]
P:175 [in Coq.Logic.EqdepFacts]
p:175 [in Coq.micromega.RingMicromega]
p:175 [in Coq.ZArith.BinInt]
P:175 [in Coq.Logic.ChoiceFacts]
P:175 [in Coq.omega.OmegaLemmas]
p:175 [in Coq.Vectors.Fin]
P:175 [in Coq.setoid_ring.Ncring_polynom]
p:176 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:176 [in Coq.setoid_ring.Ncring_polynom]
P:176 [in Coq.Logic.ClassicalFacts]
p:177 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:177 [in Coq.ZArith.BinInt]
p:177 [in Coq.ZArith.Zorder]
p:177 [in Coq.Structures.GenericMinMax]
P:177 [in Coq.setoid_ring.Ncring_polynom]
p:178 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:179 [in Coq.Logic.EqdepFacts]
p:179 [in Coq.omega.OmegaLemmas]
P:179 [in Coq.Logic.ClassicalFacts]
p:18 [in Coq.Numbers.Natural.Abstract.NSub]
P:18 [in Coq.FSets.FSetDecide]
p:18 [in Coq.PArith.BinPos]
p:18 [in Coq.Numbers.HexadecimalPos]
p:18 [in Coq.ZArith.BinInt]
p:18 [in Coq.Sets.Finite_sets]
p:18 [in Coq.PArith.Pnat]
p:18 [in Coq.btauto.Algebra]
P:18 [in Coq.MSets.MSetDecide]
P:18 [in Coq.Init.Specif]
P:18 [in Coq.Init.Logic_Type]
p:18 [in Coq.Bool.Bvector]
p:18 [in Coq.Numbers.Natural.Abstract.NOrder]
p:18 [in Coq.ZArith.Zpow_alt]
P:18 [in Coq.Reals.Ratan]
p:18 [in Coq.Numbers.DecimalPos]
p:18 [in Coq.Arith.Mult]
p:18 [in Coq.Numbers.Natural.Abstract.NGcd]
p:18 [in Coq.Numbers.NatInt.NZAdd]
p:18 [in Coq.Numbers.Integer.Abstract.ZMul]
p:18 [in Coq.ZArith.Zcompare]
P:180 [in Coq.Logic.EqdepFacts]
p:180 [in Coq.PArith.BinPos]
P:180 [in Coq.Logic.ChoiceFacts]
P:180 [in Coq.omega.OmegaLemmas]
p:180 [in Coq.ZArith.Zorder]
p:180 [in Coq.Structures.GenericMinMax]
P:180 [in Coq.Init.Logic]
P:181 [in Coq.Logic.ClassicalFacts]
p:182 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:182 [in Coq.Init.Specif]
p:182 [in Coq.setoid_ring.Ncring_polynom]
p:182 [in Coq.Reals.PSeries_reg]
p:183 [in Coq.PArith.BinPos]
P:183 [in Coq.Logic.ChoiceFacts]
P:183 [in Coq.omega.OmegaLemmas]
p:183 [in Coq.ZArith.Zorder]
p:183 [in Coq.Structures.GenericMinMax]
P:183 [in Coq.Logic.ClassicalFacts]
p:183 [in Coq.Vectors.VectorDef]
p:184 [in Coq.MSets.MSetProperties]
p:184 [in Coq.FSets.FSetProperties]
P:185 [in Coq.setoid_ring.Ncring_polynom]
p:185 [in Coq.Reals.PSeries_reg]
P:185 [in Coq.Logic.ClassicalFacts]
P:186 [in Coq.Logic.ChoiceFacts]
P:186 [in Coq.Init.Specif]
p:186 [in Coq.ZArith.Zorder]
P:186 [in Coq.Init.Logic]
p:186 [in Coq.ZArith.Znumtheory]
p:187 [in Coq.PArith.BinPos]
P:187 [in Coq.omega.OmegaLemmas]
P:187 [in Coq.setoid_ring.Ncring_polynom]
p:187 [in Coq.micromega.ZMicromega]
P:188 [in Coq.Reals.MVT]
P:188 [in Coq.setoid_ring.Ncring_polynom]
p:188 [in Coq.Reals.PSeries_reg]
p:189 [in Coq.ZArith.BinInt]
P:189 [in Coq.micromega.EnvRing]
p:189 [in Coq.FSets.FMapFullAVL]
p:189 [in Coq.ZArith.Zorder]
P:19 [in Coq.Logic.Classical_Pred_Type]
p:19 [in Coq.Arith.Div2]
p:19 [in Coq.Strings.OctalString]
p:19 [in Coq.PArith.BinPos]
p:19 [in Coq.Strings.HexString]
p:19 [in Coq.Numbers.NatInt.NZAddOrder]
P:19 [in Coq.Logic.Epsilon]
p:19 [in Coq.Reals.Binomial]
P:19 [in Coq.Arith.Wf_nat]
P:19 [in Coq.ZArith.Wf_Z]
P:19 [in Coq.Init.Wf]
p:19 [in Coq.setoid_ring.Field_theory]
p:19 [in Coq.NArith.BinNat]
P:19 [in Coq.Logic.ClassicalUniqueChoice]
p:19 [in Coq.Strings.BinaryString]
p:19 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
P:19 [in Coq.Logic.Classical_Prop]
p:19 [in Coq.Numbers.NatInt.NZMul]
p:19 [in Coq.QArith.Qreduction]
P:190 [in Coq.Reals.MVT]
P:190 [in Coq.Logic.ChoiceFacts]
p:190 [in Coq.ZArith.Znumtheory]
p:190 [in Coq.Vectors.VectorDef]
p:191 [in Coq.Vectors.VectorSpec]
p:191 [in Coq.PArith.BinPos]
P:191 [in Coq.omega.OmegaLemmas]
p:191 [in Coq.Reals.PSeries_reg]
p:191 [in Coq.ZArith.Znumtheory]
p:192 [in Coq.ZArith.BinInt]
p:192 [in Coq.ZArith.Zorder]
p:192 [in Coq.Structures.OrderedType]
P:192 [in Coq.Structures.GenericMinMax]
p:193 [in Coq.Init.Specif]
P:194 [in Coq.Logic.Hurkens]
p:194 [in Coq.setoid_ring.Ncring_polynom]
p:194 [in Coq.micromega.ZMicromega]
p:195 [in Coq.PArith.BinPos]
P:196 [in Coq.setoid_ring.Ring_polynom]
P:196 [in Coq.micromega.EnvRing]
P:196 [in Coq.omega.OmegaLemmas]
p:196 [in Coq.ZArith.Zorder]
p:197 [in Coq.FSets.FMapFacts]
P:197 [in Coq.Logic.Hurkens]
P:197 [in Coq.Structures.GenericMinMax]
p:198 [in Coq.FSets.FMapFacts]
P:198 [in Coq.Init.Specif]
P:198 [in Coq.Logic.Hurkens]
p:198 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
P:199 [in Coq.MSets.MSetInterface]
P:199 [in Coq.setoid_ring.Ring_polynom]
p:199 [in Coq.FSets.FMapFacts]
P:199 [in Coq.micromega.EnvRing]
P:2 [in Coq.Logic.Decidable]
P:2 [in Coq.Logic.Classical_Pred_Type]
p:2 [in Coq.Strings.OctalString]
p:2 [in Coq.Strings.HexString]
P:2 [in Coq.Logic.Epsilon]
p:2 [in Coq.Reals.Binomial]
P:2 [in Coq.Logic.ClassicalEpsilon]
p:2 [in Coq.ZArith.Zpow_facts]
p:2 [in Coq.PArith.Pnat]
P:2 [in Coq.Init.Specif]
P:2 [in Coq.Program.Subset]
p:2 [in Coq.QArith.Qreals]
p:2 [in Coq.Structures.DecidableType]
P:2 [in Coq.Logic.ClassicalChoice]
P:2 [in Coq.Logic.IndefiniteDescription]
p:2 [in Coq.Strings.BinaryString]
p:2 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
P:2 [in Coq.ZArith.ZArith_dec]
p:2 [in Coq.Logic.HLevels]
p:2 [in Coq.Logic.Eqdep]
P:2 [in Coq.Logic.Description]
p:20 [in Coq.setoid_ring.BinList]
P:20 [in Coq.Numbers.Integer.Abstract.ZSgnAbs]
p:20 [in Coq.Reals.Rminmax]
P:20 [in Coq.FSets.FSetDecide]
p:20 [in Coq.Logic.EqdepFacts]
p:20 [in Coq.PArith.BinPos]
p:20 [in Coq.ZArith.BinInt]
p:20 [in Coq.Numbers.Integer.Abstract.ZGcd]
p:20 [in Coq.Reals.Binomial]
P:20 [in Coq.Reals.MVT]
p:20 [in Coq.PArith.Pnat]
P:20 [in Coq.MSets.MSetDecide]
P:20 [in Coq.Init.Wf]
p:20 [in Coq.Arith.Plus]
p:20 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
P:20 [in Coq.NArith.BinNat]
p:20 [in Coq.Numbers.Natural.Abstract.NMaxMin]
P:20 [in Coq.Vectors.Fin]
p:20 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
p:20 [in Coq.Logic.ProofIrrelevanceFacts]
p:20 [in Coq.Numbers.NatInt.NZOrder]
P:20 [in Coq.Logic.HLevels]
P:20 [in Coq.ZArith.Zcomplements]
P:20 [in Coq.Logic.WKL]
P:20 [in Coq.Logic.WeakFan]
p:200 [in Coq.FSets.FMapFacts]
P:200 [in Coq.Logic.Hurkens]
P:200 [in Coq.omega.OmegaLemmas]
p:200 [in Coq.PArith.BinPosDef]
P:201 [in Coq.Logic.EqdepFacts]
p:201 [in Coq.FSets.FMapFacts]
p:201 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
p:202 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
P:202 [in Coq.MSets.MSetInterface]
p:202 [in Coq.Logic.EqdepFacts]
p:202 [in Coq.FSets.FMapFacts]
p:202 [in Coq.Reals.PSeries_reg]
p:202 [in Coq.ZArith.Znat]
p:202 [in Coq.micromega.ZMicromega]
p:203 [in Coq.Vectors.VectorSpec]
P:203 [in Coq.PArith.BinPos]
p:203 [in Coq.Init.Specif]
P:203 [in Coq.omega.OmegaLemmas]
p:203 [in Coq.ZArith.Znat]
p:203 [in Coq.PArith.BinPosDef]
p:204 [in Coq.PArith.BinPos]
p:204 [in Coq.micromega.EnvRing]
P:204 [in Coq.Structures.GenericMinMax]
p:204 [in Coq.PArith.BinPosDef]
p:204 [in Coq.micromega.ZMicromega]
P:205 [in Coq.Logic.EqdepFacts]
p:205 [in Coq.PArith.BinPos]
p:205 [in Coq.Reals.PSeries_reg]
p:206 [in Coq.Logic.EqdepFacts]
p:207 [in Coq.PArith.BinPos]
p:207 [in Coq.Reals.PSeries_reg]
p:207 [in Coq.PArith.BinPosDef]
P:208 [in Coq.Logic.EqdepFacts]
P:208 [in Coq.micromega.EnvRing]
P:208 [in Coq.FSets.FSetInterface]
p:208 [in Coq.PArith.BinPosDef]
p:208 [in Coq.micromega.ZMicromega]
p:209 [in Coq.Logic.EqdepFacts]
P:209 [in Coq.setoid_ring.Ring_polynom]
P:209 [in Coq.Structures.GenericMinMax]
p:209 [in Coq.Reals.PSeries_reg]
p:21 [in Coq.Numbers.Natural.Abstract.NSub]
p:21 [in Coq.Arith.Div2]
p:21 [in Coq.PArith.BinPos]
p:21 [in Coq.Reals.Binomial]
P:21 [in Coq.Reals.Rsqrt_def]
P:21 [in Coq.Init.Wf]
p:21 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
p:21 [in Coq.Numbers.HexadecimalQ]
P:21 [in Coq.Logic.Classical_Prop]
p:21 [in Coq.Numbers.NatInt.NZAdd]
p:21 [in Coq.Reals.Abstract.ConstructiveMinMax]
p:21 [in Coq.QArith.Qreduction]
P:21 [in Coq.Logic.StrictProp]
p:21 [in Coq.rtauto.Rtauto]
P:210 [in Coq.Init.Specif]
p:210 [in Coq.PArith.BinPosDef]
p:210 [in Coq.micromega.ZMicromega]
P:211 [in Coq.setoid_ring.Ring_polynom]
p:211 [in Coq.micromega.ZMicromega]
P:212 [in Coq.Logic.EqdepFacts]
P:212 [in Coq.micromega.EnvRing]
p:213 [in Coq.Logic.EqdepFacts]
p:213 [in Coq.PArith.BinPos]
p:213 [in Coq.micromega.EnvRing]
p:214 [in Coq.PArith.BinPos]
p:214 [in Coq.Init.Specif]
p:214 [in Coq.micromega.ZMicromega]
P:215 [in Coq.micromega.EnvRing]
P:215 [in Coq.FSets.FSetInterface]
p:216 [in Coq.Logic.EqdepFacts]
p:216 [in Coq.PArith.BinPos]
p:216 [in Coq.micromega.EnvRing]
p:216 [in Coq.ZArith.Zorder]
p:217 [in Coq.PArith.BinPos]
P:217 [in Coq.setoid_ring.Ring_polynom]
P:217 [in Coq.Init.Specif]
p:218 [in Coq.NArith.BinNat]
p:218 [in Coq.micromega.ZMicromega]
p:219 [in Coq.PArith.BinPos]
p:219 [in Coq.Init.Specif]
p:22 [in Coq.setoid_ring.BinList]
P:22 [in Coq.Numbers.Integer.Abstract.ZSgnAbs]
p:22 [in Coq.Numbers.Integer.Abstract.ZAdd]
P:22 [in Coq.FSets.FSetDecide]
p:22 [in Coq.PArith.BinPos]
p:22 [in Coq.ZArith.BinInt]
p:22 [in Coq.Reals.Binomial]
P:22 [in Coq.Reals.MVT]
p:22 [in Coq.PArith.Pnat]
p:22 [in Coq.Numbers.Natural.Abstract.NDefOps]
P:22 [in Coq.ZArith.Wf_Z]
P:22 [in Coq.MSets.MSetDecide]
p:22 [in Coq.setoid_ring.Field_theory]
p:22 [in Coq.Structures.DecidableType]
p:22 [in Coq.Strings.Ascii]
P:22 [in Coq.Logic.HLevels]
p:22 [in Coq.Numbers.HexadecimalQ]
p:22 [in Coq.Numbers.NatInt.NZMul]
p:22 [in Coq.Numbers.NatInt.NZMulOrder]
p:22 [in Coq.Arith.Mult]
p:22 [in Coq.ZArith.Zcompare]
p:220 [in Coq.ZArith.BinInt]
P:220 [in Coq.micromega.EnvRing]
P:220 [in Coq.FSets.FSetInterface]
P:220 [in Coq.Logic.ClassicalFacts]
p:221 [in Coq.PArith.BinPos]
p:221 [in Coq.ZArith.BinInt]
p:221 [in Coq.micromega.ZMicromega]
p:222 [in Coq.Logic.EqdepFacts]
p:222 [in Coq.ZArith.BinInt]
p:223 [in Coq.ZArith.BinInt]
p:223 [in Coq.micromega.ZMicromega]
P:224 [in Coq.setoid_ring.Ring_polynom]
p:224 [in Coq.setoid_ring.Field_theory]
p:224 [in Coq.NArith.BinNat]
p:225 [in Coq.Init.Specif]
P:225 [in Coq.FSets.FSetInterface]
p:225 [in Coq.QArith.QArith_base]
p:226 [in Coq.Logic.EqdepFacts]
p:226 [in Coq.micromega.ZMicromega]
p:226 [in Coq.QArith.QArith_base]
p:227 [in Coq.PArith.BinPos]
P:227 [in Coq.micromega.EnvRing]
P:227 [in Coq.Numbers.Cyclic.Int63.Int63]
P:227 [in Coq.Init.Specif]
P:227 [in Coq.Logic.ClassicalFacts]
P:228 [in Coq.setoid_ring.Ring_polynom]
P:228 [in Coq.Structures.GenericMinMax]
p:228 [in Coq.QArith.QArith_base]
p:229 [in Coq.PArith.BinPos]
P:229 [in Coq.Numbers.Cyclic.Int63.Int63]
P:229 [in Coq.Logic.Hurkens]
p:23 [in Coq.QArith.Qcanon]
p:23 [in Coq.Numbers.NatInt.NZAddOrder]
p:23 [in Coq.ZArith.BinInt]
P:23 [in Coq.Arith.Wf_nat]
p:23 [in Coq.Arith.Plus]
p:23 [in Coq.ssr.ssreflect]
P:23 [in Coq.Sorting.Sorted]
p:23 [in Coq.Numbers.Natural.Abstract.NMaxMin]
p:23 [in Coq.Bool.Bvector]
p:23 [in Coq.Numbers.NatInt.NZOrder]
P:23 [in Coq.Logic.Classical_Prop]
p:23 [in Coq.Numbers.Natural.Abstract.NGcd]
P:23 [in Coq.Vectors.VectorDef]
P:23 [in Coq.Logic.WeakFan]
P:230 [in Coq.Vectors.VectorSpec]
p:230 [in Coq.Logic.EqdepFacts]
p:230 [in Coq.NArith.BinNat]
p:230 [in Coq.micromega.ZMicromega]
p:230 [in Coq.QArith.QArith_base]
p:231 [in Coq.PArith.BinPos]
P:231 [in Coq.setoid_ring.Ring_polynom]
P:231 [in Coq.micromega.EnvRing]
p:231 [in Coq.Init.Specif]
P:231 [in Coq.Structures.GenericMinMax]
P:232 [in Coq.Logic.EqdepFacts]
p:232 [in Coq.PArith.BinPos]
p:233 [in Coq.Logic.EqdepFacts]
P:233 [in Coq.Numbers.Cyclic.Int63.Int63]
P:233 [in Coq.Init.Specif]
P:234 [in Coq.setoid_ring.Ring_polynom]
P:234 [in Coq.micromega.EnvRing]
p:235 [in Coq.PArith.BinPos]
P:235 [in Coq.Bool.Bool]
P:236 [in Coq.Vectors.VectorSpec]
p:236 [in Coq.NArith.BinNat]
P:236 [in Coq.Structures.GenericMinMax]
P:236 [in Coq.Logic.ClassicalFacts]
p:237 [in Coq.MSets.MSetInterface]
p:237 [in Coq.PArith.BinPos]
P:237 [in Coq.setoid_ring.Ring_polynom]
P:237 [in Coq.micromega.EnvRing]
p:238 [in Coq.Init.Specif]
P:238 [in Coq.Bool.Bool]
P:239 [in Coq.setoid_ring.Ring_polynom]
P:239 [in Coq.Structures.GenericMinMax]
P:239 [in Coq.Logic.ClassicalFacts]
p:239 [in Coq.micromega.ZMicromega]
p:24 [in Coq.micromega.Ztac]
p:24 [in Coq.Numbers.Natural.Abstract.NSub]
p:24 [in Coq.PArith.BinPos]
P:24 [in Coq.Logic.Epsilon]
p:24 [in Coq.PArith.Pnat]
P:24 [in Coq.Sorting.Permutation]
P:24 [in Coq.Vectors.Fin]
P:24 [in Coq.Logic.HLevels]
P:24 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
p:24 [in Coq.Numbers.NatInt.NZAdd]
p:240 [in Coq.PArith.BinPos]
P:240 [in Coq.micromega.EnvRing]
P:240 [in Coq.Logic.Hurkens]
P:240 [in Coq.Bool.Bool]
P:241 [in Coq.Vectors.VectorSpec]
p:241 [in Coq.Logic.EqdepFacts]
p:241 [in Coq.Init.Specif]
p:241 [in Coq.setoid_ring.Field_theory]
P:241 [in Coq.Logic.Hurkens]
p:241 [in Coq.micromega.ZMicromega]
p:242 [in Coq.PArith.BinPos]
P:242 [in Coq.setoid_ring.Ring_polynom]
P:242 [in Coq.micromega.EnvRing]
P:242 [in Coq.Logic.Hurkens]
P:242 [in Coq.Bool.Bool]
P:242 [in Coq.Logic.ClassicalFacts]
P:243 [in Coq.Logic.EqdepFacts]
P:243 [in Coq.Init.Specif]
p:243 [in Coq.micromega.ZMicromega]
p:244 [in Coq.Logic.EqdepFacts]
p:244 [in Coq.ssr.ssrbool]
p:245 [in Coq.PArith.BinPos]
P:245 [in Coq.setoid_ring.Ring_polynom]
P:245 [in Coq.micromega.EnvRing]
P:246 [in Coq.Logic.EqdepFacts]
P:247 [in Coq.Vectors.VectorSpec]
p:247 [in Coq.Logic.EqdepFacts]
p:247 [in Coq.PArith.BinPos]
P:248 [in Coq.setoid_ring.Ring_polynom]
P:248 [in Coq.micromega.EnvRing]
p:248 [in Coq.setoid_ring.Field_theory]
p:249 [in Coq.PArith.BinPos]
P:249 [in Coq.Init.Specif]
P:249 [in Coq.Logic.ClassicalFacts]
p:25 [in Coq.QArith.Qcanon]
P:25 [in Coq.FSets.FSetDecide]
p:25 [in Coq.PArith.BinPos]
p:25 [in Coq.ZArith.BinInt]
P:25 [in Coq.Logic.ClassicalEpsilon]
P:25 [in Coq.Logic.JMeq]
P:25 [in Coq.ZArith.Wf_Z]
P:25 [in Coq.Reals.Rsqrt_def]
P:25 [in Coq.MSets.MSetDecide]
P:25 [in Coq.Init.Wf]
p:25 [in Coq.ZArith.Int]
p:25 [in Coq.ZArith.auxiliary]
P:25 [in Coq.Init.Datatypes]
p:25 [in Coq.setoid_ring.Ring_theory]
P:25 [in Coq.Logic.Classical_Prop]
p:25 [in Coq.Arith.Mult]
p:25 [in Coq.QArith.Qpower]
P:25 [in Coq.Logic.WeakFan]
p:250 [in Coq.ssr.ssrbool]
p:250 [in Coq.ZArith.Znat]
p:250 [in Coq.micromega.ZMicromega]
P:251 [in Coq.setoid_ring.Ring_polynom]
P:251 [in Coq.micromega.EnvRing]
p:251 [in Coq.Reals.SeqProp]
P:252 [in Coq.Logic.EqdepFacts]
p:252 [in Coq.setoid_ring.Field_theory]
p:252 [in Coq.Reals.SeqProp]
p:252 [in Coq.micromega.ZMicromega]
P:253 [in Coq.setoid_ring.Ring_polynom]
P:253 [in Coq.Logic.Hurkens]
p:253 [in Coq.Reals.SeqProp]
p:254 [in Coq.Logic.EqdepFacts]
p:254 [in Coq.PArith.BinPos]
P:254 [in Coq.micromega.EnvRing]
P:254 [in Coq.Logic.Hurkens]
p:254 [in Coq.NArith.BinNat]
P:255 [in Coq.Init.Specif]
P:255 [in Coq.Sorting.Permutation]
P:256 [in Coq.setoid_ring.Ring_polynom]
p:256 [in Coq.Reals.SeqProp]
P:256 [in Coq.Vectors.VectorDef]
p:257 [in Coq.PArith.BinPos]
p:257 [in Coq.setoid_ring.Ring_polynom]
P:257 [in Coq.micromega.EnvRing]
p:257 [in Coq.Init.Specif]
p:257 [in Coq.NArith.BinNat]
p:258 [in Coq.Logic.EqdepFacts]
P:259 [in Coq.setoid_ring.Ring_polynom]
p:26 [in Coq.Reals.Cauchy_prod]
p:26 [in Coq.Reals.Runcountable]
p:26 [in Coq.Logic.ConstructiveEpsilon]
P:26 [in Coq.Logic.Eqdep_dec]
p:26 [in Coq.PArith.BinPos]
p:26 [in Coq.Floats.FloatLemmas]
p:26 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p:26 [in Coq.ZArith.Zpow_facts]
p:26 [in Coq.PArith.Pnat]
p:26 [in Coq.btauto.Algebra]
P:26 [in Coq.Init.Wf]
p:26 [in Coq.Arith.Plus]
p:26 [in Coq.micromega.Env]
p:26 [in Coq.Numbers.Natural.Abstract.NMaxMin]
p:26 [in Coq.Numbers.NatInt.NZMul]
P:26 [in Coq.Logic.Diaconescu]
P:26 [in Coq.Logic.StrictProp]
p:260 [in Coq.PArith.BinPos]
P:260 [in Coq.micromega.EnvRing]
p:260 [in Coq.NArith.BinNat]
P:261 [in Coq.Logic.EqdepFacts]
P:261 [in Coq.setoid_ring.Ring_polynom]
p:261 [in Coq.micromega.ZMicromega]
p:262 [in Coq.Logic.EqdepFacts]
p:262 [in Coq.PArith.BinPos]
P:263 [in Coq.micromega.EnvRing]
p:263 [in Coq.Init.Specif]
p:264 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:264 [in Coq.PArith.BinPos]
P:264 [in Coq.MSets.MSetProperties]
p:264 [in Coq.micromega.EnvRing]
P:264 [in Coq.FSets.FSetProperties]
p:265 [in Coq.Logic.ChoiceFacts]
p:265 [in Coq.ssr.ssrbool]
p:265 [in Coq.micromega.ZMicromega]
P:265 [in Coq.Vectors.VectorDef]
p:266 [in Coq.PArith.BinPos]
P:266 [in Coq.micromega.EnvRing]
P:267 [in Coq.Logic.EqdepFacts]
p:268 [in Coq.PArith.BinPos]
P:268 [in Coq.micromega.EnvRing]
p:269 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:269 [in Coq.Logic.EqdepFacts]
p:269 [in Coq.Init.Specif]
p:27 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:27 [in Coq.QArith.Qcanon]
p:27 [in Coq.Numbers.Natural.Abstract.NSub]
p:27 [in Coq.Logic.Eqdep_dec]
p:27 [in Coq.Reals.Rminmax]
p:27 [in Coq.Logic.EqdepFacts]
p:27 [in Coq.PArith.BinPos]
p:27 [in Coq.Numbers.NatInt.NZAddOrder]
p:27 [in Coq.ZArith.BinInt]
P:27 [in Coq.Logic.Epsilon]
p:27 [in Coq.ZArith.Zpow_facts]
P:27 [in Coq.Arith.Wf_nat]
p:27 [in Coq.Reals.Rtrigo_alt]
p:27 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
p:27 [in Coq.NArith.BinNat]
p:27 [in Coq.Numbers.NatInt.NZDomain]
P:27 [in Coq.Init.Datatypes]
p:27 [in Coq.Arith.Between]
p:27 [in Coq.Numbers.NatInt.NZMulOrder]
P:27 [in Coq.Logic.WKL]
p:27 [in Coq.Reals.Abstract.ConstructiveSum]
p:27 [in Coq.Reals.Cos_plus]
p:270 [in Coq.PArith.BinPos]
P:270 [in Coq.MSets.MSetProperties]
p:270 [in Coq.micromega.ZMicromega]
P:270 [in Coq.FSets.FSetProperties]
p:271 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:271 [in Coq.ZArith.BinInt]
P:271 [in Coq.micromega.EnvRing]
p:271 [in Coq.FSets.FMapPositive]
p:272 [in Coq.PArith.BinPos]
p:272 [in Coq.micromega.ZMicromega]
p:273 [in Coq.Logic.EqdepFacts]
P:273 [in Coq.setoid_ring.Ring_polynom]
P:273 [in Coq.Init.Specif]
P:273 [in Coq.Logic.Hurkens]
p:273 [in Coq.FSets.FMapPositive]
p:274 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:274 [in Coq.PArith.BinPos]
p:274 [in Coq.ZArith.BinInt]
p:275 [in Coq.FSets.FMapFacts]
p:275 [in Coq.ssr.ssrbool]
p:275 [in Coq.FSets.FMapPositive]
p:276 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:276 [in Coq.PArith.BinPos]
p:276 [in Coq.Init.Specif]
p:278 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:278 [in Coq.PArith.BinPos]
P:278 [in Coq.setoid_ring.Ring_polynom]
p:278 [in Coq.micromega.EnvRing]
p:279 [in Coq.ZArith.BinInt]
p:28 [in Coq.Reals.Cauchy_prod]
P:28 [in Coq.Logic.Eqdep_dec]
P:28 [in Coq.Logic.ClassicalEpsilon]
p:28 [in Coq.PArith.Pnat]
P:28 [in Coq.Bool.Bool]
p:28 [in Coq.ZArith.auxiliary]
P:28 [in Coq.Logic.ClassicalUniqueChoice]
p:28 [in Coq.Vectors.Fin]
P:28 [in Coq.Logic.Classical_Prop]
p:28 [in Coq.Arith.Gt]
p:28 [in Coq.Arith.Mult]
P:28 [in Coq.Reals.Rlogic]
p:28 [in Coq.Numbers.NatInt.NZAdd]
p:28 [in Coq.Reals.ClassicalDedekindReals]
p:280 [in Coq.PArith.BinPos]
P:280 [in Coq.Init.Logic]
p:281 [in Coq.micromega.EnvRing]
p:281 [in Coq.Init.Specif]
p:281 [in Coq.NArith.BinNat]
p:282 [in Coq.PArith.BinPos]
p:282 [in Coq.FSets.FMapWeakList]
P:283 [in Coq.Init.Specif]
p:283 [in Coq.Lists.SetoidList]
p:284 [in Coq.PArith.BinPos]
p:284 [in Coq.FSets.FMapPositive]
p:285 [in Coq.Reals.Rtopology]
p:286 [in Coq.PArith.BinPos]
p:286 [in Coq.micromega.RingMicromega]
p:286 [in Coq.Lists.SetoidList]
p:287 [in Coq.FSets.FSetBridge]
p:287 [in Coq.Init.Specif]
p:287 [in Coq.micromega.ZMicromega]
P:287 [in Coq.Vectors.VectorDef]
p:288 [in Coq.PArith.BinPos]
p:288 [in Coq.ZArith.BinInt]
P:288 [in Coq.FSets.FMapFacts]
p:288 [in Coq.Lists.SetoidList]
p:289 [in Coq.micromega.RingMicromega]
P:289 [in Coq.Init.Specif]
P:289 [in Coq.NArith.BinNat]
p:29 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:29 [in Coq.QArith.Qcanon]
p:29 [in Coq.PArith.BinPos]
p:29 [in Coq.Numbers.HexadecimalPos]
p:29 [in Coq.btauto.Algebra]
P:29 [in Coq.Logic.JMeq]
P:29 [in Coq.ZArith.Wf_Z]
P:29 [in Coq.Reals.Rsqrt_def]
p:29 [in Coq.Arith.Plus]
p:29 [in Coq.NArith.BinNat]
p:29 [in Coq.micromega.Env]
p:29 [in Coq.Numbers.NatInt.NZGcd]
p:29 [in Coq.Numbers.Natural.Abstract.NMaxMin]
P:29 [in Coq.Init.Datatypes]
p:29 [in Coq.Logic.HLevels]
p:29 [in Coq.Numbers.DecimalPos]
p:29 [in Coq.PArith.BinPosDef]
p:29 [in Coq.ZArith.Zcompare]
p:290 [in Coq.FSets.FMapList]
p:290 [in Coq.Lists.SetoidList]
p:291 [in Coq.PArith.BinPos]
p:291 [in Coq.micromega.ZMicromega]
p:292 [in Coq.micromega.RingMicromega]
p:292 [in Coq.Lists.SetoidList]
p:293 [in Coq.Init.Specif]
p:294 [in Coq.PArith.BinPos]
P:294 [in Coq.Lists.List]
p:294 [in Coq.Lists.SetoidList]
P:295 [in Coq.Init.Specif]
p:295 [in Coq.Reals.Rtopology]
p:296 [in Coq.PArith.BinPos]
P:296 [in Coq.micromega.EnvRing]
P:298 [in Coq.Lists.List]
P:298 [in Coq.Vectors.VectorDef]
p:299 [in Coq.PArith.BinPos]
P:299 [in Coq.Logic.Hurkens]
p:3 [in Coq.setoid_ring.BinList]
p:3 [in Coq.Logic.EqdepFacts]
P:3 [in Coq.ZArith.Zabs]
p:3 [in Coq.Numbers.NatInt.NZAddOrder]
p:3 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p:3 [in Coq.ZArith.Zpow_facts]
P:3 [in Coq.btauto.Algebra]
P:3 [in Coq.Reals.Rsqrt_def]
p:3 [in Coq.Numbers.Cyclic.Int63.Int63]
p:3 [in Coq.NArith.Ndist]
p:3 [in Coq.QArith.Qminmax]
p:3 [in Coq.rtauto.Bintree]
P:3 [in Coq.Logic.Berardi]
P:3 [in Coq.Bool.Sumbool]
P:3 [in Coq.Logic.ClassicalDescription]
p:3 [in Coq.Logic.Classical_Prop]
p:3 [in Coq.Numbers.Integer.Abstract.ZMulOrder]
p:3 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
p:3 [in Coq.Arith.Mult]
p:3 [in Coq.ZArith.Znat]
p:3 [in Coq.Numbers.AltBinNotations]
p:3 [in Coq.NArith.Ndec]
p:30 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:30 [in Coq.Numbers.Natural.Abstract.NSub]
p:30 [in Coq.Reals.Rminmax]
p:30 [in Coq.Floats.FloatLemmas]
P:30 [in Coq.setoid_ring.Ring_polynom]
p:30 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p:30 [in Coq.PArith.Pnat]
p:30 [in Coq.Reals.Rtrigo_alt]
p:30 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
p:30 [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
p:30 [in Coq.NArith.Ndigits]
p:30 [in Coq.Arith.Between]
p:30 [in Coq.Structures.EqualitiesFacts]
p:30 [in Coq.Numbers.NatInt.NZMul]
p:30 [in Coq.Numbers.NatInt.NZMulOrder]
p:30 [in Coq.Numbers.Natural.Abstract.NGcd]
P:30 [in Coq.Vectors.VectorDef]
p:30 [in Coq.Reals.Cos_plus]
p:300 [in Coq.ZArith.BinInt]
P:300 [in Coq.Logic.ChoiceFacts]
p:300 [in Coq.Init.Specif]
P:300 [in Coq.Init.Logic]
p:301 [in Coq.PArith.BinPos]
p:301 [in Coq.ZArith.BinInt]
p:301 [in Coq.NArith.BinNat]
P:302 [in Coq.Logic.Hurkens]
p:303 [in Coq.PArith.BinPos]
p:303 [in Coq.ZArith.BinInt]
P:303 [in Coq.Logic.ChoiceFacts]
P:303 [in Coq.Init.Specif]
P:304 [in Coq.Lists.SetoidList]
p:305 [in Coq.PArith.BinPos]
p:305 [in Coq.ZArith.BinInt]
P:305 [in Coq.Logic.Hurkens]
p:305 [in Coq.Reals.Rtopology]
p:306 [in Coq.ZArith.BinInt]
p:306 [in Coq.NArith.BinNat]
P:307 [in Coq.FSets.FSetBridge]
p:307 [in Coq.PArith.BinPos]
p:307 [in Coq.ZArith.BinInt]
p:307 [in Coq.Init.Specif]
p:308 [in Coq.ZArith.BinInt]
P:308 [in Coq.Logic.Hurkens]
p:309 [in Coq.PArith.BinPos]
p:309 [in Coq.ZArith.BinInt]
p:309 [in Coq.NArith.BinNat]
p:31 [in Coq.QArith.Qcanon]
p:31 [in Coq.Structures.OrdersLists]
p:31 [in Coq.Logic.EqdepFacts]
p:31 [in Coq.PArith.BinPos]
P:31 [in Coq.MSets.MSetProperties]
P:31 [in Coq.Logic.Epsilon]
p:31 [in Coq.PArith.Pnat]
p:31 [in Coq.btauto.Algebra]
p:31 [in Coq.Numbers.Cyclic.Int63.Int63]
p:31 [in Coq.setoid_ring.Integral_domain]
P:31 [in Coq.ssr.ssreflect]
p:31 [in Coq.NArith.BinNat]
p:31 [in Coq.micromega.Env]
p:31 [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
p:31 [in Coq.NArith.Ndigits]
p:31 [in Coq.Vectors.Fin]
p:31 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
P:31 [in Coq.Init.Datatypes]
p:31 [in Coq.Arith.Gt]
p:31 [in Coq.Arith.Mult]
P:31 [in Coq.FSets.FSetProperties]
P:310 [in Coq.FSets.FSetBridge]
p:310 [in Coq.ZArith.BinInt]
P:310 [in Coq.Init.Specif]
p:310 [in Coq.Reals.Rtopology]
P:310 [in Coq.Init.Logic]
p:311 [in Coq.PArith.BinPos]
P:311 [in Coq.FSets.FMapFacts]
p:312 [in Coq.ZArith.BinInt]
p:313 [in Coq.PArith.BinPos]
p:313 [in Coq.Reals.Rtopology]
p:314 [in Coq.ZArith.BinInt]
p:314 [in Coq.Init.Specif]
P:314 [in Coq.NArith.BinNat]
p:315 [in Coq.PArith.BinPos]
p:316 [in Coq.ZArith.BinInt]
p:317 [in Coq.PArith.BinPos]
p:317 [in Coq.ZArith.BinInt]
P:317 [in Coq.Logic.ChoiceFacts]
P:317 [in Coq.Init.Specif]
p:319 [in Coq.PArith.BinPos]
p:319 [in Coq.ZArith.BinInt]
P:319 [in Coq.NArith.BinNat]
P:32 [in Coq.Logic.Eqdep_dec]
p:32 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p:32 [in Coq.PArith.Pnat]
p:32 [in Coq.Reals.Abstract.ConstructivePower]
P:32 [in Coq.micromega.EnvRing]
p:32 [in Coq.ZArith.Int]
p:32 [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
p:32 [in Coq.ZArith.Zpower]
p:32 [in Coq.Numbers.Natural.Abstract.NMaxMin]
p:32 [in Coq.Numbers.Cyclic.Int31.Int31]
p:32 [in Coq.Logic.Classical_Prop]
p:32 [in Coq.Arith.Mult]
P:32 [in Coq.Logic.WKL]
p:32 [in Coq.Numbers.NatInt.NZAdd]
P:320 [in Coq.Logic.ChoiceFacts]
P:320 [in Coq.Init.Logic]
p:321 [in Coq.PArith.BinPos]
p:321 [in Coq.ZArith.BinInt]
p:322 [in Coq.Init.Specif]
p:323 [in Coq.PArith.BinPos]
p:323 [in Coq.ZArith.BinInt]
P:323 [in Coq.FSets.FMapFacts]
p:324 [in Coq.ZArith.BinInt]
p:325 [in Coq.PArith.BinPos]
p:325 [in Coq.Init.Specif]
p:326 [in Coq.PArith.BinPos]
p:326 [in Coq.ZArith.BinInt]
p:326 [in Coq.setoid_ring.Ring_polynom]
P:327 [in Coq.Init.Specif]
P:327 [in Coq.Init.Logic]
p:328 [in Coq.PArith.BinPos]
p:328 [in Coq.ZArith.BinInt]
p:329 [in Coq.PArith.BinPos]
P:33 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:33 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:33 [in Coq.QArith.Qcanon]
P:33 [in Coq.MSets.MSetInterface]
p:33 [in Coq.Structures.OrdersLists]
p:33 [in Coq.Reals.Rminmax]
p:33 [in Coq.PArith.BinPos]
P:33 [in Coq.Logic.ClassicalEpsilon]
p:33 [in Coq.btauto.Algebra]
P:33 [in Coq.Logic.JMeq]
P:33 [in Coq.ZArith.Wf_Z]
P:33 [in Coq.Reals.Rsqrt_def]
p:33 [in Coq.Reals.Rtrigo_alt]
p:33 [in Coq.Arith.Plus]
p:33 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
p:33 [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
p:33 [in Coq.NArith.Ndigits]
P:33 [in Coq.Vectors.Fin]
p:33 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
p:33 [in Coq.Logic.HLevels]
P:33 [in Coq.Lists.ListSet]
p:33 [in Coq.Arith.Between]
p:33 [in Coq.Numbers.NatInt.NZMulOrder]
p:330 [in Coq.PArith.BinPos]
p:330 [in Coq.ZArith.BinInt]
P:330 [in Coq.setoid_ring.Ring_polynom]
p:331 [in Coq.PArith.BinPos]
p:331 [in Coq.setoid_ring.Ring_polynom]
P:331 [in Coq.FSets.FMapFacts]
p:332 [in Coq.ZArith.BinInt]
P:332 [in Coq.Logic.ChoiceFacts]
p:333 [in Coq.PArith.BinPos]
P:333 [in Coq.Logic.ChoiceFacts]
P:333 [in Coq.Init.Specif]
p:334 [in Coq.ZArith.BinInt]
P:334 [in Coq.setoid_ring.Ring_polynom]
p:335 [in Coq.PArith.BinPos]
p:336 [in Coq.ZArith.BinInt]
p:337 [in Coq.ZArith.BinInt]
p:339 [in Coq.ZArith.BinInt]
P:339 [in Coq.setoid_ring.Ring_polynom]
P:339 [in Coq.Init.Specif]
p:34 [in Coq.Floats.FloatLemmas]
p:34 [in Coq.Numbers.Integer.Abstract.ZGcd]
P:34 [in Coq.Logic.Epsilon]
p:34 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p:34 [in Coq.PArith.Pnat]
p:34 [in Coq.setoid_ring.Integral_domain]
P:34 [in Coq.ssr.ssreflect]
P:34 [in Coq.NArith.BinNat]
P:34 [in Coq.Program.Equality]
P:34 [in Coq.Sorting.Sorted]
p:34 [in Coq.Numbers.NatInt.NZGcd]
p:34 [in Coq.ZArith.Zpower]
p:34 [in Coq.ZArith.Zbool]
P:34 [in Coq.Sorting.CPermutation]
p:34 [in Coq.Arith.Gt]
P:34 [in Coq.Logic.Diaconescu]
p:34 [in Coq.micromega.Refl]
p:34 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
p:34 [in Coq.ZArith.Zcompare]
p:340 [in Coq.setoid_ring.Ring_polynom]
p:340 [in Coq.micromega.EnvRing]
P:340 [in Coq.Logic.ChoiceFacts]
P:341 [in Coq.setoid_ring.Ring_polynom]
P:341 [in Coq.Logic.ChoiceFacts]
p:341 [in Coq.Init.Specif]
p:343 [in Coq.ZArith.BinInt]
P:343 [in Coq.setoid_ring.Ring_polynom]
P:344 [in Coq.micromega.EnvRing]
p:345 [in Coq.PArith.BinPos]
p:345 [in Coq.ZArith.BinInt]
P:345 [in Coq.setoid_ring.Ring_polynom]
p:345 [in Coq.micromega.EnvRing]
p:346 [in Coq.micromega.ZMicromega]
p:347 [in Coq.ZArith.BinInt]
p:347 [in Coq.Init.Specif]
P:348 [in Coq.setoid_ring.Ring_polynom]
P:348 [in Coq.micromega.EnvRing]
p:348 [in Coq.Logic.ChoiceFacts]
p:349 [in Coq.ZArith.BinInt]
P:349 [in Coq.Init.Specif]
P:35 [in Coq.Relations.Operators_Properties]
p:35 [in Coq.Logic.ConstructiveEpsilon]
p:35 [in Coq.Strings.OctalString]
p:35 [in Coq.PArith.BinPos]
p:35 [in Coq.Strings.HexString]
P:35 [in Coq.NArith.BinNat]
P:35 [in Coq.Classes.CMorphisms]
p:35 [in Coq.Strings.BinaryString]
p:35 [in Coq.Numbers.Natural.Abstract.NMaxMin]
p:35 [in Coq.Numbers.Cyclic.Int31.Int31]
p:35 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
p:35 [in Coq.Numbers.HexadecimalQ]
p:350 [in Coq.PArith.BinPos]
p:350 [in Coq.Logic.ChoiceFacts]
p:351 [in Coq.ZArith.BinInt]
p:352 [in Coq.PArith.BinPos]
p:352 [in Coq.ZArith.BinInt]
p:353 [in Coq.ZArith.BinInt]
P:353 [in Coq.micromega.EnvRing]
p:353 [in Coq.Init.Specif]
p:354 [in Coq.ZArith.BinInt]
p:354 [in Coq.setoid_ring.Ring_polynom]
p:354 [in Coq.micromega.EnvRing]
p:355 [in Coq.PArith.BinPos]
p:355 [in Coq.ZArith.BinInt]
P:355 [in Coq.micromega.EnvRing]
P:355 [in Coq.Init.Specif]
P:356 [in Coq.Logic.ChoiceFacts]
p:357 [in Coq.ZArith.BinInt]
P:357 [in Coq.micromega.EnvRing]
p:357 [in Coq.Init.Specif]
p:358 [in Coq.PArith.BinPos]
P:358 [in Coq.Logic.ChoiceFacts]
p:359 [in Coq.ZArith.BinInt]
P:359 [in Coq.micromega.EnvRing]
P:36 [in Coq.MSets.MSetInterface]
P:36 [in Coq.nsatz.NsatzTactic]
p:36 [in Coq.Reals.Rminmax]
P:36 [in Coq.Logic.EqdepFacts]
P:36 [in Coq.setoid_ring.Ring_polynom]
p:36 [in Coq.Reals.ArithProp]
p:36 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p:36 [in Coq.PArith.Pnat]
P:36 [in Coq.Classes.Morphisms]
p:36 [in Coq.Numbers.Natural.Abstract.NLcm]
P:36 [in Coq.Reals.Rsqrt_def]
p:36 [in Coq.Reals.Rtrigo_alt]
p:36 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
P:36 [in Coq.NArith.BinNat]
p:36 [in Coq.Program.Equality]
p:36 [in Coq.ZArith.Zpower]
p:36 [in Coq.Numbers.HexadecimalQ]
p:36 [in Coq.Arith.Between]
p:36 [in Coq.Numbers.NatInt.NZMulOrder]
P:36 [in Coq.Logic.WKL]
P:360 [in Coq.Logic.ChoiceFacts]
p:361 [in Coq.PArith.BinPos]
p:361 [in Coq.ZArith.BinInt]
p:361 [in Coq.Reals.Rtopology]
P:362 [in Coq.FSets.FMapFacts]
P:362 [in Coq.micromega.EnvRing]
p:363 [in Coq.ZArith.BinInt]
P:363 [in Coq.Logic.ChoiceFacts]
p:363 [in Coq.Init.Specif]
p:364 [in Coq.PArith.BinPos]
p:364 [in Coq.Reals.Rtopology]
p:365 [in Coq.ZArith.BinInt]
p:366 [in Coq.PArith.BinPos]
P:366 [in Coq.Init.Specif]
p:367 [in Coq.ZArith.BinInt]
p:367 [in Coq.Numbers.Cyclic.Int63.Int63]
p:368 [in Coq.Reals.Abstract.ConstructiveReals]
p:368 [in Coq.ZArith.BinInt]
p:368 [in Coq.micromega.EnvRing]
p:369 [in Coq.PArith.BinPos]
p:369 [in Coq.ZArith.BinInt]
p:369 [in Coq.Init.Specif]
p:37 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:37 [in Coq.Logic.ConstructiveEpsilon]
p:37 [in Coq.Logic.EqdepFacts]
p:37 [in Coq.PArith.BinPos]
P:37 [in Coq.Logic.JMeq]
P:37 [in Coq.ZArith.Wf_Z]
p:37 [in Coq.Arith.Plus]
P:37 [in Coq.Classes.CMorphisms]
p:37 [in Coq.Numbers.NatInt.NZGcd]
p:37 [in Coq.ZArith.Int]
p:37 [in Coq.NArith.Ndigits]
p:37 [in Coq.Vectors.Fin]
P:37 [in Coq.Sorting.CPermutation]
P:37 [in Coq.setoid_ring.Ncring_polynom]
p:37 [in Coq.Logic.HLevels]
p:37 [in Coq.Numbers.HexadecimalQ]
p:37 [in Coq.Arith.Gt]
p:37 [in Coq.ZArith.Zcompare]
p:370 [in Coq.ZArith.BinInt]
P:370 [in Coq.setoid_ring.Ring_polynom]
p:370 [in Coq.micromega.ZMicromega]
p:371 [in Coq.ZArith.BinInt]
P:371 [in Coq.FSets.FMapFacts]
P:371 [in Coq.Init.Logic]
p:372 [in Coq.PArith.BinPos]
p:372 [in Coq.ZArith.BinInt]
p:373 [in Coq.ZArith.BinInt]
p:374 [in Coq.PArith.BinPos]
p:374 [in Coq.Init.Specif]
p:375 [in Coq.ZArith.BinInt]
P:376 [in Coq.setoid_ring.Ring_polynom]
P:376 [in Coq.Init.Specif]
p:377 [in Coq.PArith.BinPos]
p:377 [in Coq.ZArith.BinInt]
p:377 [in Coq.ssr.ssrbool]
p:379 [in Coq.ZArith.BinInt]
p:379 [in Coq.FSets.FMapWeakList]
P:379 [in Coq.Init.Logic]
P:38 [in Coq.nsatz.NsatzTactic]
p:38 [in Coq.Numbers.Integer.Abstract.ZAdd]
P:38 [in Coq.Init.Peano]
p:38 [in Coq.Floats.FloatLemmas]
p:38 [in Coq.ZArith.BinInt]
P:38 [in Coq.micromega.EnvRing]
p:38 [in Coq.Numbers.DecimalQ]
p:38 [in Coq.FSets.FMapInterface]
P:38 [in Coq.Sorting.Sorted]
p:38 [in Coq.ZArith.Zpower]
p:38 [in Coq.ZArith.Zorder]
p:38 [in Coq.NArith.Ndigits]
p:38 [in Coq.Numbers.Natural.Abstract.NMaxMin]
p:38 [in Coq.Numbers.HexadecimalQ]
p:38 [in Coq.Structures.EqualitiesFacts]
p:38 [in Coq.btauto.Reflect]
p:380 [in Coq.PArith.BinPos]
p:380 [in Coq.ssr.ssrbool]
p:382 [in Coq.ZArith.BinInt]
p:382 [in Coq.Init.Specif]
p:382 [in Coq.ssr.ssrbool]
p:384 [in Coq.PArith.BinPos]
p:384 [in Coq.ZArith.BinInt]
P:385 [in Coq.Init.Specif]
p:385 [in Coq.ssr.ssrbool]
p:386 [in Coq.ssr.ssrbool]
p:387 [in Coq.PArith.BinPos]
p:389 [in Coq.ssr.ssrbool]
P:39 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
P:39 [in Coq.Relations.Operators_Properties]
p:39 [in Coq.Numbers.Natural.Abstract.NSub]
P:39 [in Coq.setoid_ring.Ring_polynom]
p:39 [in Coq.Numbers.Natural.Abstract.NLcm]
p:39 [in Coq.Numbers.DecimalQ]
P:39 [in Coq.Reals.Rsqrt_def]
p:39 [in Coq.Init.Wf]
p:39 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
p:39 [in Coq.ZArith.Zeven]
p:39 [in Coq.ssr.ssreflect]
p:39 [in Coq.ZArith.Zbool]
p:39 [in Coq.Structures.GenericMinMax]
P:39 [in Coq.Lists.ListSet]
P:39 [in Coq.Reals.RList]
p:39 [in Coq.Arith.Between]
p:39 [in Coq.Numbers.NatInt.NZMulOrder]
p:39 [in Coq.Reals.Cos_plus]
p:390 [in Coq.PArith.BinPos]
p:390 [in Coq.ssr.ssrbool]
p:391 [in Coq.Init.Specif]
P:391 [in Coq.Init.Logic]
P:393 [in Coq.Init.Specif]
p:393 [in Coq.ssr.ssrbool]
p:394 [in Coq.PArith.BinPos]
P:395 [in Coq.Init.Logic]
p:397 [in Coq.PArith.BinPos]
p:399 [in Coq.Init.Specif]
p:4 [in Coq.Numbers.Natural.Abstract.NIso]
P:4 [in Coq.FSets.FSetDecide]
p:4 [in Coq.PArith.Pnat]
P:4 [in Coq.Logic.PropExtensionality]
P:4 [in Coq.MSets.MSetDecide]
p:4 [in Coq.Structures.DecidableType]
p:4 [in Coq.Numbers.NatInt.NZGcd]
P:4 [in Coq.Logic.Classical_Prop]
p:4 [in Coq.ZArith.Znat]
p:40 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:40 [in Coq.Numbers.DecimalQ]
p:40 [in Coq.FSets.FMapInterface]
P:40 [in Coq.Program.Equality]
p:40 [in Coq.rtauto.Bintree]
p:40 [in Coq.Numbers.NatInt.NZGcd]
p:40 [in Coq.ZArith.Int]
p:40 [in Coq.Vectors.Fin]
P:40 [in Coq.Logic.Berardi]
p:40 [in Coq.micromega.RMicromega]
P:40 [in Coq.Logic.WKL]
P:40 [in Coq.Sorting.Heap]
p:400 [in Coq.PArith.BinPos]
P:401 [in Coq.Init.Specif]
p:401 [in Coq.ssr.ssrbool]
P:401 [in Coq.Init.Logic]
p:403 [in Coq.PArith.BinPos]
p:404 [in Coq.ssr.ssrbool]
P:405 [in Coq.Init.Logic]
p:406 [in Coq.PArith.BinPos]
p:407 [in Coq.Init.Specif]
p:407 [in Coq.ssr.ssrbool]
p:408 [in Coq.ZArith.BinInt]
P:409 [in Coq.Init.Specif]
p:41 [in Coq.Numbers.Integer.Abstract.ZAdd]
P:41 [in Coq.Sets.Finite_sets_facts]
p:41 [in Coq.PArith.BinPos]
p:41 [in Coq.ZArith.BinInt]
p:41 [in Coq.Numbers.Integer.Abstract.ZGcd]
P:41 [in Coq.setoid_ring.Ring_polynom]
P:41 [in Coq.micromega.EnvRing]
p:41 [in Coq.btauto.Algebra]
P:41 [in Coq.Logic.JMeq]
P:41 [in Coq.ZArith.Wf_Z]
p:41 [in Coq.Numbers.DecimalQ]
p:41 [in Coq.Arith.Plus]
p:41 [in Coq.NArith.BinNat]
p:41 [in Coq.ZArith.Zorder]
p:41 [in Coq.Numbers.Natural.Abstract.NMaxMin]
p:41 [in Coq.Logic.HLevels]
p:41 [in Coq.Arith.Gt]
p:41 [in Coq.Structures.EqualitiesFacts]
p:41 [in Coq.Arith.Mult]
p:41 [in Coq.Reals.ClassicalConstructiveReals]
p:410 [in Coq.PArith.BinPos]
p:410 [in Coq.ssr.ssrbool]
p:410 [in Coq.MSets.MSetRBT]
P:411 [in Coq.Init.Logic]
p:412 [in Coq.MSets.MSetRBT]
p:413 [in Coq.PArith.BinPos]
p:413 [in Coq.ssr.ssrbool]
p:414 [in Coq.ssr.ssrbool]
p:416 [in Coq.PArith.BinPos]
p:417 [in Coq.Init.Specif]
P:418 [in Coq.setoid_ring.Ring_polynom]
p:418 [in Coq.Init.Specif]
p:42 [in Coq.Numbers.Natural.Abstract.NSub]
p:42 [in Coq.Structures.OrdersLists]
P:42 [in Coq.Logic.EqdepFacts]
p:42 [in Coq.Numbers.HexadecimalPos]
P:42 [in Coq.Arith.Wf_nat]
p:42 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
p:42 [in Coq.ssr.ssreflect]
p:42 [in Coq.Program.Equality]
p:42 [in Coq.Vectors.Fin]
p:42 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
P:42 [in Coq.Sorting.CPermutation]
p:42 [in Coq.Arith.Between]
p:42 [in Coq.Numbers.DecimalPos]
p:42 [in Coq.Numbers.NatInt.NZMulOrder]
P:42 [in Coq.Vectors.VectorDef]
p:42 [in Coq.Reals.Cos_plus]
p:420 [in Coq.PArith.BinPos]
P:420 [in Coq.Logic.ChoiceFacts]
P:421 [in Coq.Init.Specif]
p:422 [in Coq.PArith.BinPos]
P:422 [in Coq.Logic.ChoiceFacts]
P:422 [in Coq.Init.Logic]
p:425 [in Coq.PArith.BinPos]
p:426 [in Coq.PArith.BinPos]
P:426 [in Coq.setoid_ring.Ring_polynom]
p:426 [in Coq.setoid_ring.Field_theory]
p:427 [in Coq.PArith.BinPos]
p:427 [in Coq.Init.Specif]
p:428 [in Coq.PArith.BinPos]
p:428 [in Coq.Init.Specif]
p:428 [in Coq.ssr.ssrbool]
p:429 [in Coq.ZArith.BinInt]
p:429 [in Coq.setoid_ring.Field_theory]
p:43 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
P:43 [in Coq.nsatz.NsatzTactic]
p:43 [in Coq.Logic.EqdepFacts]
p:43 [in Coq.Numbers.NatInt.NZAddOrder]
P:43 [in Coq.micromega.EnvRing]
p:43 [in Coq.btauto.Algebra]
p:43 [in Coq.Numbers.Natural.Abstract.NLcm]
P:43 [in Coq.Reals.Rsqrt_def]
p:43 [in Coq.NArith.BinNat]
p:43 [in Coq.Numbers.NatInt.NZGcd]
p:43 [in Coq.ZArith.Int]
p:43 [in Coq.Sets.Image]
P:43 [in Coq.Logic.WKL]
p:430 [in Coq.PArith.BinPos]
P:431 [in Coq.Init.Specif]
p:432 [in Coq.ZArith.BinInt]
p:433 [in Coq.PArith.BinPos]
P:434 [in Coq.Init.Logic]
P:435 [in Coq.setoid_ring.Ring_polynom]
p:435 [in Coq.setoid_ring.Field_theory]
p:436 [in Coq.PArith.BinPos]
p:437 [in Coq.Init.Specif]
p:437 [in Coq.ssr.ssrbool]
p:438 [in Coq.PArith.BinPos]
p:438 [in Coq.ZArith.BinInt]
p:438 [in Coq.Numbers.Cyclic.Int63.Int63]
p:438 [in Coq.setoid_ring.Field_theory]
p:439 [in Coq.FSets.FMapFacts]
p:439 [in Coq.Init.Logic]
P:44 [in Coq.Relations.Operators_Properties]
P:44 [in Coq.Sets.Finite_sets_facts]
p:44 [in Coq.PArith.BinPos]
p:44 [in Coq.Reals.Exp_prop]
p:44 [in Coq.Numbers.Cyclic.Int63.Int63]
p:44 [in Coq.micromega.OrderedRing]
p:44 [in Coq.ZArith.Zorder]
p:44 [in Coq.NArith.Ndigits]
p:44 [in Coq.Numbers.Natural.Abstract.NMaxMin]
p:44 [in Coq.Numbers.NatInt.NZParity]
P:44 [in Coq.setoid_ring.Ncring_polynom]
p:44 [in Coq.Numbers.NatInt.NZOrder]
p:44 [in Coq.Arith.Gt]
p:44 [in Coq.Reals.ClassicalConstructiveReals]
p:440 [in Coq.PArith.BinPos]
p:440 [in Coq.setoid_ring.Ring_polynom]
p:441 [in Coq.FSets.FMapFacts]
P:441 [in Coq.Init.Specif]
P:442 [in Coq.Init.Logic]
p:443 [in Coq.PArith.BinPos]
p:443 [in Coq.setoid_ring.Ring_polynom]
P:444 [in Coq.Logic.ChoiceFacts]
p:444 [in Coq.Init.Specif]
p:446 [in Coq.PArith.BinPos]
P:446 [in Coq.Logic.ChoiceFacts]
p:447 [in Coq.setoid_ring.Ring_polynom]
p:447 [in Coq.Init.Logic]
P:448 [in Coq.Logic.ChoiceFacts]
p:449 [in Coq.PArith.BinPos]
P:449 [in Coq.Logic.ChoiceFacts]
p:449 [in Coq.FSets.FMapList]
p:45 [in Coq.Numbers.Natural.Abstract.NSub]
p:45 [in Coq.Arith.Wf_nat]
P:45 [in Coq.Logic.JMeq]
p:45 [in Coq.Numbers.Natural.Abstract.NDefOps]
p:45 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
p:45 [in Coq.Reals.Abstract.ConstructiveLimits]
p:45 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
p:45 [in Coq.Numbers.HexadecimalQ]
p:45 [in Coq.Structures.EqualitiesFacts]
p:45 [in Coq.NArith.BinNatDef]
P:45 [in Coq.Sorting.Heap]
p:450 [in Coq.ZArith.BinInt]
P:450 [in Coq.Init.Logic]
p:452 [in Coq.PArith.BinPos]
p:452 [in Coq.Init.Specif]
p:452 [in Coq.Init.Logic]
p:453 [in Coq.FSets.FMapList]
P:454 [in Coq.Init.Specif]
p:455 [in Coq.PArith.BinPos]
p:456 [in Coq.ssr.ssrbool]
p:457 [in Coq.ZArith.BinInt]
p:458 [in Coq.FSets.FMapWeakList]
p:459 [in Coq.Init.Logic]
p:46 [in Coq.ZArith.BinInt]
P:46 [in Coq.setoid_ring.Ring_polynom]
P:46 [in Coq.Arith.Wf_nat]
p:46 [in Coq.btauto.Algebra]
P:46 [in Coq.ZArith.Wf_Z]
p:46 [in Coq.Init.Wf]
p:46 [in Coq.ZArith.Zeven]
P:46 [in Coq.NArith.BinNat]
p:46 [in Coq.rtauto.Bintree]
p:46 [in Coq.Numbers.NatInt.NZGcd]
p:46 [in Coq.ZArith.Int]
p:46 [in Coq.Logic.HLevels]
p:46 [in Coq.setoid_ring.Ring_theory]
p:46 [in Coq.Numbers.HexadecimalQ]
p:46 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
p:46 [in Coq.micromega.RMicromega]
P:46 [in Coq.Logic.WKL]
p:46 [in Coq.Reals.Abstract.ConstructiveSum]
p:46 [in Coq.Numbers.Natural.Abstract.NGcd]
p:460 [in Coq.PArith.BinPos]
p:460 [in Coq.ZArith.BinInt]
p:460 [in Coq.Init.Specif]
p:461 [in Coq.Init.Specif]
P:462 [in Coq.Init.Logic]
p:463 [in Coq.PArith.BinPos]
p:463 [in Coq.ZArith.BinInt]
P:463 [in Coq.Init.Specif]
p:464 [in Coq.FSets.FMapWeakList]
p:465 [in Coq.FSets.FMapWeakList]
p:465 [in Coq.Init.Logic]
p:466 [in Coq.PArith.BinPos]
p:466 [in Coq.ZArith.BinInt]
p:466 [in Coq.setoid_ring.Field_theory]
P:468 [in Coq.setoid_ring.Ring_polynom]
p:468 [in Coq.setoid_ring.Field_theory]
p:469 [in Coq.ZArith.BinInt]
p:47 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:47 [in Coq.PArith.BinPos]
p:47 [in Coq.Numbers.NatInt.NZAddOrder]
p:47 [in Coq.Reals.Exp_prop]
p:47 [in Coq.Numbers.Natural.Abstract.NLcm]
p:47 [in Coq.ZArith.Zeven]
p:47 [in Coq.ZArith.Zpower]
p:47 [in Coq.ZArith.Zorder]
p:47 [in Coq.Numbers.NatInt.NZParity]
p:47 [in Coq.Numbers.NatInt.NZOrder]
p:47 [in Coq.micromega.RMicromega]
P:47 [in Coq.Vectors.VectorDef]
p:470 [in Coq.Init.Specif]
p:470 [in Coq.Init.Logic]
P:473 [in Coq.Init.Logic]
p:474 [in Coq.Init.Specif]
p:475 [in Coq.FSets.FMapWeakList]
p:475 [in Coq.FSets.FMapList]
P:476 [in Coq.Init.Specif]
p:476 [in Coq.FSets.FMapWeakList]
p:476 [in Coq.FSets.FMapList]
p:477 [in Coq.PArith.BinPos]
P:477 [in Coq.setoid_ring.Ring_polynom]
p:479 [in Coq.PArith.BinPos]
p:48 [in Coq.Numbers.Natural.Abstract.NSub]
P:48 [in Coq.Logic.Eqdep_dec]
p:48 [in Coq.Numbers.Integer.Abstract.ZAdd]
P:48 [in Coq.Logic.EqdepFacts]
p:48 [in Coq.Numbers.Integer.Abstract.ZGcd]
P:48 [in Coq.micromega.EnvRing]
p:48 [in Coq.Numbers.Natural.Abstract.NDefOps]
P:48 [in Coq.Reals.Rsqrt_def]
P:48 [in Coq.ssr.ssrbool]
p:48 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
P:48 [in Coq.Reals.Rbasic_fun]
p:480 [in Coq.setoid_ring.Field_theory]
p:481 [in Coq.PArith.BinPos]
p:481 [in Coq.ZArith.BinInt]
p:481 [in Coq.Init.Logic]
p:482 [in Coq.Init.Logic]
p:483 [in Coq.PArith.BinPos]
P:484 [in Coq.Init.Specif]
p:485 [in Coq.PArith.BinPos]
P:485 [in Coq.setoid_ring.Ring_polynom]
P:485 [in Coq.ssr.ssrbool]
P:485 [in Coq.Init.Logic]
p:486 [in Coq.PArith.BinPos]
p:488 [in Coq.setoid_ring.Ring_polynom]
p:49 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:49 [in Coq.Logic.Eqdep_dec]
p:49 [in Coq.Structures.OrdersLists]
P:49 [in Coq.FSets.FSetBridge]
p:49 [in Coq.Logic.EqdepFacts]
p:49 [in Coq.Numbers.HexadecimalPos]
P:49 [in Coq.setoid_ring.Ring_polynom]
p:49 [in Coq.ZArith.Zpow_facts]
p:49 [in Coq.Arith.Wf_nat]
p:49 [in Coq.Arith.Plus]
P:49 [in Coq.NArith.BinNat]
p:49 [in Coq.Program.Equality]
p:49 [in Coq.Numbers.NatInt.NZGcd]
p:49 [in Coq.ZArith.Int]
p:49 [in Coq.ZArith.Zpower]
P:49 [in Coq.Vectors.Fin]
p:49 [in Coq.Numbers.DecimalPos]
p:49 [in Coq.Numbers.NatInt.NZMulOrder]
P:49 [in Coq.Logic.WKL]
p:49 [in Coq.Numbers.Natural.Abstract.NGcd]
p:49 [in Coq.QArith.Qpower]
p:492 [in Coq.setoid_ring.Ring_polynom]
P:492 [in Coq.Init.Specif]
p:493 [in Coq.Init.Logic]
p:494 [in Coq.PArith.BinPos]
p:495 [in Coq.PArith.BinPos]
p:495 [in Coq.Init.Specif]
P:495 [in Coq.ssr.ssrbool]
p:495 [in Coq.FSets.FMapList]
p:496 [in Coq.setoid_ring.Ring_polynom]
p:496 [in Coq.FSets.FMapList]
P:497 [in Coq.Init.Logic]
p:498 [in Coq.ZArith.BinInt]
p:498 [in Coq.FSets.FMapFacts]
p:499 [in Coq.setoid_ring.Ring_polynom]
P:5 [in Coq.Logic.Classical_Pred_Type]
P:5 [in Coq.Reals.Abstract.ConstructiveLUB]
p:5 [in Coq.Structures.OrdersEx]
P:5 [in Coq.QArith.Qcabs]
p:5 [in Coq.ZArith.Zmax]
p:5 [in Coq.ZArith.Zpow_facts]
P:5 [in Coq.btauto.Algebra]
P:5 [in Coq.ZArith.Wf_Z]
p:5 [in Coq.Numbers.Cyclic.Int63.Int63]
p:5 [in Coq.Numbers.Natural.Abstract.NAddOrder]
p:5 [in Coq.Arith.Plus]
P:5 [in Coq.QArith.Qabs]
p:5 [in Coq.NArith.Ndigits]
P:5 [in Coq.Vectors.Fin]
p:5 [in Coq.ZArith.Zpow_alt]
P:5 [in Coq.Reals.Rbasic_fun]
P:5 [in Coq.ZArith.ZArith_dec]
P:5 [in Coq.Bool.Sumbool]
P:5 [in Coq.Logic.Classical_Prop]
P:5 [in Coq.Classes.DecidableClass]
p:5 [in Coq.Numbers.NatInt.NZMulOrder]
p:5 [in Coq.ZArith.Zcomplements]
p:5 [in Coq.ZArith.Znat]
p:5 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
p:5 [in Coq.Numbers.Natural.Abstract.NAdd]
p:5 [in Coq.NArith.Ndec]
P:5 [in Coq.Init.Tactics]
p:50 [in Coq.PArith.BinPos]
p:50 [in Coq.Numbers.HexadecimalPos]
p:50 [in Coq.ZArith.BinInt]
p:50 [in Coq.Strings.String]
P:50 [in Coq.Arith.Wf_nat]
p:50 [in Coq.Reals.Exp_prop]
p:50 [in Coq.setoid_ring.Field_theory]
p:50 [in Coq.Reals.Rdefinitions]
p:50 [in Coq.ZArith.Zpower]
p:50 [in Coq.NArith.Ndigits]
p:50 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
p:50 [in Coq.Numbers.DecimalPos]
p:50 [in Coq.Reals.Cos_rel]
p:500 [in Coq.Init.Logic]
p:501 [in Coq.ZArith.BinInt]
P:501 [in Coq.setoid_ring.Ring_polynom]
p:503 [in Coq.Init.Specif]
p:504 [in Coq.Init.Logic]
p:506 [in Coq.ZArith.BinInt]
p:508 [in Coq.ZArith.BinInt]
p:509 [in Coq.Reals.RIneq]
p:51 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:51 [in Coq.Numbers.Natural.Abstract.NSub]
p:51 [in Coq.Numbers.Integer.Abstract.ZAdd]
p:51 [in Coq.Numbers.HexadecimalPos]
P:51 [in Coq.MSets.MSetProperties]
p:51 [in Coq.Numbers.NatInt.NZAddOrder]
P:51 [in Coq.micromega.EnvRing]
p:51 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
p:51 [in Coq.Reals.Abstract.ConstructiveLimits]
P:51 [in Coq.Reals.Rbasic_fun]
p:51 [in Coq.Structures.GenericMinMax]
p:51 [in Coq.Numbers.DecimalPos]
P:51 [in Coq.FSets.FSetProperties]
p:510 [in Coq.ZArith.BinInt]
p:511 [in Coq.setoid_ring.Ring_polynom]
p:511 [in Coq.Init.Specif]
p:513 [in Coq.Init.Logic]
p:514 [in Coq.PArith.BinPos]
p:515 [in Coq.setoid_ring.Ring_polynom]
P:516 [in Coq.Init.Specif]
P:516 [in Coq.Init.Logic]
p:517 [in Coq.PArith.BinPos]
p:518 [in Coq.setoid_ring.Ring_polynom]
p:52 [in Coq.Structures.OrdersLists]
p:52 [in Coq.ZArith.Zpow_facts]
P:52 [in Coq.Reals.Rsqrt_def]
p:52 [in Coq.setoid_ring.Field_theory]
p:52 [in Coq.Arith.Plus]
p:52 [in Coq.Numbers.NatInt.NZGcd]
p:52 [in Coq.ZArith.Int]
P:52 [in Coq.setoid_ring.Ncring_polynom]
p:52 [in Coq.Numbers.NatInt.NZMulOrder]
p:52 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
P:52 [in Coq.Logic.WKL]
p:52 [in Coq.Numbers.Natural.Abstract.NGcd]
p:520 [in Coq.PArith.BinPos]
p:520 [in Coq.setoid_ring.Ring_polynom]
p:520 [in Coq.Init.Specif]
p:521 [in Coq.Init.Specif]
p:521 [in Coq.Init.Logic]
p:522 [in Coq.Init.Logic]
p:523 [in Coq.PArith.BinPos]
p:523 [in Coq.setoid_ring.Ring_polynom]
p:525 [in Coq.setoid_ring.Ring_polynom]
p:526 [in Coq.PArith.BinPos]
p:526 [in Coq.Init.Specif]
p:526 [in Coq.Reals.RIneq]
P:527 [in Coq.setoid_ring.Ring_polynom]
p:527 [in Coq.Init.Specif]
p:527 [in Coq.Reals.RIneq]
p:527 [in Coq.Init.Logic]
p:528 [in Coq.Reals.RIneq]
p:528 [in Coq.Init.Logic]
p:529 [in Coq.PArith.BinPos]
P:529 [in Coq.Init.Specif]
P:53 [in Coq.FSets.FSetBridge]
p:53 [in Coq.PArith.BinPos]
P:53 [in Coq.setoid_ring.Ring_polynom]
p:53 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p:53 [in Coq.Reals.Exp_prop]
p:53 [in Coq.Init.Wf]
P:53 [in Coq.NArith.BinNat]
p:53 [in Coq.Reals.Rdefinitions]
P:53 [in Coq.Vectors.VectorDef]
p:530 [in Coq.Reals.RIneq]
p:532 [in Coq.PArith.BinPos]
p:535 [in Coq.PArith.BinPos]
p:535 [in Coq.Init.Specif]
p:538 [in Coq.PArith.BinPos]
P:538 [in Coq.Init.Specif]
p:54 [in Coq.Numbers.Natural.Abstract.NSub]
p:54 [in Coq.Numbers.Integer.Abstract.ZAdd]
P:54 [in Coq.Logic.EqdepFacts]
p:54 [in Coq.Numbers.HexadecimalPos]
p:54 [in Coq.Strings.String]
P:54 [in Coq.Arith.Wf_nat]
P:54 [in Coq.Init.Specif]
p:54 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
P:54 [in Coq.NArith.BinNat]
p:54 [in Coq.micromega.OrderedRing]
p:54 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
p:54 [in Coq.Numbers.DecimalPos]
p:54 [in Coq.PArith.BinPosDef]
p:54 [in Coq.Reals.Cos_rel]
P:541 [in Coq.ssr.ssrbool]
P:543 [in Coq.ssr.ssrbool]
p:544 [in Coq.Init.Specif]
P:545 [in Coq.ssr.ssrbool]
P:546 [in Coq.Init.Specif]
P:547 [in Coq.ssr.ssrbool]
p:55 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
P:55 [in Coq.Logic.Eqdep_dec]
p:55 [in Coq.Logic.EqdepFacts]
p:55 [in Coq.micromega.RingMicromega]
p:55 [in Coq.Numbers.NatInt.NZAddOrder]
p:55 [in Coq.ZArith.BinInt]
P:55 [in Coq.micromega.EnvRing]
p:55 [in Coq.btauto.Algebra]
P:55 [in Coq.NArith.BinNat]
p:55 [in Coq.ZArith.Int]
p:55 [in Coq.Init.Datatypes]
p:55 [in Coq.Numbers.NatInt.NZMulOrder]
P:55 [in Coq.Logic.WKL]
p:55 [in Coq.Numbers.Natural.Abstract.NGcd]
p:55 [in Coq.QArith.QArith_base]
P:550 [in Coq.ssr.ssrbool]
p:552 [in Coq.Init.Specif]
P:553 [in Coq.ssr.ssrbool]
P:554 [in Coq.Init.Specif]
p:555 [in Coq.PArith.BinPos]
p:557 [in Coq.PArith.BinPos]
P:557 [in Coq.ssr.ssrbool]
p:559 [in Coq.PArith.BinPos]
P:56 [in Coq.FSets.FSetBridge]
p:56 [in Coq.PArith.BinPos]
p:56 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p:56 [in Coq.ZArith.Zpow_facts]
p:56 [in Coq.Reals.Exp_prop]
p:56 [in Coq.NArith.Ndigits]
P:56 [in Coq.setoid_ring.Ncring_polynom]
p:56 [in Coq.Numbers.Integer.Abstract.ZMulOrder]
p:56 [in Coq.Lists.SetoidList]
p:560 [in Coq.Init.Specif]
p:561 [in Coq.PArith.BinPos]
P:561 [in Coq.ssr.ssrbool]
p:562 [in Coq.PArith.BinPos]
P:562 [in Coq.Init.Specif]
p:564 [in Coq.PArith.BinPos]
P:565 [in Coq.ssr.ssrbool]
p:567 [in Coq.PArith.BinPos]
p:57 [in Coq.Numbers.Natural.Abstract.NSub]
p:57 [in Coq.Numbers.Integer.Abstract.ZAdd]
p:57 [in Coq.Numbers.NaryFunctions]
p:57 [in Coq.Arith.Wf_nat]
P:57 [in Coq.Reals.Rsqrt_def]
p:57 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
p:57 [in Coq.Structures.OrderedTypeEx]
p:57 [in Coq.ZArith.Int]
p:57 [in Coq.Init.Datatypes]
p:57 [in Coq.setoid_ring.Ring_theory]
p:57 [in Coq.PArith.BinPosDef]
p:570 [in Coq.PArith.BinPos]
p:570 [in Coq.Init.Specif]
p:571 [in Coq.Init.Specif]
P:571 [in Coq.ssr.ssrbool]
p:572 [in Coq.PArith.BinPos]
P:574 [in Coq.Init.Specif]
P:574 [in Coq.ssr.ssrbool]
p:575 [in Coq.PArith.BinPos]
P:578 [in Coq.ssr.ssrbool]
p:58 [in Coq.QArith.Qcanon]
p:58 [in Coq.ZArith.Zpow_facts]
P:58 [in Coq.Arith.Wf_nat]
P:58 [in Coq.NArith.BinNat]
p:58 [in Coq.rtauto.Bintree]
p:58 [in Coq.Numbers.NatInt.NZMulOrder]
P:58 [in Coq.Logic.ClassicalFacts]
P:58 [in Coq.Logic.WKL]
p:580 [in Coq.Init.Specif]
p:581 [in Coq.Init.Specif]
p:584 [in Coq.Lists.List]
P:584 [in Coq.Init.Specif]
p:586 [in Coq.Lists.List]
p:59 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:59 [in Coq.PArith.BinPos]
p:59 [in Coq.Numbers.NatInt.NZAddOrder]
p:59 [in Coq.Numbers.Integer.Abstract.ZGcd]
p:59 [in Coq.Reals.Exp_prop]
p:59 [in Coq.ZArith.Int]
p:59 [in Coq.PArith.BinPosDef]
p:59 [in Coq.Reals.Abstract.ConstructiveSum]
p:59 [in Coq.rtauto.Rtauto]
p:590 [in Coq.Init.Specif]
P:594 [in Coq.Init.Specif]
p:594 [in Coq.FSets.FMapWeakList]
p:595 [in Coq.PArith.BinPos]
p:597 [in Coq.Init.Specif]
p:598 [in Coq.PArith.BinPos]
p:6 [in Coq.Strings.OctalString]
p:6 [in Coq.Strings.HexString]
p:6 [in Coq.Numbers.NatInt.NZAddOrder]
p:6 [in Coq.PArith.Pnat]
p:6 [in Coq.QArith.Qminmax]
P:6 [in Coq.Logic.ClassicalChoice]
p:6 [in Coq.Numbers.DecimalN]
p:6 [in Coq.Strings.BinaryString]
p:6 [in Coq.Vectors.Fin]
p:6 [in Coq.Numbers.HexadecimalN]
p:6 [in Coq.Logic.ProofIrrelevanceFacts]
P:6 [in Coq.Logic.PropExtensionalityFacts]
p:6 [in Coq.ZArith.Zcomplements]
p:6 [in Coq.ZArith.Znat]
p:6 [in Coq.Numbers.Natural.Abstract.NGcd]
p:6 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
P:6 [in Coq.Reals.ClassicalDedekindReals]
p:60 [in Coq.Numbers.Natural.Abstract.NSub]
P:60 [in Coq.Logic.Eqdep_dec]
p:60 [in Coq.Numbers.Integer.Abstract.ZAdd]
P:60 [in Coq.Logic.EqdepFacts]
p:60 [in Coq.Numbers.HexadecimalPos]
P:60 [in Coq.setoid_ring.Ring_polynom]
p:60 [in Coq.PArith.Pnat]
p:60 [in Coq.btauto.Algebra]
p:60 [in Coq.Init.Specif]
p:60 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
p:60 [in Coq.Numbers.DecimalPos]
p:603 [in Coq.PArith.BinPos]
p:605 [in Coq.Init.Specif]
p:606 [in Coq.PArith.BinPos]
P:607 [in Coq.Init.Specif]
p:608 [in Coq.PArith.BinPos]
p:609 [in Coq.PArith.BinPos]
p:61 [in Coq.Vectors.VectorSpec]
p:61 [in Coq.nsatz.NsatzTactic]
p:61 [in Coq.Logic.Eqdep_dec]
p:61 [in Coq.Logic.EqdepFacts]
p:61 [in Coq.PArith.Pnat]
p:61 [in Coq.Arith.Wf_nat]
P:61 [in Coq.Logic.FunctionalExtensionality]
p:61 [in Coq.Numbers.Natural.Abstract.NLcm]
P:61 [in Coq.Reals.Rsqrt_def]
p:61 [in Coq.Numbers.NatInt.NZGcd]
p:61 [in Coq.ZArith.Int]
p:61 [in Coq.Init.Datatypes]
p:61 [in Coq.setoid_ring.Ring_theory]
p:61 [in Coq.Numbers.NatInt.NZMulOrder]
P:61 [in Coq.Logic.WKL]
p:61 [in Coq.PArith.BinPosDef]
p:610 [in Coq.PArith.BinPos]
p:611 [in Coq.PArith.BinPos]
p:613 [in Coq.PArith.BinPos]
p:613 [in Coq.Init.Specif]
p:614 [in Coq.FSets.FMapFacts]
p:614 [in Coq.Init.Specif]
p:615 [in Coq.PArith.BinPos]
p:615 [in Coq.FSets.FMapList]
p:616 [in Coq.PArith.BinPos]
p:616 [in Coq.FSets.FMapFacts]
P:616 [in Coq.Init.Specif]
p:618 [in Coq.FSets.FMapFacts]
p:619 [in Coq.PArith.BinPos]
P:62 [in Coq.FSets.FSetBridge]
p:62 [in Coq.PArith.BinPos]
P:62 [in Coq.MSets.MSetProperties]
p:62 [in Coq.Numbers.Integer.Abstract.ZGcd]
p:62 [in Coq.ZArith.Zpow_facts]
P:62 [in Coq.Arith.Wf_nat]
P:62 [in Coq.micromega.EnvRing]
P:62 [in Coq.Logic.Diaconescu]
P:62 [in Coq.FSets.FSetProperties]
p:620 [in Coq.FSets.FMapFacts]
p:622 [in Coq.FSets.FMapFacts]
p:623 [in Coq.Init.Specif]
p:624 [in Coq.FSets.FMapFacts]
p:626 [in Coq.FSets.FMapFacts]
p:627 [in Coq.FSets.FMapFacts]
p:627 [in Coq.Init.Specif]
p:628 [in Coq.FSets.FMapFacts]
P:629 [in Coq.Init.Specif]
p:63 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:63 [in Coq.Numbers.Integer.Abstract.ZAdd]
P:63 [in Coq.Logic.JMeq]
p:63 [in Coq.ZArith.Int]
p:63 [in Coq.Numbers.DecimalPos]
P:63 [in Coq.Logic.WKL]
p:63 [in Coq.QArith.QArith_base]
P:637 [in Coq.Init.Specif]
p:64 [in Coq.PArith.BinPos]
p:64 [in Coq.btauto.Algebra]
p:64 [in Coq.Logic.JMeq]
p:64 [in Coq.Numbers.Natural.Abstract.NLcm]
p:64 [in Coq.FSets.FMapInterface]
p:64 [in Coq.rtauto.Bintree]
p:64 [in Coq.Structures.GenericMinMax]
P:64 [in Coq.Logic.WKL]
p:64 [in Coq.PArith.BinPosDef]
p:64 [in Coq.Reals.Cos_rel]
P:643 [in Coq.ssr.ssrbool]
P:645 [in Coq.Init.Specif]
p:648 [in Coq.Init.Specif]
P:648 [in Coq.ssr.ssrbool]
P:65 [in Coq.Lists.Streams]
p:65 [in Coq.Numbers.Natural.Abstract.NSub]
p:65 [in Coq.Numbers.Integer.Abstract.ZGcd]
P:65 [in Coq.setoid_ring.Ring_polynom]
p:65 [in Coq.Numbers.NaryFunctions]
P:65 [in Coq.Reals.Rsqrt_def]
p:65 [in Coq.Numbers.NatInt.NZGcd]
p:65 [in Coq.ZArith.Int]
p:65 [in Coq.ZArith.Zpower]
p:65 [in Coq.Numbers.DecimalPos]
p:65 [in Coq.Numbers.NatInt.NZMulOrder]
p:65 [in Coq.QArith.QArith_base]
P:65 [in Coq.rtauto.Rtauto]
p:656 [in Coq.Init.Specif]
P:656 [in Coq.ssr.ssrbool]
P:66 [in Coq.Logic.Eqdep_dec]
P:66 [in Coq.FSets.FSetBridge]
p:66 [in Coq.Numbers.Integer.Abstract.ZAdd]
P:66 [in Coq.Logic.EqdepFacts]
p:66 [in Coq.PArith.BinPos]
P:66 [in Coq.Arith.Wf_nat]
p:66 [in Coq.Reals.Exp_prop]
P:66 [in Coq.MSets.MSetWeakList]
p:66 [in Coq.NArith.Ndigits]
p:66 [in Coq.Structures.EqualitiesFacts]
p:66 [in Coq.Numbers.DecimalPos]
p:66 [in Coq.Reals.Cos_rel]
p:662 [in Coq.Init.Specif]
P:663 [in Coq.FSets.FMapFacts]
P:664 [in Coq.ssr.ssrbool]
P:667 [in Coq.Init.Specif]
p:67 [in Coq.Vectors.VectorSpec]
p:67 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:67 [in Coq.Logic.Eqdep_dec]
p:67 [in Coq.Numbers.Natural.Abstract.NDiv]
p:67 [in Coq.Logic.EqdepFacts]
p:67 [in Coq.Numbers.HexadecimalPos]
p:67 [in Coq.Numbers.NaryFunctions]
P:67 [in Coq.micromega.EnvRing]
p:67 [in Coq.Numbers.Integer.Abstract.ZLcm]
p:67 [in Coq.NArith.Ndigits]
p:67 [in Coq.Structures.GenericMinMax]
P:67 [in Coq.Logic.Diaconescu]
p:67 [in Coq.QArith.QArith_base]
P:670 [in Coq.FSets.FMapFacts]
p:671 [in Coq.Init.Specif]
p:672 [in Coq.Init.Specif]
p:677 [in Coq.Init.Specif]
p:678 [in Coq.Init.Specif]
P:68 [in Coq.Lists.Streams]
p:68 [in Coq.Numbers.Natural.Abstract.NSub]
p:68 [in Coq.PArith.BinPos]
p:68 [in Coq.Numbers.Integer.Abstract.ZGcd]
p:68 [in Coq.Numbers.NatInt.NZGcd]
P:68 [in Coq.Logic.WKL]
P:69 [in Coq.PArith.BinPos]
p:69 [in Coq.Numbers.HexadecimalPos]
P:69 [in Coq.MSets.MSetProperties]
p:69 [in Coq.PArith.Pnat]
p:69 [in Coq.Arith.Wf_nat]
p:69 [in Coq.Reals.Exp_prop]
P:69 [in Coq.Logic.JMeq]
P:69 [in Coq.MSets.MSetWeakList]
p:69 [in Coq.Reals.Rtrigo_alt]
p:69 [in Coq.ZArith.Zpower]
p:69 [in Coq.Numbers.DecimalPos]
P:69 [in Coq.FSets.FSetProperties]
p:69 [in Coq.QArith.QArith_base]
P:693 [in Coq.FSets.FMapFacts]
p:7 [in Coq.setoid_ring.BinList]
P:7 [in Coq.Logic.Epsilon]
p:7 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
P:7 [in Coq.Logic.ClassicalEpsilon]
p:7 [in Coq.PArith.Pnat]
p:7 [in Coq.ZArith.Zmin]
P:7 [in Coq.btauto.Algebra]
P:7 [in Coq.Reals.Rsqrt_def]
P:7 [in Coq.Init.Specif]
P:7 [in Coq.Logic.IndefiniteDescription]
p:7 [in Coq.Numbers.Natural.Abstract.NMulOrder]
P:7 [in Coq.Logic.Berardi]
p:7 [in Coq.Logic.HLevels]
P:7 [in Coq.Logic.Classical_Prop]
p:7 [in Coq.Numbers.Integer.Abstract.ZMulOrder]
P:7 [in Coq.Classes.DecidableClass]
P:7 [in Coq.ZArith.Zcomplements]
p:7 [in Coq.QArith.Qpower]
p:7 [in Coq.micromega.VarMap]
p:7 [in Coq.QArith.Qreduction]
p:7 [in Coq.ZArith.Zcompare]
p:70 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
P:70 [in Coq.FSets.FSetBridge]
p:70 [in Coq.Numbers.HexadecimalPos]
P:70 [in Coq.Arith.Wf_nat]
p:70 [in Coq.Logic.JMeq]
p:70 [in Coq.Numbers.Integer.Abstract.ZLcm]
p:70 [in Coq.setoid_ring.Ncring_tac]
p:70 [in Coq.Structures.GenericMinMax]
P:70 [in Coq.setoid_ring.Ncring_polynom]
P:70 [in Coq.Logic.WKL]
P:703 [in Coq.FSets.FMapFacts]
P:709 [in Coq.MSets.MSetRBT]
p:71 [in Coq.PArith.BinPos]
p:71 [in Coq.Numbers.NatInt.NZAddOrder]
p:71 [in Coq.Numbers.Integer.Abstract.ZGcd]
P:71 [in Coq.setoid_ring.Ring_polynom]
p:71 [in Coq.Reals.Rbasic_fun]
p:71 [in Coq.Structures.EqualitiesFacts]
P:71 [in Coq.Logic.Diaconescu]
P:71 [in Coq.Init.Logic]
p:71 [in Coq.QArith.QArith_base]
P:711 [in Coq.MSets.MSetRBT]
p:72 [in Coq.Logic.Eqdep_dec]
P:72 [in Coq.Logic.EqdepFacts]
P:72 [in Coq.Reals.MVT]
p:72 [in Coq.Reals.Rtrigo_alt]
P:72 [in Coq.Classes.CMorphisms]
p:72 [in Coq.ZArith.Zpower]
P:72 [in Coq.setoid_ring.Ncring_polynom]
p:72 [in Coq.btauto.Reflect]
p:72 [in Coq.rtauto.Rtauto]
p:73 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:73 [in Coq.Numbers.Natural.Abstract.NSub]
p:73 [in Coq.PArith.BinPos]
p:73 [in Coq.Numbers.HexadecimalPos]
p:73 [in Coq.PArith.Pnat]
p:73 [in Coq.Arith.Wf_nat]
P:73 [in Coq.micromega.EnvRing]
p:73 [in Coq.Structures.GenericMinMax]
p:73 [in Coq.PArith.BinPosDef]
p:73 [in Coq.QArith.QArith_base]
p:74 [in Coq.Numbers.Integer.Abstract.ZGcd]
P:74 [in Coq.Arith.Wf_nat]
p:74 [in Coq.Numbers.Integer.Abstract.ZLcm]
p:74 [in Coq.Numbers.NatInt.NZGcd]
p:74 [in Coq.ZArith.Zpower]
p:75 [in Coq.PArith.BinPos]
p:75 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
P:75 [in Coq.Logic.JMeq]
P:75 [in Coq.Reals.Rsqrt_def]
p:75 [in Coq.Reals.Rtrigo_alt]
P:75 [in Coq.Init.Logic]
p:75 [in Coq.PArith.BinPosDef]
p:76 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:76 [in Coq.Numbers.Natural.Abstract.NSub]
P:76 [in Coq.setoid_ring.Ring_polynom]
p:76 [in Coq.PArith.Pnat]
p:76 [in Coq.Reals.Exp_prop]
p:76 [in Coq.btauto.Algebra]
p:76 [in Coq.Logic.JMeq]
p:76 [in Coq.NArith.BinNat]
p:76 [in Coq.Structures.GenericMinMax]
P:76 [in Coq.setoid_ring.Ncring_polynom]
p:76 [in Coq.Reals.Cos_plus]
p:77 [in Coq.QArith.Qcanon]
p:77 [in Coq.PArith.BinPos]
P:77 [in Coq.Init.Specif]
p:77 [in Coq.Reals.Abstract.ConstructiveLimits]
p:77 [in Coq.PArith.BinPosDef]
p:78 [in Coq.PArith.Pnat]
P:78 [in Coq.Arith.Wf_nat]
P:78 [in Coq.micromega.EnvRing]
p:78 [in Coq.Numbers.Integer.Abstract.ZLcm]
p:78 [in Coq.Reals.Rtrigo_alt]
p:78 [in Coq.Reals.Cos_rel]
p:79 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:79 [in Coq.Numbers.Natural.Abstract.NSub]
P:79 [in Coq.Logic.Eqdep_dec]
P:79 [in Coq.Logic.EqdepFacts]
p:79 [in Coq.Reals.Exp_prop]
p:79 [in Coq.NArith.BinNat]
p:79 [in Coq.Structures.GenericMinMax]
p:79 [in Coq.Reals.Cos_plus]
p:8 [in Coq.Arith.Minus]
P:8 [in Coq.Arith.Le]
p:8 [in Coq.Logic.EqdepFacts]
p:8 [in Coq.Floats.FloatLemmas]
p:8 [in Coq.PArith.Pnat]
p:8 [in Coq.ZArith.Zmin]
P:8 [in Coq.ZArith.Wf_Z]
p:8 [in Coq.Numbers.Natural.Abstract.NAddOrder]
p:8 [in Coq.Arith.Plus]
P:8 [in Coq.Reals.Rbasic_fun]
p:8 [in Coq.Numbers.NatInt.NZMul]
P:8 [in Coq.Vectors.VectorDef]
p:80 [in Coq.Logic.Eqdep_dec]
P:80 [in Coq.PArith.BinPos]
P:80 [in Coq.setoid_ring.Ring_polynom]
p:80 [in Coq.PArith.Pnat]
p:80 [in Coq.ZArith.Zpower]
p:80 [in Coq.Reals.Cos_rel]
p:81 [in Coq.Strings.String]
p:81 [in Coq.Arith.Wf_nat]
p:81 [in Coq.btauto.Algebra]
P:81 [in Coq.Logic.FunctionalExtensionality]
P:81 [in Coq.ssr.ssrbool]
p:81 [in Coq.Numbers.NatInt.NZDiv]
P:81 [in Coq.Logic.ClassicalFacts]
p:81 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
p:82 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:82 [in Coq.Numbers.Natural.Abstract.NSub]
p:82 [in Coq.PArith.BinPos]
p:82 [in Coq.PArith.Pnat]
P:82 [in Coq.Arith.Wf_nat]
p:82 [in Coq.Reals.Exp_prop]
P:82 [in Coq.micromega.EnvRing]
p:82 [in Coq.setoid_ring.Ncring_tac]
p:82 [in Coq.ZArith.Zpower]
p:82 [in Coq.Structures.GenericMinMax]
p:82 [in Coq.Init.Datatypes]
P:82 [in Coq.setoid_ring.Ncring_polynom]
p:82 [in Coq.Reals.Cos_rel]
p:83 [in Coq.Numbers.Cyclic.Int63.Int63]
p:83 [in Coq.Init.Specif]
p:84 [in Coq.PArith.BinPos]
p:84 [in Coq.PArith.Pnat]
p:84 [in Coq.ZArith.Zorder]
P:84 [in Coq.setoid_ring.Ncring_polynom]
p:84 [in Coq.Reals.Cos_rel]
p:85 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
P:85 [in Coq.PArith.BinPos]
p:85 [in Coq.Arith.Wf_nat]
p:85 [in Coq.Reals.Exp_prop]
P:85 [in Coq.Reals.Rsqrt_def]
P:85 [in Coq.ssr.ssrbool]
p:85 [in Coq.micromega.OrderedRing]
p:85 [in Coq.Structures.GenericMinMax]
P:85 [in Coq.Init.Datatypes]
P:86 [in Coq.Logic.EqdepFacts]
P:86 [in Coq.setoid_ring.Ring_polynom]
p:86 [in Coq.PArith.Pnat]
P:86 [in Coq.Arith.Wf_nat]
p:86 [in Coq.Numbers.Cyclic.Int63.Int63]
p:86 [in Coq.Arith.PeanoNat]
p:86 [in Coq.ZArith.Zpower]
p:86 [in Coq.ZArith.Zorder]
P:86 [in Coq.Init.Logic]
p:87 [in Coq.Program.Wf]
p:87 [in Coq.Numbers.Integer.Abstract.ZAdd]
p:87 [in Coq.PArith.BinPos]
p:87 [in Coq.Numbers.NaryFunctions]
P:87 [in Coq.ssr.ssrbool]
p:87 [in Coq.ZArith.Zorder]
p:87 [in Coq.Vectors.VectorDef]
p:88 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:88 [in Coq.PArith.Pnat]
P:88 [in Coq.micromega.EnvRing]
P:88 [in Coq.omega.OmegaLemmas]
p:88 [in Coq.ZArith.Zorder]
p:88 [in Coq.Structures.GenericMinMax]
p:88 [in Coq.PArith.BinPosDef]
p:89 [in Coq.Vectors.VectorSpec]
P:89 [in Coq.PArith.BinPos]
p:89 [in Coq.Numbers.NaryFunctions]
P:89 [in Coq.Reals.Rsqrt_def]
p:89 [in Coq.MSets.MSetRBT]
p:89 [in Coq.Vectors.Fin]
P:89 [in Coq.setoid_ring.Ncring_polynom]
p:9 [in Coq.Numbers.Natural.Abstract.NSub]
p:9 [in Coq.Numbers.NatInt.NZAddOrder]
p:9 [in Coq.QArith.Qminmax]
p:9 [in Coq.NArith.BinNat]
P:9 [in Coq.Program.Equality]
p:9 [in Coq.omega.OmegaLemmas]
p:9 [in Coq.ZArith.Zpower]
p:9 [in Coq.ZArith.Zpow_alt]
P:9 [in Coq.Logic.Classical_Prop]
P:9 [in Coq.Classes.DecidableClass]
P:9 [in Coq.Logic.WKL]
p:9 [in Coq.Numbers.Natural.Abstract.NGcd]
p:9 [in Coq.QArith.Qpower]
P:9 [in Coq.Init.Tactics]
P:9 [in Coq.FSets.FSetCompat]
p:90 [in Coq.Numbers.Integer.Abstract.ZAdd]
P:90 [in Coq.PArith.BinPos]
p:90 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
p:90 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
P:90 [in Coq.Arith.Wf_nat]
p:90 [in Coq.btauto.Algebra]
P:90 [in Coq.Logic.FunctionalExtensionality]
P:90 [in Coq.Sorting.Permutation]
p:91 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:91 [in Coq.Numbers.Natural.Abstract.NSub]
P:91 [in Coq.PArith.BinPos]
p:91 [in Coq.PArith.Pnat]
P:91 [in Coq.Sorting.Permutation]
p:91 [in Coq.micromega.OrderedRing]
p:91 [in Coq.Structures.GenericMinMax]
p:91 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
p:92 [in Coq.Numbers.Natural.Abstract.NSub]
p:92 [in Coq.PArith.BinPos]
P:92 [in Coq.setoid_ring.Ring_polynom]
P:92 [in Coq.Sorting.Permutation]
p:92 [in Coq.omega.OmegaLemmas]
p:92 [in Coq.NArith.Ndigits]
P:92 [in Coq.Init.Logic]
p:92 [in Coq.PArith.BinPosDef]
p:93 [in Coq.Vectors.VectorSpec]
p:93 [in Coq.Numbers.Integer.Abstract.ZAdd]
P:93 [in Coq.Logic.EqdepFacts]
P:93 [in Coq.ssr.ssrbool]
P:93 [in Coq.omega.OmegaLemmas]
P:94 [in Coq.ZArith.BinInt]
p:94 [in Coq.PArith.Pnat]
P:94 [in Coq.Arith.Wf_nat]
P:94 [in Coq.micromega.EnvRing]
p:94 [in Coq.btauto.Algebra]
P:94 [in Coq.Logic.ChoiceFacts]
P:94 [in Coq.Init.Specif]
p:94 [in Coq.ZArith.Zorder]
P:94 [in Coq.Sorting.CPermutation]
p:94 [in Coq.Structures.GenericMinMax]
P:941 [in Coq.Lists.List]
P:945 [in Coq.Lists.List]
P:949 [in Coq.Lists.List]
p:95 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
P:95 [in Coq.ssr.ssrbool]
p:95 [in Coq.Arith.PeanoNat]
p:95 [in Coq.NArith.Ndigits]
P:95 [in Coq.setoid_ring.Ncring_polynom]
p:95 [in Coq.PArith.BinPosDef]
P:953 [in Coq.Lists.List]
P:957 [in Coq.Lists.List]
p:96 [in Coq.Reals.Abstract.ConstructiveReals]
p:96 [in Coq.Numbers.Integer.Abstract.ZAdd]
p:96 [in Coq.PArith.BinPos]
P:96 [in Coq.MSets.MSetProperties]
P:96 [in Coq.setoid_ring.Ring_polynom]
p:96 [in Coq.PArith.Pnat]
p:96 [in Coq.Numbers.Cyclic.Int31.Int31]
P:96 [in Coq.Sorting.CPermutation]
p:96 [in Coq.PArith.BinPosDef]
P:96 [in Coq.FSets.FSetProperties]
P:961 [in Coq.Lists.List]
P:965 [in Coq.Lists.List]
P:968 [in Coq.Lists.List]
p:97 [in Coq.PArith.BinPos]
p:97 [in Coq.PArith.Pnat]
P:97 [in Coq.Logic.ChoiceFacts]
P:97 [in Coq.Init.Specif]
P:97 [in Coq.ssr.ssrbool]
P:97 [in Coq.Sorting.Permutation]
p:97 [in Coq.omega.OmegaLemmas]
p:97 [in Coq.ZArith.Zorder]
p:97 [in Coq.Vectors.Fin]
p:97 [in Coq.Structures.GenericMinMax]
p:97 [in Coq.Reals.Abstract.ConstructiveMinMax]
P:972 [in Coq.Lists.List]
P:976 [in Coq.Lists.List]
P:98 [in Coq.ZArith.BinInt]
P:98 [in Coq.Arith.Wf_nat]
P:98 [in Coq.micromega.EnvRing]
P:98 [in Coq.omega.OmegaLemmas]
p:98 [in Coq.NArith.Ndigits]
P:985 [in Coq.Lists.List]
p:99 [in Coq.Numbers.Integer.Abstract.ZAdd]
p:99 [in Coq.Numbers.NaryFunctions]
P:99 [in Coq.ssr.ssrbool]
P:99 [in Coq.Sorting.CPermutation]
P:99 [in Coq.Reals.Ranalysis5]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (68863 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (985 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (44709 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (761 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1497 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (570 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11380 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (976 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (603 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (298 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (460 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (476 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (811 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1157 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4018 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (162 entries) |