| 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 | (72487 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 | (1049 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 | (47021 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 | (788 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 | (1537 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 | (588 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 | (11841 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 | (1025 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 | (634 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 | (306 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 | (473 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 | (486 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 | (881 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 | (1465 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 | (4229 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 | (164 entries) |
P (binder)
PandQ:3 [in Coq.ssr.ssrfun]partition:229 [in Coq.FSets.FSetInterface]
partition:74 [in Coq.FSets.FSetBridge]
pat:212 [in Coq.micromega.Tauto]
pat:3 [in Coq.Arith.Cantor]
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:438 [in Coq.micromega.Tauto]
pat:44 [in Coq.Init.Specif]
pat:442 [in Coq.micromega.Tauto]
pat:45 [in Coq.Init.Specif]
pat:46 [in Coq.Init.Specif]
pat:9 [in Coq.Arith.Cantor]
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:122 [in Coq.Init.Datatypes]
Peq:127 [in Coq.Init.Datatypes]
Peq:132 [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:330 [in Coq.micromega.ZMicromega]
pf1:353 [in Coq.micromega.ZMicromega]
pf1:356 [in Coq.micromega.ZMicromega]
pf2:354 [in Coq.micromega.ZMicromega]
pf2:357 [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:321 [in Coq.micromega.ZMicromega]
pf:335 [in Coq.micromega.ZMicromega]
pf:338 [in Coq.micromega.ZMicromega]
pf:344 [in Coq.micromega.ZMicromega]
pf:346 [in Coq.micromega.ZMicromega]
pf:348 [in Coq.micromega.ZMicromega]
pf:350 [in Coq.micromega.ZMicromega]
Pf:600 [in Coq.ssr.ssrbool]
Pf:603 [in Coq.ssr.ssrbool]
Pgoal:115 [in Coq.ssr.ssreflect]
Pgoal:77 [in Coq.ssr.ssreflect]
Pgoal:80 [in Coq.ssr.ssreflect]
Pgoal:86 [in Coq.ssr.ssreflect]
Pgt:124 [in Coq.Init.Datatypes]
Pgt:129 [in Coq.Init.Datatypes]
Pgt:134 [in Coq.Init.Datatypes]
Phf:654 [in Coq.ssr.ssrbool]
Phf:656 [in Coq.ssr.ssrbool]
Phf:658 [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:574 [in Coq.ssr.ssrbool]
Ph:647 [in Coq.ssr.ssrbool]
Ph:648 [in Coq.ssr.ssrbool]
Ph:649 [in Coq.ssr.ssrbool]
Ph:655 [in Coq.ssr.ssrbool]
Ph:657 [in Coq.ssr.ssrbool]
Ph:659 [in Coq.ssr.ssrbool]
Ph:710 [in Coq.ssr.ssrbool]
Ph:715 [in Coq.ssr.ssrbool]
Ph:723 [in Coq.ssr.ssrbool]
Ph:731 [in Coq.ssr.ssrbool]
Plemma:114 [in Coq.ssr.ssreflect]
Plemma:76 [in Coq.ssr.ssreflect]
Plemma:81 [in Coq.ssr.ssreflect]
Plemma:85 [in Coq.ssr.ssreflect]
plow:40 [in Coq.Reals.Runcountable]
plow:48 [in Coq.Reals.Runcountable]
plow:62 [in Coq.Reals.Runcountable]
Plt:123 [in Coq.Init.Datatypes]
Plt:128 [in Coq.Init.Datatypes]
Plt:133 [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]
polarity:239 [in Coq.micromega.Tauto]
polarity:243 [in Coq.micromega.Tauto]
polarity:249 [in Coq.micromega.Tauto]
polarity:255 [in Coq.micromega.Tauto]
polarity:261 [in Coq.micromega.Tauto]
polarity:269 [in Coq.micromega.Tauto]
pol:163 [in Coq.micromega.Tauto]
pol:168 [in Coq.micromega.Tauto]
pol:172 [in Coq.micromega.Tauto]
pol:176 [in Coq.micromega.Tauto]
pol:180 [in Coq.micromega.Tauto]
pol:195 [in Coq.micromega.Tauto]
pol:329 [in Coq.micromega.Tauto]
pol:333 [in Coq.micromega.Tauto]
pol:337 [in Coq.micromega.Tauto]
pol:341 [in Coq.micromega.Tauto]
pol:356 [in Coq.micromega.Tauto]
pol:360 [in Coq.micromega.Tauto]
pol:363 [in Coq.micromega.Tauto]
pol:378 [in Coq.micromega.Tauto]
pol:382 [in Coq.micromega.Tauto]
pol:401 [in Coq.micromega.Tauto]
pol:409 [in Coq.micromega.Tauto]
pol:413 [in Coq.micromega.Tauto]
pol:415 [in Coq.micromega.Tauto]
pol:417 [in Coq.micromega.Tauto]
pol:420 [in Coq.micromega.Tauto]
pol:422 [in Coq.micromega.Tauto]
pol:424 [in Coq.micromega.Tauto]
pol:427 [in Coq.micromega.Tauto]
pol:461 [in Coq.micromega.Tauto]
pol:463 [in Coq.micromega.Tauto]
pol:465 [in Coq.micromega.Tauto]
pol:471 [in Coq.micromega.Tauto]
pol:473 [in Coq.micromega.Tauto]
pol:475 [in Coq.micromega.Tauto]
pol:481 [in Coq.micromega.Tauto]
pol:483 [in Coq.micromega.Tauto]
pol:485 [in Coq.micromega.Tauto]
pol:491 [in Coq.micromega.Tauto]
pol:493 [in Coq.micromega.Tauto]
pol:495 [in Coq.micromega.Tauto]
pol:500 [in Coq.micromega.Tauto]
pol:591 [in Coq.micromega.Tauto]
pol:594 [in Coq.micromega.Tauto]
pol:597 [in Coq.micromega.Tauto]
pol:607 [in Coq.micromega.Tauto]
pol:610 [in Coq.micromega.Tauto]
pol:613 [in Coq.micromega.Tauto]
pol:617 [in Coq.micromega.Tauto]
post:329 [in Coq.micromega.ZMicromega]
posz:328 [in Coq.micromega.ZMicromega]
pos:191 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
PP':115 [in Coq.setoid_ring.Ring_polynom]
PP':117 [in Coq.micromega.EnvRing]
pp:426 [in Coq.ssr.ssrbool]
pp:429 [in Coq.ssr.ssrbool]
pqr:1004 [in Coq.Init.Specif]
pqr:583 [in Coq.Init.Specif]
pqr:593 [in Coq.Init.Specif]
pqr:707 [in Coq.Init.Logic]
pqr:717 [in Coq.Init.Logic]
pqr:742 [in Coq.Init.Specif]
pqr:845 [in Coq.Init.Specif]
pqr:855 [in Coq.Init.Specif]
pqr:909 [in Coq.Init.Logic]
PQ':113 [in Coq.setoid_ring.Ring_polynom]
PQ':115 [in Coq.micromega.EnvRing]
pq:169 [in Coq.Init.Specif]
pq:176 [in Coq.Init.Specif]
pq:322 [in Coq.Init.Specif]
pq:386 [in Coq.Init.Specif]
pq:393 [in Coq.Init.Specif]
pq:477 [in Coq.Init.Logic]
pq:484 [in Coq.Init.Logic]
pq:485 [in Coq.Init.Specif]
pq:582 [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:313 [in Coq.Reals.Ranalysis5]
prf:319 [in Coq.micromega.ZMicromega]
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:112 [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:396 [in Coq.Reals.Ranalysis1]
pr:41 [in Coq.Reals.SeqProp]
pr:433 [in Coq.Reals.RiemannInt]
pr:433 [in Coq.micromega.ZMicromega]
pr:435 [in Coq.micromega.ZMicromega]
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':282 [in Coq.ssr.ssrbool]
pT:280 [in Coq.ssr.ssrbool]
pT:377 [in Coq.ssr.ssrbool]
pT:425 [in Coq.ssr.ssrbool]
pT:427 [in Coq.ssr.ssrbool]
pt:450 [in Coq.micromega.ZMicromega]
pt:454 [in Coq.micromega.ZMicromega]
P_hprop:523 [in Coq.Init.Specif]
P_hprop:507 [in Coq.Init.Specif]
P_hprop:344 [in Coq.Init.Specif]
P_hprop:251 [in Coq.Init.Specif]
P_hprop:799 [in Coq.Init.Logic]
P_hprop:631 [in Coq.Init.Logic]
P_hprop:614 [in Coq.Init.Logic]
P_hprop:604 [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':188 [in Coq.Init.Specif]
P':197 [in Coq.micromega.EnvRing]
p':2 [in Coq.NArith.Ndec]
P':200 [in Coq.micromega.EnvRing]
p':209 [in Coq.Init.Specif]
P':210 [in Coq.setoid_ring.Ring_polynom]
P':212 [in Coq.setoid_ring.Ring_polynom]
p':218 [in Coq.Init.Specif]
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':286 [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':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':8 [in Coq.Logic.ClassicalChoice]
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:447 [in Coq.Init.Logic]
P0:453 [in Coq.Init.Logic]
P0:650 [in Coq.Init.Logic]
P0:657 [in Coq.Init.Logic]
p1:103 [in Coq.Vectors.VectorSpec]
p1:104 [in Coq.micromega.ZifyClasses]
p1:109 [in Coq.Vectors.VectorSpec]
p1:113 [in Coq.Logic.Eqdep_dec]
p1:113 [in Coq.setoid_ring.Field_theory]
p1:115 [in Coq.Vectors.VectorSpec]
p1:116 [in Coq.setoid_ring.Field_theory]
P1:122 [in Coq.micromega.ZifyClasses]
p1:123 [in Coq.Logic.EqdepFacts]
p1:127 [in Coq.Logic.EqdepFacts]
P1:13 [in Coq.Vectors.Fin]
P1:138 [in Coq.micromega.ZifyClasses]
P1:140 [in Coq.ssr.ssrbool]
p1:142 [in Coq.Logic.Eqdep_dec]
P1:145 [in Coq.ssr.ssrbool]
P1:149 [in Coq.micromega.ZifyClasses]
p1:15 [in Coq.micromega.Ztac]
P1:151 [in Coq.ssr.ssrbool]
p1:155 [in Coq.Vectors.VectorSpec]
P1:155 [in Coq.micromega.EnvRing]
P1:158 [in Coq.ssr.ssrbool]
p1:159 [in Coq.Logic.EqdepFacts]
P1:160 [in Coq.setoid_ring.Ring_polynom]
P1:161 [in Coq.micromega.EnvRing]
P1:163 [in Coq.ssr.ssrbool]
p1:164 [in Coq.Logic.EqdepFacts]
p1:165 [in Coq.Vectors.VectorSpec]
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: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:238 [in Coq.Logic.EqdepFacts]
p1:24 [in Coq.Vectors.VectorSpec]
p1:24 [in Coq.Logic.Eqdep_dec]
p1:257 [in Coq.ssr.ssrbool]
P1:26 [in Coq.Vectors.Fin]
p1:260 [in Coq.ssr.ssrbool]
p1:263 [in Coq.ssr.ssrbool]
p1:268 [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:291 [in Coq.ssr.ssrbool]
p1:294 [in Coq.ssr.ssrbool]
P1:296 [in Coq.setoid_ring.Ring_polynom]
p1:299 [in Coq.ssr.ssrbool]
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:42 [in Coq.Logic.Eqdep_dec]
p1:5 [in Coq.Logic.PropExtensionality]
p1:52 [in Coq.micromega.ZifyClasses]
p1:59 [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:95 [in Coq.Logic.Eqdep_dec]
p1:99 [in Coq.micromega.ZifyClasses]
p2:100 [in Coq.micromega.ZifyClasses]
p2:104 [in Coq.Vectors.VectorSpec]
p2:110 [in Coq.Vectors.VectorSpec]
p2:114 [in Coq.Logic.Eqdep_dec]
p2:114 [in Coq.setoid_ring.Field_theory]
P2:115 [in Coq.setoid_ring.Ncring_polynom]
p2:116 [in Coq.Vectors.VectorSpec]
p2:117 [in Coq.setoid_ring.Field_theory]
P2:123 [in Coq.micromega.EnvRing]
p2:124 [in Coq.Logic.EqdepFacts]
P2:125 [in Coq.micromega.ZifyClasses]
P2:125 [in Coq.setoid_ring.Ncring_polynom]
P2:141 [in Coq.ssr.ssrbool]
p2:143 [in Coq.Logic.Eqdep_dec]
P2:146 [in Coq.ssr.ssrbool]
P2:152 [in Coq.micromega.ZifyClasses]
P2:152 [in Coq.ssr.ssrbool]
p2:156 [in Coq.Vectors.VectorSpec]
P2:157 [in Coq.micromega.EnvRing]
P2:159 [in Coq.ssr.ssrbool]
p2:16 [in Coq.micromega.Ztac]
P2:162 [in Coq.setoid_ring.Ring_polynom]
P2:163 [in Coq.micromega.EnvRing]
P2:164 [in Coq.ssr.ssrbool]
p2:166 [in Coq.Vectors.VectorSpec]
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: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:239 [in Coq.Logic.EqdepFacts]
p2:25 [in Coq.Vectors.VectorSpec]
p2:25 [in Coq.Logic.Eqdep_dec]
p2:258 [in Coq.ssr.ssrbool]
p2:261 [in Coq.ssr.ssrbool]
p2:264 [in Coq.ssr.ssrbool]
p2:269 [in Coq.ssr.ssrbool]
P2:287 [in Coq.setoid_ring.Ring_polynom]
p2:292 [in Coq.ssr.ssrbool]
P2:293 [in Coq.setoid_ring.Ring_polynom]
p2:295 [in Coq.ssr.ssrbool]
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:300 [in Coq.ssr.ssrbool]
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:43 [in Coq.Logic.Eqdep_dec]
p2:53 [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:96 [in Coq.Logic.Eqdep_dec]
P3:142 [in Coq.ssr.ssrbool]
P3:147 [in Coq.ssr.ssrbool]
P3:153 [in Coq.ssr.ssrbool]
P3:160 [in Coq.ssr.ssrbool]
P3:165 [in Coq.ssr.ssrbool]
p3:167 [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:148 [in Coq.ssr.ssrbool]
P4:154 [in Coq.ssr.ssrbool]
P4:166 [in Coq.ssr.ssrbool]
P5:155 [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.QArith.Qreals]
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.Reals.Cauchy.PosExtra]
p:1 [in Coq.Reals.Cauchy.QExtra]
p:1 [in Coq.NArith.Ndec]
P:1 [in Coq.Logic.WeakFan]
p:10 [in Coq.Arith.Le]
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.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.Reals.Cauchy.ConstructiveExtra]
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.EqdepFacts]
p:100 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p:100 [in Coq.PArith.Pnat]
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:1002 [in Coq.Lists.List]
p:1002 [in Coq.Init.Specif]
p:1003 [in Coq.Init.Specif]
P:1006 [in Coq.Lists.List]
p:1006 [in Coq.Init.Specif]
p:1007 [in Coq.Init.Specif]
P:101 [in Coq.setoid_ring.Ring_polynom]
p:101 [in Coq.PArith.Pnat]
P:101 [in Coq.Logic.FunctionalExtensionality]
p:101 [in Coq.ZArith.Znat]
P:1010 [in Coq.Lists.List]
P:1011 [in Coq.Init.Specif]
P:1019 [in Coq.Init.Specif]
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.ZArith.Znat]
P:1020 [in Coq.Lists.List]
P:1024 [in Coq.Lists.List]
P:1027 [in Coq.Init.Specif]
P:1028 [in Coq.Lists.List]
p:103 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:103 [in Coq.Logic.Eqdep_dec]
P:103 [in Coq.micromega.EnvRing]
p:103 [in Coq.btauto.Algebra]
p:103 [in Coq.Numbers.Integer.Abstract.ZLcm]
P:103 [in Coq.ssr.ssrbool]
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:103 [in Coq.Init.Logic]
p:1030 [in Coq.Init.Specif]
P:1035 [in Coq.Lists.List]
p:1038 [in Coq.Init.Specif]
P:1039 [in Coq.Lists.List]
P:104 [in Coq.MSets.MSetInterface]
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:1043 [in Coq.Lists.List]
p:1044 [in Coq.Init.Specif]
P:1049 [in Coq.Lists.List]
P:1049 [in Coq.Init.Specif]
p:105 [in Coq.Reals.Cauchy_prod]
P:105 [in Coq.setoid_ring.Ring_polynom]
p:105 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
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.Numbers.Integer.Abstract.ZDivTrunc]
p:105 [in Coq.ZArith.Int]
p:105 [in Coq.Structures.GenericMinMax]
p:105 [in Coq.Reals.Abstract.ConstructiveMinMax]
p:1053 [in Coq.Init.Specif]
p:1054 [in Coq.Init.Specif]
p:1059 [in Coq.Init.Specif]
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:1060 [in Coq.Init.Specif]
p:107 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
P:107 [in Coq.MSets.MSetInterface]
P:107 [in Coq.Logic.Eqdep_dec]
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:108 [in Coq.Reals.Cauchy_prod]
p:108 [in Coq.Logic.Eqdep_dec]
p:108 [in Coq.Reals.Rtrigo1]
p:108 [in Coq.Arith.Wf_nat]
p:108 [in Coq.btauto.Algebra]
P:108 [in Coq.Init.Specif]
p:108 [in Coq.setoid_ring.Field_theory]
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.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.Arith.Cantor]
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:110 [in Coq.Reals.Rtrigo1]
P:110 [in Coq.PArith.BinPos]
p:110 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p:110 [in Coq.Arith.Wf_nat]
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.Init.Specif]
p:111 [in Coq.setoid_ring.Field_theory]
p:111 [in Coq.ZArith.Int]
p:111 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
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.omega.OmegaLemmas]
p:112 [in Coq.ZArith.Zorder]
P:113 [in Coq.Arith.Wf_nat]
p:113 [in Coq.btauto.Algebra]
P:113 [in Coq.Logic.ChoiceFacts]
p:113 [in Coq.Init.Nat]
p:113 [in Coq.ZArith.Int]
p:113 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
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.EqdepFacts]
P:115 [in Coq.ssr.ssrbool]
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.Arith.Wf_nat]
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.ssr.ssrbool]
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.Init.Specif]
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.Logic.Eqdep_dec]
p:119 [in Coq.Logic.EqdepFacts]
P:119 [in Coq.PArith.BinPos]
p:119 [in Coq.setoid_ring.Field_theory]
P:119 [in Coq.ssr.ssrbool]
p:119 [in Coq.ZArith.Zdiv]
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.Reals.MVT]
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.Logic.StrictProp]
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.Logic.Eqdep_dec]
p:120 [in Coq.PArith.BinPos]
P:120 [in Coq.ssr.ssreflect]
p:120 [in Coq.Reals.Rbasic_fun]
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.ssr.ssrbool]
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.Vectors.VectorSpec]
p:123 [in Coq.PArith.BinPos]
P:123 [in Coq.ssr.ssrbool]
p:123 [in Coq.PArith.BinPosDef]
p:123 [in Coq.Relations.Relation_Operators]
P:124 [in Coq.Logic.Eqdep_dec]
p:124 [in Coq.ZArith.BinInt]
p:124 [in Coq.Arith.Wf_nat]
p:124 [in Coq.btauto.Algebra]
p:124 [in Coq.FSets.FMapInterface]
p:124 [in Coq.Init.Specif]
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:126 [in Coq.Program.Wf]
p:126 [in Coq.Logic.Eqdep_dec]
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.ssr.ssrbool]
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.EqdepFacts]
P:129 [in Coq.ssr.ssrbool]
p:129 [in Coq.Structures.OrderedType]
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.Arith.Cantor]
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.QArith.QArith_base]
P:13 [in Coq.Logic.WeakFan]
p:130 [in Coq.PArith.BinPos]
P:130 [in Coq.Init.Specif]
P:130 [in Coq.ssr.ssrbool]
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.ssr.ssrbool]
p:131 [in Coq.NArith.Ndigits]
P:131 [in Coq.setoid_ring.Ncring_polynom]
p:132 [in Coq.Logic.Eqdep_dec]
P:132 [in Coq.Logic.EqdepFacts]
p:132 [in Coq.PArith.BinPos]
P:132 [in Coq.ssr.ssreflect]
p:132 [in Coq.ZArith.Znat]
p:132 [in Coq.setoid_ring.Ncring]
p:133 [in Coq.Logic.EqdepFacts]
p:133 [in Coq.PArith.BinPos]
P:133 [in Coq.ssr.ssrbool]
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.PArith.BinPosDef]
p:133 [in Coq.setoid_ring.Ncring]
p:134 [in Coq.Init.Specif]
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.ssr.ssrbool]
p:135 [in Coq.setoid_ring.Ncring]
p:135 [in Coq.ZArith.Znumtheory]
P:136 [in Coq.Logic.Eqdep_dec]
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.Init.Logic]
p:137 [in Coq.Logic.Eqdep_dec]
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:138 [in Coq.ssr.ssrbool]
p:138 [in Coq.Vectors.Fin]
p:138 [in Coq.FSets.FMapPositive]
p:138 [in Coq.PArith.BinPosDef]
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: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:140 [in Coq.Init.Logic]
p:140 [in Coq.ZArith.Znumtheory]
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.PArith.BinPos]
P:142 [in Coq.Init.Specif]
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:143 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
p:143 [in Coq.PArith.BinPosDef]
p:144 [in Coq.Reals.Cauchy_prod]
P:144 [in Coq.Reals.Rfunctions]
P:144 [in Coq.Init.Logic]
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.EqdepFacts]
P:146 [in Coq.Arith.Wf_nat]
P:146 [in Coq.Init.Specif]
P:146 [in Coq.omega.OmegaLemmas]
p:146 [in Coq.ZArith.Znumtheory]
p:147 [in Coq.Reals.Cauchy_prod]
P:147 [in Coq.Logic.Eqdep_dec]
p:147 [in Coq.ZArith.BinInt]
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.Init.Logic]
p:148 [in Coq.PArith.BinPosDef]
P:149 [in Coq.Logic.Eqdep_dec]
p:149 [in Coq.Logic.EqdepFacts]
P:149 [in Coq.Arith.Wf_nat]
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.Arith.Cantor]
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.Classes.DecidableClass]
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.EqdepFacts]
p:150 [in Coq.PArith.BinPos]
p:150 [in Coq.btauto.Algebra]
P:150 [in Coq.Init.Specif]
p:150 [in Coq.ZArith.Znumtheory]
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: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.Eqdep_dec]
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.Eqdep_dec]
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.PArith.BinPos]
P:155 [in Coq.omega.OmegaLemmas]
p:155 [in Coq.ZArith.Znumtheory]
p:155 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:156 [in Coq.Reals.Cauchy_prod]
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.omega.OmegaLemmas]
P:158 [in Coq.setoid_ring.Ncring_polynom]
p:158 [in Coq.QArith.QArith_base]
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.Vectors.VectorSpec]
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.Arith.Cantor]
p:16 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
p:16 [in Coq.setoid_ring.Ring_theory]
P:160 [in Coq.Logic.Eqdep_dec]
p:160 [in Coq.PArith.BinPos]
p:160 [in Coq.ZArith.Zorder]
p:160 [in Coq.Structures.GenericMinMax]
p:160 [in Coq.PArith.BinPosDef]
p:160 [in Coq.ZArith.Znumtheory]
p:161 [in Coq.Logic.Eqdep_dec]
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: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.Init.Specif]
p:163 [in Coq.ZArith.Zorder]
p:163 [in Coq.Structures.GenericMinMax]
p:163 [in Coq.ZArith.Znumtheory]
P:163 [in Coq.FSets.FSetCompat]
p:164 [in Coq.Vectors.VectorDef]
P:165 [in Coq.ssr.ssrfun]
p:165 [in Coq.Vectors.Fin]
p:165 [in Coq.ZArith.Znumtheory]
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.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.Logic.EqdepFacts]
p:168 [in Coq.Init.Specif]
p:169 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:169 [in Coq.PArith.BinPos]
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.micromega.ZifyClasses]
p:171 [in Coq.PArith.BinPos]
P:171 [in Coq.Init.Specif]
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:172 [in Coq.ZArith.Znumtheory]
P:173 [in Coq.micromega.ZifyClasses]
P:173 [in Coq.Logic.EqdepFacts]
p:173 [in Coq.PArith.BinPos]
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:174 [in Coq.setoid_ring.Ncring_polynom]
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.Init.Specif]
P:175 [in Coq.omega.OmegaLemmas]
p:175 [in Coq.Vectors.Fin]
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:178 [in Coq.micromega.ZifyClasses]
P:178 [in Coq.Init.Specif]
p:179 [in Coq.Logic.EqdepFacts]
p:179 [in Coq.omega.OmegaLemmas]
P:179 [in Coq.Logic.ClassicalFacts]
P:18 [in Coq.Vectors.VectorSpec]
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.Logic.ChoiceFacts]
P:180 [in Coq.ssr.ssrbool]
P:180 [in Coq.omega.OmegaLemmas]
p:180 [in Coq.ZArith.Zorder]
p:180 [in Coq.Structures.GenericMinMax]
p:181 [in Coq.PArith.BinPos]
P:181 [in Coq.Logic.ClassicalFacts]
p:182 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:182 [in Coq.setoid_ring.Ncring_polynom]
p:182 [in Coq.Reals.PSeries_reg]
P:182 [in Coq.Init.Logic]
p:182 [in Coq.QArith.QArith_base]
p:183 [in Coq.PArith.BinPos]
P:183 [in Coq.Logic.ChoiceFacts]
p:183 [in Coq.Init.Specif]
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.ZArith.Zorder]
P:186 [in Coq.setoid_ring.Ncring_polynom]
p:187 [in Coq.PArith.BinPos]
P:187 [in Coq.Init.Specif]
P:187 [in Coq.omega.OmegaLemmas]
P:188 [in Coq.Reals.MVT]
P:188 [in Coq.setoid_ring.Ncring_polynom]
p:188 [in Coq.Reals.PSeries_reg]
P:188 [in Coq.Init.Logic]
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:19 [in Coq.QArith.QArith_base]
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.PArith.BinPos]
P:191 [in Coq.omega.OmegaLemmas]
p:191 [in Coq.Reals.PSeries_reg]
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.Vectors.VectorSpec]
P:194 [in Coq.Logic.Hurkens]
p:194 [in Coq.setoid_ring.Ncring_polynom]
p:194 [in Coq.ZArith.Znumtheory]
p:195 [in Coq.PArith.BinPos]
p:195 [in Coq.ZArith.Znumtheory]
P:196 [in Coq.setoid_ring.Ring_polynom]
P:196 [in Coq.micromega.EnvRing]
p:196 [in Coq.Init.Specif]
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.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.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:2 [in Coq.Numbers.Cyclic.Int63.Uint63]
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.Init.Specif]
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:203 [in Coq.PArith.BinPos]
P:203 [in Coq.omega.OmegaLemmas]
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:205 [in Coq.Vectors.VectorSpec]
P:205 [in Coq.Logic.EqdepFacts]
p:205 [in Coq.Reals.PSeries_reg]
p:205 [in Coq.micromega.ZMicromega]
p:206 [in Coq.Logic.EqdepFacts]
p:206 [in Coq.PArith.BinPos]
p:207 [in Coq.PArith.BinPos]
p:207 [in Coq.Init.Specif]
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: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.Logic.Classical_Prop]
p:21 [in Coq.QArith.Qpower]
p:21 [in Coq.Numbers.NatInt.NZAdd]
p:21 [in Coq.Reals.Abstract.ConstructiveMinMax]
p:21 [in Coq.QArith.Qreduction]
p:21 [in Coq.QArith.QArith_base]
p:21 [in Coq.rtauto.Rtauto]
P:211 [in Coq.setoid_ring.Ring_polynom]
p:211 [in Coq.PArith.BinPosDef]
P:212 [in Coq.Logic.EqdepFacts]
P:212 [in Coq.micromega.EnvRing]
P:212 [in Coq.Init.Specif]
p:212 [in Coq.micromega.ZMicromega]
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.ZArith.Znat]
P:215 [in Coq.micromega.EnvRing]
P:215 [in Coq.FSets.FSetInterface]
p:215 [in Coq.ZArith.Znat]
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:219 [in Coq.PArith.BinPos]
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.NatInt.NZMul]
p:22 [in Coq.Numbers.NatInt.NZMulOrder]
p:22 [in Coq.Arith.Mult]
p:22 [in Coq.Numbers.Cyclic.Int63.Sint63]
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:220 [in Coq.micromega.ZMicromega]
p:221 [in Coq.PArith.BinPos]
p:221 [in Coq.ZArith.BinInt]
p:222 [in Coq.Logic.EqdepFacts]
p:222 [in Coq.ZArith.BinInt]
P:222 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:222 [in Coq.micromega.ZMicromega]
p:223 [in Coq.ZArith.BinInt]
P:224 [in Coq.setoid_ring.Ring_polynom]
P:224 [in Coq.Init.Specif]
p:224 [in Coq.setoid_ring.Field_theory]
p:224 [in Coq.NArith.BinNat]
P:224 [in Coq.Numbers.Cyclic.Int63.Uint63]
P:225 [in Coq.FSets.FSetInterface]
p:226 [in Coq.Logic.EqdepFacts]
p:226 [in Coq.micromega.ZMicromega]
p:227 [in Coq.PArith.BinPos]
P:227 [in Coq.micromega.EnvRing]
P:227 [in Coq.Logic.ClassicalFacts]
P:228 [in Coq.setoid_ring.Ring_polynom]
p:228 [in Coq.Init.Specif]
P:228 [in Coq.Structures.GenericMinMax]
P:228 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:228 [in Coq.micromega.ZMicromega]
p:229 [in Coq.PArith.BinPos]
P:229 [in Coq.Logic.Hurkens]
p:229 [in Coq.micromega.ZMicromega]
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.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.QArith.QArith_base]
P:23 [in Coq.Logic.WeakFan]
p:230 [in Coq.Logic.EqdepFacts]
p:230 [in Coq.NArith.BinNat]
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.Vectors.VectorSpec]
P:232 [in Coq.Logic.EqdepFacts]
p:232 [in Coq.PArith.BinPos]
p:232 [in Coq.micromega.ZMicromega]
p:233 [in Coq.Logic.EqdepFacts]
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.Init.Specif]
p:236 [in Coq.NArith.BinNat]
P:236 [in Coq.Structures.GenericMinMax]
P:236 [in Coq.Logic.ClassicalFacts]
p:236 [in Coq.micromega.ZMicromega]
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.Vectors.VectorSpec]
P:238 [in Coq.Bool.Bool]
P:239 [in Coq.setoid_ring.Ring_polynom]
P:239 [in Coq.Init.Specif]
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.Numbers.NatInt.NZAdd]
p:24 [in Coq.Numbers.Cyclic.Int63.Sint63]
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.Logic.EqdepFacts]
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.Vectors.VectorSpec]
P:243 [in Coq.Logic.EqdepFacts]
p:244 [in Coq.Logic.EqdepFacts]
p:244 [in Coq.Init.Specif]
p:244 [in Coq.micromega.ZMicromega]
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.Logic.EqdepFacts]
p:247 [in Coq.PArith.BinPos]
P:247 [in Coq.Init.Specif]
P:248 [in Coq.setoid_ring.Ring_polynom]
P:248 [in Coq.micromega.EnvRing]
p:248 [in Coq.setoid_ring.Field_theory]
p:248 [in Coq.micromega.ZMicromega]
P:249 [in Coq.Vectors.VectorSpec]
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.ssr.ssreflect]
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.QArith_base]
P:25 [in Coq.Logic.WeakFan]
p:250 [in Coq.QArith.QArith_base]
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: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:254 [in Coq.QArith.QArith_base]
p:255 [in Coq.Init.Specif]
P:256 [in Coq.setoid_ring.Ring_polynom]
p:256 [in Coq.Reals.SeqProp]
P:256 [in Coq.Vectors.VectorDef]
p:256 [in Coq.QArith.QArith_base]
p:257 [in Coq.PArith.BinPos]
P:257 [in Coq.micromega.EnvRing]
P:257 [in Coq.Init.Specif]
p:257 [in Coq.NArith.BinNat]
p:257 [in Coq.micromega.ZMicromega]
p:258 [in Coq.Logic.EqdepFacts]
P:258 [in Coq.setoid_ring.Ring_polynom]
p:258 [in Coq.QArith.QArith_base]
p:259 [in Coq.setoid_ring.Ring_polynom]
p:259 [in Coq.micromega.ZMicromega]
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.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:260 [in Coq.PArith.BinPos]
P:260 [in Coq.micromega.EnvRing]
p:260 [in Coq.NArith.BinNat]
p:260 [in Coq.QArith.QArith_base]
P:261 [in Coq.Logic.EqdepFacts]
P:261 [in Coq.setoid_ring.Ring_polynom]
p:261 [in Coq.Init.Specif]
p:261 [in Coq.micromega.ZMicromega]
p:262 [in Coq.Logic.EqdepFacts]
p:262 [in Coq.PArith.BinPos]
p:262 [in Coq.ZArith.Znat]
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.FSets.FSetProperties]
P:265 [in Coq.micromega.EnvRing]
p:265 [in Coq.Logic.ChoiceFacts]
P:265 [in Coq.Vectors.VectorDef]
p:266 [in Coq.PArith.BinPos]
p:266 [in Coq.micromega.EnvRing]
p:266 [in Coq.ssr.ssrbool]
P:267 [in Coq.Logic.EqdepFacts]
p:268 [in Coq.PArith.BinPos]
P:268 [in Coq.micromega.EnvRing]
p:268 [in Coq.Init.Specif]
P:268 [in Coq.Sorting.Permutation]
p:268 [in Coq.micromega.ZMicromega]
p:269 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:269 [in Coq.Logic.EqdepFacts]
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.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.QArith.QArith_base]
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.micromega.EnvRing]
p:271 [in Coq.Init.Specif]
p:271 [in Coq.FSets.FMapPositive]
p:272 [in Coq.PArith.BinPos]
p:272 [in Coq.ssr.ssrbool]
p:273 [in Coq.Logic.EqdepFacts]
p:273 [in Coq.ZArith.BinInt]
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:275 [in Coq.FSets.FMapFacts]
p:275 [in Coq.FSets.FMapPositive]
p:276 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:276 [in Coq.PArith.BinPos]
p:276 [in Coq.ZArith.BinInt]
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.Init.Specif]
p:279 [in Coq.micromega.ZMicromega]
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:280 [in Coq.PArith.BinPos]
p:281 [in Coq.ZArith.BinInt]
p:281 [in Coq.micromega.EnvRing]
p:281 [in Coq.NArith.BinNat]
p:282 [in Coq.PArith.BinPos]
p:282 [in Coq.FSets.FMapWeakList]
P:282 [in Coq.Init.Logic]
p:283 [in Coq.micromega.ZMicromega]
p:283 [in Coq.Lists.SetoidList]
p:284 [in Coq.PArith.BinPos]
p:284 [in Coq.FSets.FMapPositive]
p:285 [in Coq.Vectors.VectorSpec]
P:285 [in Coq.Init.Specif]
p:285 [in Coq.Reals.Rtopology]
p:285 [in Coq.Lists.SetoidList]
p:286 [in Coq.PArith.BinPos]
p:286 [in Coq.micromega.RingMicromega]
p:286 [in Coq.QArith.QArith_base]
p:287 [in Coq.FSets.FSetBridge]
p:287 [in Coq.ssr.ssrbool]
P:287 [in Coq.Vectors.VectorDef]
p:287 [in Coq.QArith.QArith_base]
p:288 [in Coq.PArith.BinPos]
P:288 [in Coq.FSets.FMapFacts]
p:288 [in Coq.micromega.ZMicromega]
p:288 [in Coq.Lists.SetoidList]
p:289 [in Coq.micromega.RingMicromega]
P:289 [in Coq.NArith.BinNat]
p:289 [in Coq.QArith.QArith_base]
p:29 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:29 [in Coq.QArith.Qcanon]
P:29 [in Coq.Logic.Eqdep_dec]
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.Reals.Cauchy.ConstructiveCauchyReals]
p:29 [in Coq.Numbers.DecimalPos]
p:29 [in Coq.PArith.BinPosDef]
p:29 [in Coq.ZArith.Zcompare]
p:29 [in Coq.QArith.QArith_base]
p:290 [in Coq.ZArith.BinInt]
p:290 [in Coq.Init.Specif]
p:290 [in Coq.FSets.FMapList]
p:290 [in Coq.micromega.ZMicromega]
p:290 [in Coq.Lists.SetoidList]
p:291 [in Coq.PArith.BinPos]
p:291 [in Coq.QArith.QArith_base]
p:292 [in Coq.micromega.RingMicromega]
p:292 [in Coq.Lists.SetoidList]
p:293 [in Coq.Init.Specif]
p:293 [in Coq.QArith.QArith_base]
p:294 [in Coq.PArith.BinPos]
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:297 [in Coq.ssr.ssrbool]
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.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.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.QArith.Qpower]
p:30 [in Coq.Numbers.Cyclic.Int63.Uint63]
P:30 [in Coq.Vectors.VectorDef]
p:30 [in Coq.Reals.Cos_plus]
P:300 [in Coq.Logic.ChoiceFacts]
p:300 [in Coq.Init.Specif]
p:301 [in Coq.PArith.BinPos]
p:301 [in Coq.NArith.BinNat]
p:302 [in Coq.ZArith.BinInt]
P:302 [in Coq.Logic.Hurkens]
P:302 [in Coq.Init.Logic]
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.Init.Specif]
P:305 [in Coq.Logic.Hurkens]
p:305 [in Coq.Reals.Rtopology]
p:305 [in Coq.micromega.ZMicromega]
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: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.Lists.List]
p:309 [in Coq.NArith.BinNat]
p:309 [in Coq.micromega.ZMicromega]
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.setoid_ring.Integral_domain]
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.Reals.Rtopology]
p:311 [in Coq.PArith.BinPos]
p:311 [in Coq.ZArith.BinInt]
P:311 [in Coq.FSets.FMapFacts]
p:311 [in Coq.Init.Specif]
p:312 [in Coq.ZArith.BinInt]
P:312 [in Coq.Init.Logic]
p:313 [in Coq.PArith.BinPos]
P:313 [in Coq.Lists.List]
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:316 [in Coq.Init.Specif]
p:317 [in Coq.PArith.BinPos]
P:317 [in Coq.Logic.ChoiceFacts]
p:318 [in Coq.ZArith.BinInt]
p:319 [in Coq.PArith.BinPos]
p:319 [in Coq.ZArith.BinInt]
P:319 [in Coq.NArith.BinNat]
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:321 [in Coq.PArith.BinPos]
p:321 [in Coq.ZArith.BinInt]
p:321 [in Coq.Init.Specif]
P:322 [in Coq.Init.Logic]
p:323 [in Coq.PArith.BinPos]
p:323 [in Coq.ZArith.BinInt]
P:323 [in Coq.FSets.FMapFacts]
p:324 [in Coq.Init.Specif]
p:325 [in Coq.PArith.BinPos]
p:325 [in Coq.ZArith.BinInt]
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.Vectors.VectorSpec]
p:328 [in Coq.PArith.BinPos]
p:328 [in Coq.ZArith.BinInt]
P:328 [in Coq.Init.Specif]
p:329 [in Coq.PArith.BinPos]
P:329 [in Coq.Init.Logic]
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.Logic.Eqdep_dec]
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.ssr.ssrbool]
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.ssr.ssreflect]
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.Vectors.VectorSpec]
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:333 [in Coq.PArith.BinPos]
P:333 [in Coq.Logic.ChoiceFacts]
p:334 [in Coq.ZArith.BinInt]
P:334 [in Coq.setoid_ring.Ring_polynom]
P:334 [in Coq.Logic.ChoiceFacts]
P:334 [in Coq.Init.Specif]
p:335 [in Coq.PArith.BinPos]
p:336 [in Coq.ZArith.BinInt]
p:338 [in Coq.ZArith.BinInt]
P:338 [in Coq.setoid_ring.Ring_polynom]
p:339 [in Coq.ZArith.BinInt]
P:339 [in Coq.Logic.ChoiceFacts]
p:34 [in Coq.Floats.FloatLemmas]
p:34 [in Coq.Numbers.Integer.Abstract.ZGcd]
P:34 [in Coq.Logic.Epsilon]
p:34 [in Coq.PArith.Pnat]
p:34 [in Coq.setoid_ring.Integral_domain]
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.ZArith.Zcompare]
P:340 [in Coq.Vectors.VectorSpec]
P:340 [in Coq.setoid_ring.Ring_polynom]
p:340 [in Coq.micromega.EnvRing]
P:340 [in Coq.Init.Specif]
p:341 [in Coq.ZArith.BinInt]
p:341 [in Coq.setoid_ring.Ring_polynom]
P:341 [in Coq.Logic.ChoiceFacts]
p:342 [in Coq.Init.Specif]
P:343 [in Coq.setoid_ring.Ring_polynom]
P:344 [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.micromega.EnvRing]
p:347 [in Coq.ZArith.BinInt]
P:348 [in Coq.setoid_ring.Ring_polynom]
P:348 [in Coq.micromega.EnvRing]
p:348 [in Coq.Logic.ChoiceFacts]
p:348 [in Coq.Init.Specif]
p:349 [in Coq.ZArith.BinInt]
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.ssr.ssrbool]
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: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.micromega.EnvRing]
p:352 [in Coq.micromega.ZMicromega]
p:353 [in Coq.ZArith.BinInt]
p:354 [in Coq.ZArith.BinInt]
p:354 [in Coq.setoid_ring.Ring_polynom]
P:354 [in Coq.micromega.EnvRing]
p:354 [in Coq.Init.Specif]
p:355 [in Coq.PArith.BinPos]
p:355 [in Coq.ZArith.BinInt]
p:355 [in Coq.micromega.EnvRing]
p:355 [in Coq.micromega.ZMicromega]
p:356 [in Coq.ZArith.BinInt]
P:356 [in Coq.Logic.ChoiceFacts]
p:357 [in Coq.ZArith.BinInt]
P:357 [in Coq.micromega.EnvRing]
p:358 [in Coq.PArith.BinPos]
P:358 [in Coq.micromega.EnvRing]
P:358 [in Coq.Logic.ChoiceFacts]
P:358 [in Coq.Init.Specif]
p:359 [in Coq.ZArith.BinInt]
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.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.ssr.ssreflect]
P:36 [in Coq.NArith.BinNat]
p:36 [in Coq.Program.Equality]
p:36 [in Coq.ZArith.Zpower]
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.Init.Specif]
p:361 [in Coq.Reals.Rtopology]
P:362 [in Coq.FSets.FMapFacts]
P:362 [in Coq.micromega.EnvRing]
p:362 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:363 [in Coq.Reals.Abstract.ConstructiveReals]
p:363 [in Coq.ZArith.BinInt]
P:363 [in Coq.Logic.ChoiceFacts]
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:368 [in Coq.micromega.EnvRing]
P:368 [in Coq.Init.Specif]
p:369 [in Coq.PArith.BinPos]
p:369 [in Coq.ZArith.BinInt]
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.Reals.Cauchy.ConstructiveRcomplete]
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.Arith.Gt]
p:37 [in Coq.Reals.ClassicalDedekindReals]
p:37 [in Coq.ZArith.Zcompare]
p:370 [in Coq.ZArith.BinInt]
P:370 [in Coq.setoid_ring.Ring_polynom]
p:371 [in Coq.ZArith.BinInt]
P:371 [in Coq.FSets.FMapFacts]
p:372 [in Coq.PArith.BinPos]
p:372 [in Coq.ZArith.BinInt]
p:372 [in Coq.Init.Specif]
p:372 [in Coq.micromega.ZMicromega]
p:373 [in Coq.ZArith.BinInt]
P:373 [in Coq.Init.Logic]
p:374 [in Coq.PArith.BinPos]
p:374 [in Coq.ZArith.BinInt]
P:374 [in Coq.Init.Specif]
p:375 [in Coq.ZArith.BinInt]
P:376 [in Coq.setoid_ring.Ring_polynom]
p:377 [in Coq.PArith.BinPos]
p:377 [in Coq.ZArith.BinInt]
p:378 [in Coq.Init.Specif]
p:379 [in Coq.ZArith.BinInt]
p:379 [in Coq.FSets.FMapWeakList]
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.FSets.FMapInterface]
P:38 [in Coq.ssr.ssrbool]
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.Structures.EqualitiesFacts]
p:38 [in Coq.btauto.Reflect]
p:380 [in Coq.PArith.BinPos]
P:380 [in Coq.Init.Specif]
p:381 [in Coq.ZArith.BinInt]
P:381 [in Coq.Init.Logic]
p:384 [in Coq.PArith.BinPos]
p:384 [in Coq.ZArith.BinInt]
p:385 [in Coq.Init.Specif]
p:386 [in Coq.ZArith.BinInt]
p:387 [in Coq.PArith.BinPos]
P:388 [in Coq.Init.Specif]
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.Reals.Rsqrt_def]
p:39 [in Coq.Init.Wf]
P:39 [in Coq.ssr.ssrbool]
p:39 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
p:39 [in Coq.ZArith.Zeven]
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:392 [in Coq.Init.Specif]
P:393 [in Coq.Init.Logic]
p:394 [in Coq.PArith.BinPos]
P:395 [in Coq.Init.Specif]
p:396 [in Coq.micromega.ZMicromega]
p:397 [in Coq.PArith.BinPos]
P:397 [in Coq.Init.Logic]
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:4 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:4 [in Coq.Reals.Cauchy.QExtra]
P:4 [in Coq.Reals.ClassicalDedekindReals]
p:40 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:40 [in Coq.PArith.Pnat]
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.Reals.ClassicalConstructiveReals]
P:40 [in Coq.Sorting.Heap]
p:400 [in Coq.PArith.BinPos]
p:400 [in Coq.Init.Specif]
p:403 [in Coq.PArith.BinPos]
P:403 [in Coq.Init.Specif]
P:403 [in Coq.Init.Logic]
p:406 [in Coq.PArith.BinPos]
p:407 [in Coq.Init.Specif]
p:407 [in Coq.ssr.ssrbool]
P:407 [in Coq.Init.Logic]
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.Reals.Cauchy.ConstructiveRcomplete]
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.ssr.ssrbool]
p:41 [in Coq.Arith.Plus]
p:41 [in Coq.ssr.ssreflect]
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:410 [in Coq.PArith.BinPos]
p:410 [in Coq.ZArith.BinInt]
P:410 [in Coq.Init.Specif]
p:410 [in Coq.ssr.ssrbool]
p:410 [in Coq.MSets.MSetRBT]
p:412 [in Coq.ssr.ssrbool]
p:412 [in Coq.MSets.MSetRBT]
p:413 [in Coq.PArith.BinPos]
P:413 [in Coq.Init.Logic]
p:414 [in Coq.micromega.ZMicromega]
p:415 [in Coq.Init.Specif]
p:415 [in Coq.ssr.ssrbool]
p:416 [in Coq.PArith.BinPos]
p:416 [in Coq.ssr.ssrbool]
P:418 [in Coq.setoid_ring.Ring_polynom]
P:418 [in Coq.Init.Specif]
p:419 [in Coq.ssr.ssrbool]
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.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:420 [in Coq.ssr.ssrbool]
p:422 [in Coq.PArith.BinPos]
P:422 [in Coq.Logic.ChoiceFacts]
p:423 [in Coq.Init.Specif]
p:423 [in Coq.ssr.ssrbool]
P:424 [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.Init.Specif]
p:426 [in Coq.setoid_ring.Field_theory]
p:427 [in Coq.PArith.BinPos]
p:428 [in Coq.PArith.BinPos]
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.ssr.ssrbool]
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:43 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:430 [in Coq.PArith.BinPos]
p:431 [in Coq.ZArith.BinInt]
p:431 [in Coq.Init.Specif]
p:431 [in Coq.ssr.ssrbool]
p:433 [in Coq.PArith.BinPos]
p:433 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:434 [in Coq.ZArith.BinInt]
p:434 [in Coq.Init.Specif]
p:434 [in Coq.ssr.ssrbool]
P:435 [in Coq.setoid_ring.Ring_polynom]
p:435 [in Coq.setoid_ring.Field_theory]
p:436 [in Coq.PArith.BinPos]
P:436 [in Coq.Init.Specif]
P:436 [in Coq.Init.Logic]
p:437 [in Coq.ssr.ssrbool]
p:438 [in Coq.PArith.BinPos]
p:438 [in Coq.setoid_ring.Field_theory]
p:438 [in Coq.Init.Logic]
p:439 [in Coq.FSets.FMapFacts]
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.ssr.ssreflect]
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:440 [in Coq.PArith.BinPos]
p:440 [in Coq.ZArith.BinInt]
p:440 [in Coq.setoid_ring.Ring_polynom]
p:440 [in Coq.ssr.ssrbool]
P:440 [in Coq.Init.Logic]
p:441 [in Coq.FSets.FMapFacts]
P:442 [in Coq.Init.Specif]
p:443 [in Coq.PArith.BinPos]
p:443 [in Coq.setoid_ring.Ring_polynom]
p:443 [in Coq.ssr.ssrbool]
P:444 [in Coq.Logic.ChoiceFacts]
p:444 [in Coq.ssr.ssrbool]
p:444 [in Coq.Init.Logic]
p:446 [in Coq.PArith.BinPos]
P:446 [in Coq.Logic.ChoiceFacts]
p:447 [in Coq.setoid_ring.Ring_polynom]
P:448 [in Coq.Logic.ChoiceFacts]
P:448 [in Coq.Init.Specif]
p:449 [in Coq.PArith.BinPos]
P:449 [in Coq.Logic.ChoiceFacts]
p:449 [in Coq.Init.Logic]
p:449 [in Coq.FSets.FMapList]
p:45 [in Coq.Numbers.Natural.Abstract.NSub]
p:45 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
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.ssr.ssrbool]
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.Structures.EqualitiesFacts]
p:45 [in Coq.NArith.BinNatDef]
p:45 [in Coq.Reals.ClassicalConstructiveReals]
P:45 [in Coq.Sorting.Heap]
p:452 [in Coq.PArith.BinPos]
p:452 [in Coq.ZArith.BinInt]
p:453 [in Coq.Init.Specif]
p:453 [in Coq.FSets.FMapList]
p:455 [in Coq.PArith.BinPos]
p:455 [in Coq.Init.Logic]
p:456 [in Coq.Init.Specif]
P:458 [in Coq.Init.Specif]
p:458 [in Coq.ssr.ssrbool]
p:458 [in Coq.FSets.FMapWeakList]
p:459 [in Coq.ZArith.BinInt]
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.micromega.RMicromega]
P:46 [in Coq.Logic.WKL]
p:460 [in Coq.PArith.BinPos]
p:462 [in Coq.ZArith.BinInt]
p:463 [in Coq.PArith.BinPos]
p:463 [in Coq.Init.Specif]
p:463 [in Coq.Init.Logic]
p:464 [in Coq.FSets.FMapWeakList]
p:465 [in Coq.ZArith.BinInt]
p:465 [in Coq.FSets.FMapWeakList]
P:465 [in Coq.Init.Logic]
p:466 [in Coq.PArith.BinPos]
p:466 [in Coq.Init.Specif]
p:466 [in Coq.setoid_ring.Field_theory]
p:467 [in Coq.ssr.ssrbool]
p:468 [in Coq.ZArith.BinInt]
P:468 [in Coq.setoid_ring.Ring_polynom]
P:468 [in Coq.Init.Specif]
p:468 [in Coq.setoid_ring.Field_theory]
p:469 [in Coq.Init.Logic]
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.ssr.ssrbool]
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.Reals.Abstract.ConstructiveSum]
P:47 [in Coq.Vectors.VectorDef]
p:471 [in Coq.ZArith.BinInt]
P:471 [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.FSets.FMapWeakList]
p:476 [in Coq.Init.Logic]
p:476 [in Coq.FSets.FMapList]
p:477 [in Coq.PArith.BinPos]
P:477 [in Coq.setoid_ring.Ring_polynom]
p:477 [in Coq.Init.Specif]
p:479 [in Coq.PArith.BinPos]
P:479 [in Coq.Init.Specif]
P:479 [in Coq.Init.Logic]
p:48 [in Coq.Numbers.Natural.Abstract.NSub]
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.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:483 [in Coq.PArith.BinPos]
p:483 [in Coq.ZArith.BinInt]
p:483 [in Coq.Init.Logic]
p:484 [in Coq.Init.Specif]
p:485 [in Coq.PArith.BinPos]
P:485 [in Coq.setoid_ring.Ring_polynom]
p:486 [in Coq.PArith.BinPos]
p:486 [in Coq.ssr.ssrbool]
P:486 [in Coq.Init.Logic]
p:487 [in Coq.Init.Specif]
p:488 [in Coq.setoid_ring.Ring_polynom]
p:488 [in Coq.Init.Specif]
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.ssr.ssrbool]
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:491 [in Coq.Init.Specif]
p:491 [in Coq.Init.Logic]
p:492 [in Coq.setoid_ring.Ring_polynom]
p:494 [in Coq.PArith.BinPos]
P:494 [in Coq.Init.Logic]
p:495 [in Coq.PArith.BinPos]
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.Specif]
p:498 [in Coq.FSets.FMapFacts]
p:498 [in Coq.Init.Logic]
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.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.Reals.Cauchy.ConstructiveExtra]
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.QArith.Qpower]
p:5 [in Coq.Numbers.Natural.Abstract.NAdd]
p:5 [in Coq.Reals.Cauchy.PosExtra]
p:5 [in Coq.Reals.Cauchy.QExtra]
p:5 [in Coq.NArith.Ndec]
p:5 [in Coq.QArith.QArith_base]
P:5 [in Coq.Init.Tactics]
p:50 [in Coq.Logic.Eqdep_dec]
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.Numbers.DecimalPos]
p:50 [in Coq.Numbers.Natural.Abstract.NGcd]
p:50 [in Coq.Reals.Cos_rel]
p:500 [in Coq.ZArith.BinInt]
P:501 [in Coq.setoid_ring.Ring_polynom]
P:501 [in Coq.Init.Logic]
p:503 [in Coq.ZArith.BinInt]
P:503 [in Coq.Init.Specif]
p:505 [in Coq.Init.Specif]
p:506 [in Coq.Init.Logic]
p:508 [in Coq.ZArith.BinInt]
p:509 [in Coq.Reals.RIneq]
P:509 [in Coq.Init.Logic]
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.ssr.ssrbool]
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.Reals.Cauchy.ConstructiveCauchyReals]
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:512 [in Coq.ZArith.BinInt]
P:513 [in Coq.Init.Specif]
p:514 [in Coq.PArith.BinPos]
p:514 [in Coq.Init.Logic]
p:515 [in Coq.setoid_ring.Ring_polynom]
P:515 [in Coq.ssr.ssrbool]
p:517 [in Coq.PArith.BinPos]
p:517 [in Coq.Init.Specif]
P:517 [in Coq.Init.Logic]
p:518 [in Coq.setoid_ring.Ring_polynom]
P:519 [in Coq.Init.Specif]
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:520 [in Coq.PArith.BinPos]
p:520 [in Coq.setoid_ring.Ring_polynom]
p:521 [in Coq.Init.Specif]
p:521 [in Coq.Init.Logic]
p:523 [in Coq.PArith.BinPos]
p:523 [in Coq.setoid_ring.Ring_polynom]
P:523 [in Coq.Init.Logic]
p:525 [in Coq.setoid_ring.Ring_polynom]
P:525 [in Coq.ssr.ssrbool]
p:526 [in Coq.PArith.BinPos]
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:528 [in Coq.Reals.RIneq]
p:528 [in Coq.Init.Logic]
p:529 [in Coq.PArith.BinPos]
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.Exp_prop]
p:53 [in Coq.Init.Wf]
P:53 [in Coq.ssr.ssrbool]
P:53 [in Coq.NArith.BinNat]
p:53 [in Coq.Reals.Rdefinitions]
p:53 [in Coq.Numbers.Natural.Abstract.NGcd]
P:53 [in Coq.Vectors.VectorDef]
P:530 [in Coq.Init.Specif]
p:530 [in Coq.Reals.RIneq]
p:531 [in Coq.Reals.RIneq]
p:531 [in Coq.Init.Logic]
p:532 [in Coq.PArith.BinPos]
p:532 [in Coq.Reals.RIneq]
p:532 [in Coq.Init.Logic]
p:533 [in Coq.Init.Specif]
p:533 [in Coq.Reals.RIneq]
P:534 [in Coq.Init.Logic]
p:535 [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.Numbers.DecimalPos]
p:54 [in Coq.PArith.BinPosDef]
p:54 [in Coq.Reals.Cos_rel]
P:540 [in Coq.Init.Specif]
P:540 [in Coq.Init.Logic]
p:541 [in Coq.PArith.BinPos]
p:546 [in Coq.Init.Specif]
P:546 [in Coq.Init.Logic]
P:549 [in Coq.Init.Specif]
p:55 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
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:551 [in Coq.Init.Logic]
p:554 [in Coq.Init.Logic]
p:555 [in Coq.PArith.BinPos]
p:555 [in Coq.Init.Specif]
P:556 [in Coq.Init.Logic]
p:557 [in Coq.PArith.BinPos]
P:557 [in Coq.Init.Specif]
p:559 [in Coq.PArith.BinPos]
P:56 [in Coq.Logic.Eqdep_dec]
P:56 [in Coq.FSets.FSetBridge]
p:56 [in Coq.PArith.BinPos]
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.Reals.Cauchy.ConstructiveCauchyReals]
p:56 [in Coq.Numbers.Natural.Abstract.NGcd]
p:56 [in Coq.Lists.SetoidList]
p:561 [in Coq.PArith.BinPos]
p:561 [in Coq.Init.Logic]
p:562 [in Coq.PArith.BinPos]
p:563 [in Coq.Init.Specif]
p:564 [in Coq.PArith.BinPos]
p:564 [in Coq.Init.Logic]
P:565 [in Coq.Init.Specif]
P:566 [in Coq.Init.Logic]
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:57 [in Coq.QArith.Qpower]
p:570 [in Coq.PArith.BinPos]
p:571 [in Coq.Init.Specif]
P:571 [in Coq.ssr.ssrbool]
p:572 [in Coq.PArith.BinPos]
p:572 [in Coq.Init.Logic]
P:573 [in Coq.Init.Specif]
P:573 [in Coq.ssr.ssrbool]
p:575 [in Coq.PArith.BinPos]
P:575 [in Coq.ssr.ssrbool]
p:575 [in Coq.Init.Logic]
P:577 [in Coq.ssr.ssrbool]
P:577 [in Coq.Init.Logic]
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.ssr.ssrbool]
p:581 [in Coq.Init.Specif]
p:582 [in Coq.Init.Specif]
P:583 [in Coq.ssr.ssrbool]
p:584 [in Coq.Init.Logic]
P:585 [in Coq.Init.Specif]
p:585 [in Coq.Init.Logic]
P:587 [in Coq.ssr.ssrbool]
P:588 [in Coq.Init.Logic]
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.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.Numbers.Natural.Abstract.NGcd]
p:59 [in Coq.rtauto.Rtauto]
p:591 [in Coq.Init.Specif]
P:591 [in Coq.ssr.ssrbool]
p:592 [in Coq.Init.Specif]
p:594 [in Coq.FSets.FMapWeakList]
P:594 [in Coq.Init.Logic]
p:595 [in Coq.PArith.BinPos]
P:595 [in Coq.Init.Specif]
P:595 [in Coq.ssr.ssrbool]
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:60 [in Coq.Numbers.Natural.Abstract.NSub]
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.btauto.Algebra]
p:60 [in Coq.Init.Specif]
p:60 [in Coq.Numbers.Integer.Abstract.ZMaxMin]
p:60 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
p:60 [in Coq.Numbers.DecimalPos]
P:600 [in Coq.Init.Logic]
P:601 [in Coq.ssr.ssrbool]
p:602 [in Coq.Init.Logic]
p:603 [in Coq.PArith.BinPos]
p:603 [in Coq.Init.Specif]
P:604 [in Coq.ssr.ssrbool]
p:606 [in Coq.PArith.BinPos]
P:607 [in Coq.Init.Specif]
p:608 [in Coq.PArith.BinPos]
P:608 [in Coq.ssr.ssrbool]
p:608 [in Coq.Init.Logic]
p:609 [in Coq.PArith.BinPos]
p:61 [in Coq.nsatz.NsatzTactic]
p:61 [in Coq.Logic.EqdepFacts]
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:610 [in Coq.Init.Logic]
p:611 [in Coq.PArith.BinPos]
p:611 [in Coq.Lists.List]
p:612 [in Coq.Init.Logic]
p:613 [in Coq.PArith.BinPos]
p:613 [in Coq.Lists.List]
p:613 [in Coq.Init.Specif]
p:614 [in Coq.FSets.FMapFacts]
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:617 [in Coq.Init.Specif]
p:618 [in Coq.FSets.FMapFacts]
p:619 [in Coq.PArith.BinPos]
p:619 [in Coq.Init.Logic]
P:62 [in Coq.FSets.FSetBridge]
p:62 [in Coq.PArith.BinPos]
P:62 [in Coq.MSets.MSetProperties]
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:621 [in Coq.Init.Logic]
p:622 [in Coq.FSets.FMapFacts]
p:624 [in Coq.FSets.FMapFacts]
p:625 [in Coq.Init.Specif]
p:625 [in Coq.Init.Logic]
p:626 [in Coq.FSets.FMapFacts]
p:627 [in Coq.FSets.FMapFacts]
P:627 [in Coq.Init.Logic]
p:628 [in Coq.FSets.FMapFacts]
P:629 [in Coq.Init.Specif]
p:629 [in Coq.Init.Logic]
p:63 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:63 [in Coq.Numbers.Integer.Abstract.ZAdd]
p:63 [in Coq.Numbers.Integer.Abstract.ZGcd]
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:635 [in Coq.Init.Logic]
p:637 [in Coq.Init.Specif]
P:638 [in Coq.Init.Logic]
P:64 [in Coq.Logic.Eqdep_dec]
p:64 [in Coq.PArith.BinPos]
p:64 [in Coq.PArith.Pnat]
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.Reals.Cauchy.ConstructiveCauchyReals]
P:64 [in Coq.Logic.WKL]
p:64 [in Coq.PArith.BinPosDef]
p:64 [in Coq.Reals.Cos_rel]
P:641 [in Coq.Init.Specif]
p:641 [in Coq.Init.Logic]
p:644 [in Coq.Init.Specif]
p:646 [in Coq.Init.Logic]
P:65 [in Coq.Lists.Streams]
p:65 [in Coq.Vectors.VectorSpec]
p:65 [in Coq.Numbers.Natural.Abstract.NSub]
P:65 [in Coq.setoid_ring.Ring_polynom]
p:65 [in Coq.Numbers.NaryFunctions]
p:65 [in Coq.PArith.Pnat]
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.rtauto.Rtauto]
p:652 [in Coq.Init.Specif]
p:652 [in Coq.Init.Logic]
P:654 [in Coq.Init.Specif]
p:659 [in Coq.Init.Logic]
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.Numbers.Integer.Abstract.ZGcd]
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:660 [in Coq.Init.Specif]
p:661 [in Coq.Init.Specif]
P:663 [in Coq.FSets.FMapFacts]
P:663 [in Coq.Init.Specif]
P:664 [in Coq.Init.Logic]
p:67 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
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:670 [in Coq.FSets.FMapFacts]
p:670 [in Coq.Init.Specif]
p:670 [in Coq.Init.Logic]
P:673 [in Coq.Init.Logic]
p:674 [in Coq.Init.Specif]
P:676 [in Coq.Init.Specif]
p:679 [in Coq.Init.Logic]
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.NatInt.NZGcd]
P:68 [in Coq.Logic.WKL]
P:681 [in Coq.Init.Logic]
P:684 [in Coq.Init.Specif]
p:687 [in Coq.Init.Logic]
P:689 [in Coq.Init.Logic]
P:69 [in Coq.PArith.BinPos]
p:69 [in Coq.Numbers.HexadecimalPos]
P:69 [in Coq.MSets.MSetProperties]
p:69 [in Coq.Numbers.Integer.Abstract.ZGcd]
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:692 [in Coq.Init.Specif]
P:693 [in Coq.FSets.FMapFacts]
p:695 [in Coq.Init.Logic]
P:697 [in Coq.Init.Logic]
p:699 [in Coq.Init.Specif]
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.ZArith.Zpow_alt]
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.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.ssr.ssrbool]
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:703 [in Coq.Init.Specif]
P:705 [in Coq.Init.Specif]
p:705 [in Coq.Init.Logic]
p:706 [in Coq.Init.Logic]
P:709 [in Coq.ssr.ssrbool]
P:709 [in Coq.MSets.MSetRBT]
P:709 [in Coq.Init.Logic]
p:71 [in Coq.Vectors.VectorSpec]
P:71 [in Coq.Logic.Eqdep_dec]
p:71 [in Coq.PArith.BinPos]
p:71 [in Coq.Numbers.NatInt.NZAddOrder]
P:71 [in Coq.setoid_ring.Ring_polynom]
p:71 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p:71 [in Coq.Reals.Rbasic_fun]
p:71 [in Coq.Structures.EqualitiesFacts]
P:71 [in Coq.Logic.Diaconescu]
P:711 [in Coq.MSets.MSetRBT]
p:712 [in Coq.Init.Specif]
P:714 [in Coq.ssr.ssrbool]
p:715 [in Coq.Init.Logic]
p:716 [in Coq.Init.Specif]
p:716 [in Coq.Init.Logic]
P:718 [in Coq.Init.Specif]
P:719 [in Coq.Init.Logic]
p:72 [in Coq.Logic.Eqdep_dec]
P:72 [in Coq.Logic.EqdepFacts]
p:72 [in Coq.Numbers.Integer.Abstract.ZGcd]
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.Init.Logic]
p:72 [in Coq.btauto.Reflect]
p:72 [in Coq.rtauto.Rtauto]
P:722 [in Coq.ssr.ssrbool]
p:725 [in Coq.Init.Logic]
p:727 [in Coq.Init.Specif]
P:729 [in Coq.Init.Logic]
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.Reals.MVT]
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:730 [in Coq.ssr.ssrbool]
p:731 [in Coq.Init.Specif]
P:733 [in Coq.Init.Specif]
p:737 [in Coq.Init.Logic]
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:74 [in Coq.QArith.Qpower]
p:740 [in Coq.Init.Specif]
p:741 [in Coq.Init.Specif]
P:741 [in Coq.Init.Logic]
p:744 [in Coq.Init.Specif]
p:745 [in Coq.Init.Specif]
P:749 [in Coq.Init.Specif]
p:749 [in Coq.Init.Logic]
p:75 [in Coq.PArith.BinPos]
p:75 [in Coq.Numbers.Integer.Abstract.ZGcd]
P:75 [in Coq.Logic.JMeq]
P:75 [in Coq.Reals.Rsqrt_def]
p:75 [in Coq.Reals.Rtrigo_alt]
p:75 [in Coq.PArith.BinPosDef]
P:753 [in Coq.Init.Logic]
P:757 [in Coq.Init.Specif]
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.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:761 [in Coq.Init.Logic]
P:765 [in Coq.Init.Specif]
P:765 [in Coq.Init.Logic]
p:768 [in Coq.Init.Specif]
p:768 [in Coq.Init.Logic]
p:77 [in Coq.QArith.Qcanon]
p:77 [in Coq.Logic.Eqdep_dec]
p:77 [in Coq.PArith.BinPos]
p:77 [in Coq.PArith.Pnat]
P:77 [in Coq.Init.Specif]
p:77 [in Coq.PArith.BinPosDef]
p:77 [in Coq.QArith.Qpower]
p:776 [in Coq.Init.Specif]
p:776 [in Coq.Init.Logic]
P:778 [in Coq.Init.Logic]
p:78 [in Coq.Numbers.Integer.Abstract.ZGcd]
p:78 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
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.Abstract.ConstructiveLimits]
p:78 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:78 [in Coq.Reals.Cos_rel]
p:780 [in Coq.Init.Logic]
p:784 [in Coq.Init.Specif]
P:789 [in Coq.Init.Specif]
p:789 [in Coq.Init.Logic]
p:79 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:79 [in Coq.Numbers.Natural.Abstract.NSub]
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:793 [in Coq.Init.Specif]
p:794 [in Coq.Init.Specif]
P:794 [in Coq.Init.Logic]
p:797 [in Coq.Init.Logic]
p:799 [in Coq.Init.Specif]
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:8 [in Coq.Reals.Cauchy.QExtra]
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.QArith.Qpower]
p:80 [in Coq.Reals.Cos_rel]
p:800 [in Coq.Init.Specif]
p:801 [in Coq.Init.Logic]
P:802 [in Coq.Init.Specif]
p:808 [in Coq.Init.Specif]
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.Numbers.NatInt.NZDiv]
P:81 [in Coq.Logic.ClassicalFacts]
p:81 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:81 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
p:810 [in Coq.Init.Logic]
P:811 [in Coq.Init.Specif]
P:812 [in Coq.Init.Logic]
p:817 [in Coq.Init.Specif]
p:818 [in Coq.Init.Logic]
P:819 [in Coq.Init.Specif]
p:819 [in Coq.Init.Logic]
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:821 [in Coq.Init.Logic]
p:825 [in Coq.Init.Specif]
P:827 [in Coq.Init.Specif]
p:827 [in Coq.Init.Logic]
P:829 [in Coq.Init.Logic]
p:83 [in Coq.Init.Specif]
P:83 [in Coq.Init.Logic]
p:833 [in Coq.Init.Specif]
P:835 [in Coq.Init.Specif]
p:836 [in Coq.Init.Logic]
P:84 [in Coq.Logic.Eqdep_dec]
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:840 [in Coq.Init.Logic]
p:841 [in Coq.Init.Logic]
p:843 [in Coq.Init.Specif]
P:843 [in Coq.Init.Logic]
p:844 [in Coq.Init.Specif]
P:847 [in Coq.Init.Specif]
p:85 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:85 [in Coq.Logic.Eqdep_dec]
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.micromega.OrderedRing]
p:85 [in Coq.Structures.GenericMinMax]
P:851 [in Coq.Init.Logic]
p:853 [in Coq.Init.Specif]
p:854 [in Coq.Init.Specif]
P:857 [in Coq.Init.Specif]
P:859 [in Coq.Init.Logic]
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.ZArith.Zpower]
p:86 [in Coq.ZArith.Zorder]
p:865 [in Coq.Init.Specif]
p:866 [in Coq.Init.Logic]
P:869 [in Coq.Init.Specif]
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.ZArith.Zorder]
p:87 [in Coq.Vectors.VectorDef]
p:870 [in Coq.Init.Logic]
P:872 [in Coq.Init.Logic]
p:875 [in Coq.Init.Specif]
P:879 [in Coq.Init.Specif]
p:879 [in Coq.Init.Logic]
p:88 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:88 [in Coq.PArith.Pnat]
P:88 [in Coq.micromega.EnvRing]
p:88 [in Coq.Arith.PeanoNat]
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:883 [in Coq.Init.Logic]
P:885 [in Coq.Init.Logic]
p:887 [in Coq.Init.Specif]
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:89 [in Coq.Init.Logic]
P:891 [in Coq.Init.Specif]
p:894 [in Coq.Init.Logic]
p:898 [in Coq.Init.Logic]
p:899 [in Coq.Init.Specif]
p:9 [in Coq.Arith.Le]
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.Reals.Cauchy.QExtra]
P:9 [in Coq.Reals.ClassicalDedekindReals]
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.PArith.Pnat]
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:900 [in Coq.Init.Logic]
P:903 [in Coq.Init.Specif]
p:906 [in Coq.Init.Specif]
p:907 [in Coq.Init.Logic]
p:908 [in Coq.Init.Logic]
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.Reals.Cauchy.ConstructiveRcomplete]
P:91 [in Coq.Sorting.Permutation]
p:91 [in Coq.micromega.OrderedRing]
p:91 [in Coq.Structures.GenericMinMax]
P:91 [in Coq.Init.Datatypes]
p:91 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
p:911 [in Coq.Init.Logic]
p:912 [in Coq.Init.Logic]
p:914 [in Coq.Init.Specif]
P:916 [in Coq.Init.Specif]
P:916 [in Coq.Init.Logic]
p:92 [in Coq.Reals.Abstract.ConstructiveReals]
p:92 [in Coq.Numbers.Natural.Abstract.NSub]
P:92 [in Coq.setoid_ring.Ring_polynom]
p:92 [in Coq.PArith.Pnat]
P:92 [in Coq.Sorting.Permutation]
p:92 [in Coq.omega.OmegaLemmas]
p:92 [in Coq.NArith.Ndigits]
p:92 [in Coq.PArith.BinPosDef]
p:922 [in Coq.Init.Specif]
p:923 [in Coq.Init.Specif]
P:924 [in Coq.Init.Logic]
P:925 [in Coq.Init.Specif]
p:93 [in Coq.Vectors.VectorSpec]
p:93 [in Coq.Numbers.Integer.Abstract.ZAdd]
P:93 [in Coq.Logic.EqdepFacts]
p:93 [in Coq.PArith.BinPos]
p:93 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
P:93 [in Coq.omega.OmegaLemmas]
p:932 [in Coq.Init.Specif]
P:932 [in Coq.Init.Logic]
p:935 [in Coq.Init.Logic]
p:936 [in Coq.Init.Specif]
P:938 [in Coq.Init.Specif]
P:94 [in Coq.ZArith.BinInt]
p:94 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
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:943 [in Coq.Init.Logic]
P:946 [in Coq.Init.Specif]
p:949 [in Coq.Init.Logic]
p:95 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:95 [in Coq.PArith.Pnat]
p:95 [in Coq.NArith.Ndigits]
P:95 [in Coq.setoid_ring.Ncring_polynom]
p:95 [in Coq.Init.Logic]
p:95 [in Coq.PArith.BinPosDef]
P:954 [in Coq.Init.Specif]
P:954 [in Coq.Init.Logic]
p:958 [in Coq.Init.Logic]
p:959 [in Coq.Init.Logic]
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.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.Init.Specif]
p:964 [in Coq.Init.Logic]
p:965 [in Coq.Init.Specif]
p:965 [in Coq.Init.Logic]
P:967 [in Coq.Init.Specif]
p:97 [in Coq.Vectors.VectorSpec]
p:97 [in Coq.Reals.Abstract.ConstructiveReals]
p:97 [in Coq.PArith.BinPos]
p:97 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
P:97 [in Coq.Logic.ChoiceFacts]
P:97 [in Coq.Init.Specif]
P:97 [in Coq.Sorting.Permutation]
p:97 [in Coq.Arith.PeanoNat]
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:974 [in Coq.Init.Specif]
P:975 [in Coq.Lists.List]
p:978 [in Coq.Init.Specif]
P:979 [in Coq.Lists.List]
P:98 [in Coq.ZArith.BinInt]
p:98 [in Coq.PArith.Pnat]
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:980 [in Coq.Init.Specif]
P:983 [in Coq.Lists.List]
P:987 [in Coq.Lists.List]
p:989 [in Coq.Init.Specif]
p:99 [in Coq.Numbers.Integer.Abstract.ZAdd]
p:99 [in Coq.Numbers.NaryFunctions]
P:99 [in Coq.Logic.FunctionalExtensionality]
P:99 [in Coq.Sorting.CPermutation]
P:99 [in Coq.Reals.Ranalysis5]
p:99 [in Coq.QArith.Qpower]
P:991 [in Coq.Lists.List]
p:993 [in Coq.Init.Specif]
P:995 [in Coq.Lists.List]
P:995 [in Coq.Init.Specif]
P:999 [in Coq.Lists.List]
| 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 | (72487 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 | (1049 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 | (47021 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 | (788 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 | (1537 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 | (588 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 | (11841 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 | (1025 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 | (634 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 | (306 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 | (473 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 | (486 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 | (881 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 | (1465 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 | (4229 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 | (164 entries) |