| 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 | (73252 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 | (1016 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 | (47569 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 | (800 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 | (1555 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 | (592 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 | (11846 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 | (959 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 | (629 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 | (308 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 | (475 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 | (494 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 | (912 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 | (1503 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 | (4428 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 | (166 entries) |
P (binder)
PandQ:3 [in Coq.ssr.ssrfun]partition:229 [in Coq.FSets.FSetInterface]
partition:74 [in Coq.FSets.FSetBridge]
pat:107 [in Coq.ZArith.Znumtheory]
pat:120 [in Coq.ZArith.Znumtheory]
pat:212 [in Coq.micromega.Tauto]
pat:3 [in Coq.Arith.Cantor]
pat:30 [in Coq.Strings.String]
pat:33 [in Coq.Strings.String]
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:46 [in Coq.Numbers.Natural.Abstract.NGcd]
pat:49 [in Coq.Numbers.Natural.Abstract.NGcd]
pat:57 [in Coq.Strings.Ascii]
pat:60 [in Coq.Strings.Ascii]
pat:9 [in Coq.Arith.Cantor]
pat:94 [in Coq.ZArith.Znumtheory]
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:622 [in Coq.ssr.ssrbool]
Pf:625 [in Coq.ssr.ssrbool]
Pgoal:102 [in Coq.ssr.ssreflect]
Pgt:124 [in Coq.Init.Datatypes]
Pgt:129 [in Coq.Init.Datatypes]
Pgt:134 [in Coq.Init.Datatypes]
Phf:676 [in Coq.ssr.ssrbool]
Phf:678 [in Coq.ssr.ssrbool]
Phf:680 [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:596 [in Coq.ssr.ssrbool]
Ph:669 [in Coq.ssr.ssrbool]
Ph:670 [in Coq.ssr.ssrbool]
Ph:671 [in Coq.ssr.ssrbool]
Ph:677 [in Coq.ssr.ssrbool]
Ph:679 [in Coq.ssr.ssrbool]
Ph:681 [in Coq.ssr.ssrbool]
Ph:788 [in Coq.ssr.ssrbool]
Ph:793 [in Coq.ssr.ssrbool]
Ph:801 [in Coq.ssr.ssrbool]
Ph:809 [in Coq.ssr.ssrbool]
Plemma:101 [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:436 [in Coq.ssr.ssrbool]
pp:439 [in Coq.ssr.ssrbool]
pqr:1010 [in Coq.Init.Specif]
pqr:589 [in Coq.Init.Specif]
pqr:599 [in Coq.Init.Specif]
pqr:708 [in Coq.Init.Logic]
pqr:718 [in Coq.Init.Logic]
pqr:748 [in Coq.Init.Specif]
pqr:851 [in Coq.Init.Specif]
pqr:861 [in Coq.Init.Specif]
pqr:910 [in Coq.Init.Logic]
PQ':113 [in Coq.setoid_ring.Ring_polynom]
PQ':115 [in Coq.micromega.EnvRing]
pq:175 [in Coq.Init.Specif]
pq:182 [in Coq.Init.Specif]
pq:328 [in Coq.Init.Specif]
pq:392 [in Coq.Init.Specif]
pq:399 [in Coq.Init.Specif]
pq:478 [in Coq.Init.Logic]
pq:485 [in Coq.Init.Logic]
pq:491 [in Coq.Init.Specif]
pq:583 [in Coq.Init.Logic]
Pratan:311 [in Coq.Reals.Ratan]
precomposed_eq:25 [in Coq.Logic.Adjointification]
pred:84 [in Coq.MSets.MSetRBT]
preo:134 [in Coq.Classes.CRelationClasses]
preo:170 [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:148 [in Coq.micromega.RingMicromega]
Prf:261 [in Coq.Reals.Ranalysis5]
Prf:305 [in Coq.Reals.Ranalysis5]
prf:319 [in Coq.micromega.ZMicromega]
Prf:361 [in Coq.Reals.Ranalysis5]
Prf:404 [in Coq.Reals.Ranalysis5]
Prf:421 [in Coq.Reals.Ranalysis5]
prf:77 [in Coq.rtauto.Rtauto]
Prg_incr:306 [in Coq.Reals.Ranalysis5]
Prg_incr:263 [in Coq.Reals.Ranalysis5]
Prg:262 [in Coq.Reals.Ranalysis5]
Prg:362 [in Coq.Reals.Ranalysis5]
Prmymeta:312 [in Coq.Reals.Ratan]
property:116 [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:182 [in Coq.Reals.Ranalysis5]
pr1:211 [in Coq.Reals.RiemannInt]
pr1:23 [in Coq.Reals.Ranalysis5]
Pr1:246 [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:65 [in Coq.Reals.Ratan]
pr1:66 [in Coq.Reals.RiemannInt]
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:29 [in Coq.Reals.NewtonInt]
pr:30 [in Coq.Reals.MVT]
pr:313 [in Coq.Reals.RiemannInt]
pr:322 [in Coq.Reals.Ratan]
pr:323 [in Coq.Reals.Ratan]
pr:33 [in Coq.Reals.SeqProp]
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:70 [in Coq.Reals.Ratan]
pr:71 [in Coq.btauto.Algebra]
pr:74 [in Coq.Reals.Runcountable]
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:221 [in Coq.Reals.RiemannInt]
psi2:224 [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':292 [in Coq.ssr.ssrbool]
pT:290 [in Coq.ssr.ssrbool]
pT:387 [in Coq.ssr.ssrbool]
pT:435 [in Coq.ssr.ssrbool]
pT:437 [in Coq.ssr.ssrbool]
pt:450 [in Coq.micromega.ZMicromega]
pt:454 [in Coq.micromega.ZMicromega]
P_hprop:529 [in Coq.Init.Specif]
P_hprop:513 [in Coq.Init.Specif]
P_hprop:350 [in Coq.Init.Specif]
P_hprop:257 [in Coq.Init.Specif]
P_hprop:800 [in Coq.Init.Logic]
P_hprop:632 [in Coq.Init.Logic]
P_hprop:615 [in Coq.Init.Logic]
P_hprop:605 [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':194 [in Coq.Init.Specif]
P':197 [in Coq.micromega.EnvRing]
p':2 [in Coq.NArith.Ndec]
P':200 [in Coq.micromega.EnvRing]
P':210 [in Coq.setoid_ring.Ring_polynom]
P':212 [in Coq.setoid_ring.Ring_polynom]
p':215 [in Coq.Init.Specif]
p':219 [in Coq.NArith.BinNat]
p':224 [in Coq.Init.Specif]
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':47 [in Coq.Logic.Adjointification]
p':48 [in Coq.Logic.Adjointification]
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:448 [in Coq.Init.Logic]
P0:454 [in Coq.Init.Logic]
P0:651 [in Coq.Init.Logic]
P0:658 [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:115 [in Coq.Relations.Relation_Operators]
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:142 [in Coq.Logic.Eqdep_dec]
P1:144 [in Coq.ssr.ssrbool]
P1:149 [in Coq.micromega.ZifyClasses]
P1:149 [in Coq.ssr.ssrbool]
p1:15 [in Coq.micromega.Ztac]
p1:155 [in Coq.Vectors.VectorSpec]
P1:155 [in Coq.micromega.EnvRing]
P1:155 [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:162 [in Coq.ssr.ssrbool]
p1:164 [in Coq.Logic.EqdepFacts]
p1:165 [in Coq.Vectors.VectorSpec]
P1:167 [in Coq.micromega.EnvRing]
P1:167 [in Coq.ssr.ssrbool]
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:26 [in Coq.Vectors.Fin]
p1:267 [in Coq.ssr.ssrbool]
p1:27 [in Coq.Logic.Adjointification]
p1:270 [in Coq.ssr.ssrbool]
p1:273 [in Coq.ssr.ssrbool]
p1:278 [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:29 [in Coq.Logic.Adjointification]
P1:291 [in Coq.setoid_ring.Ring_polynom]
P1:296 [in Coq.setoid_ring.Ring_polynom]
P1:301 [in Coq.micromega.EnvRing]
p1:301 [in Coq.ssr.ssrbool]
p1:304 [in Coq.ssr.ssrbool]
P1:307 [in Coq.setoid_ring.Ring_polynom]
P1:307 [in Coq.micromega.EnvRing]
p1:309 [in Coq.ssr.ssrbool]
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:116 [in Coq.Relations.Relation_Operators]
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:143 [in Coq.Logic.Eqdep_dec]
P2:145 [in Coq.ssr.ssrbool]
P2:150 [in Coq.ssr.ssrbool]
P2:152 [in Coq.micromega.ZifyClasses]
p2:156 [in Coq.Vectors.VectorSpec]
P2:156 [in Coq.ssr.ssrbool]
P2:157 [in Coq.micromega.EnvRing]
p2:16 [in Coq.micromega.Ztac]
P2:162 [in Coq.setoid_ring.Ring_polynom]
P2:163 [in Coq.micromega.EnvRing]
P2:163 [in Coq.ssr.ssrbool]
p2:166 [in Coq.Vectors.VectorSpec]
P2:168 [in Coq.ssr.ssrbool]
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:268 [in Coq.ssr.ssrbool]
p2:271 [in Coq.ssr.ssrbool]
p2:274 [in Coq.ssr.ssrbool]
p2:279 [in Coq.ssr.ssrbool]
p2:28 [in Coq.Logic.Adjointification]
P2:287 [in Coq.setoid_ring.Ring_polynom]
P2:293 [in Coq.setoid_ring.Ring_polynom]
P2:298 [in Coq.setoid_ring.Ring_polynom]
p2:3 [in Coq.Logic.ProofIrrelevance]
p2:3 [in Coq.Logic.ProofIrrelevanceFacts]
p2:30 [in Coq.Logic.Classical_Prop]
p2:30 [in Coq.Logic.Adjointification]
p2:302 [in Coq.ssr.ssrbool]
P2:303 [in Coq.micromega.EnvRing]
p2:305 [in Coq.ssr.ssrbool]
P2:309 [in Coq.micromega.EnvRing]
p2:31 [in Coq.micromega.Ztac]
p2:310 [in Coq.ssr.ssrbool]
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:146 [in Coq.ssr.ssrbool]
P3:151 [in Coq.ssr.ssrbool]
P3:157 [in Coq.ssr.ssrbool]
P3:164 [in Coq.ssr.ssrbool]
p3:167 [in Coq.Vectors.VectorSpec]
P3:169 [in Coq.ssr.ssrbool]
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:152 [in Coq.ssr.ssrbool]
P4:158 [in Coq.ssr.ssrbool]
P4:170 [in Coq.ssr.ssrbool]
P5:159 [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.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.Numbers.Natural.Abstract.NAddOrder]
p:10 [in Coq.Program.Equality]
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.Arith.Arith_prebase]
P:100 [in Coq.Logic.EqdepFacts]
p:100 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
p:100 [in Coq.Strings.String]
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:1001 [in Coq.Init.Specif]
P:1003 [in Coq.Lists.List]
P:1007 [in Coq.Lists.List]
p:1008 [in Coq.Init.Specif]
p:1009 [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:1011 [in Coq.Lists.List]
p:1012 [in Coq.Init.Specif]
p:1013 [in Coq.Init.Specif]
P:1014 [in Coq.Lists.List]
P:1017 [in Coq.Init.Specif]
P:1018 [in Coq.Lists.List]
p:102 [in Coq.Numbers.Integer.Abstract.ZAdd]
p:102 [in Coq.PArith.BinPos]
P:102 [in Coq.ZArith.BinInt]
p:102 [in Coq.Numbers.NaryFunctions]
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:1022 [in Coq.Lists.List]
P:1025 [in Coq.Init.Specif]
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.MSets.MSetList]
P:103 [in Coq.omega.OmegaLemmas]
p:103 [in Coq.ZArith.Zorder]
P:103 [in Coq.setoid_ring.Ncring_polynom]
P:1032 [in Coq.Lists.List]
P:1033 [in Coq.Init.Specif]
P:1036 [in Coq.Lists.List]
p:1036 [in Coq.Init.Specif]
P:104 [in Coq.MSets.MSetInterface]
p:104 [in Coq.Arith.Arith_prebase]
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.Init.Logic]
P:104 [in Coq.FSets.FSetProperties]
P:1040 [in Coq.Lists.List]
p:1044 [in Coq.Init.Specif]
P:1047 [in Coq.Lists.List]
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:1050 [in Coq.Init.Specif]
P:1051 [in Coq.Lists.List]
P:1055 [in Coq.Lists.List]
P:1055 [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:1061 [in Coq.Lists.List]
p:1065 [in Coq.Init.Specif]
p:1066 [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.ssr.ssreflect]
p:107 [in Coq.micromega.OrderedRing]
p:107 [in Coq.ZArith.Int]
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.Arith.Arith_prebase]
p:109 [in Coq.Numbers.Integer.Abstract.ZLcm]
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.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.Arith.Gt]
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.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.ssr.ssrbool]
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.Numbers.Integer.Abstract.ZLcm]
P:112 [in Coq.omega.OmegaLemmas]
p:112 [in Coq.ZArith.Zorder]
p:113 [in Coq.Arith.Arith_prebase]
P:113 [in Coq.Arith.Wf_nat]
p:113 [in Coq.btauto.Algebra]
P:113 [in Coq.Logic.ChoiceFacts]
P:113 [in Coq.ssr.ssrbool]
p:113 [in Coq.Init.Nat]
p:113 [in Coq.ZArith.Int]
p:113 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
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.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.ZArith.BinInt]
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.Numbers.Cyclic.ZModulo.ZModulo]
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.ssr.ssreflect]
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.Numbers.Natural.Abstract.NGcd]
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.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.Logic.ClassicalFacts]
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:121 [in Coq.Reals.Rbasic_fun]
p:122 [in Coq.Arith.Arith_prebase]
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:124 [in Coq.Logic.Eqdep_dec]
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.Arith.Arith_prebase]
P:125 [in Coq.ssr.ssrbool]
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.ZArith.BinInt]
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.ZArith.BinInt]
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.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.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.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.ssr.ssrbool]
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.Relations.Relation_Operators]
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: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.ssr.ssrbool]
P:137 [in Coq.FSets.FSetInterface]
p:137 [in Coq.micromega.OrderedRing]
P:137 [in Coq.Init.Logic]
p:138 [in Coq.Vectors.Fin]
p:138 [in Coq.FSets.FMapPositive]
p:138 [in Coq.PArith.BinPosDef]
p:138 [in Coq.Relations.Relation_Operators]
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.ssr.ssrbool]
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.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.Arith.Mult]
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:141 [in Coq.QArith.Qcanon]
p:141 [in Coq.Logic.EqdepFacts]
p:141 [in Coq.micromega.OrderedRing]
P:141 [in Coq.Init.Logic]
p:142 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
p:142 [in Coq.Arith.Arith_prebase]
p:142 [in Coq.PArith.BinPos]
P:142 [in Coq.Init.Specif]
P:142 [in Coq.ssr.ssrbool]
p:142 [in Coq.ZArith.Zorder]
p:142 [in Coq.Vectors.Fin]
p:142 [in Coq.Structures.GenericMinMax]
p:143 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
p:143 [in Coq.PArith.BinPosDef]
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.NArith.BinNat]
p:145 [in Coq.micromega.OrderedRing]
p:145 [in Coq.ZArith.Zorder]
p:145 [in Coq.Structures.GenericMinMax]
P:145 [in Coq.Init.Logic]
p:145 [in Coq.PArith.BinPosDef]
p:146 [in Coq.Logic.EqdepFacts]
P:146 [in Coq.Reals.Rfunctions]
P:146 [in Coq.Arith.Wf_nat]
P:146 [in Coq.Init.Specif]
P:146 [in Coq.omega.OmegaLemmas]
P:147 [in Coq.Logic.Eqdep_dec]
p:147 [in Coq.Arith.Arith_prebase]
p:147 [in Coq.NArith.BinNat]
p:147 [in Coq.Vectors.Fin]
p:148 [in Coq.Logic.Eqdep_dec]
p:148 [in Coq.PArith.BinPos]
p:148 [in Coq.ZArith.Zorder]
p:148 [in Coq.Structures.GenericMinMax]
p:148 [in Coq.PArith.BinPosDef]
P:149 [in Coq.Logic.Eqdep_dec]
p:149 [in Coq.Logic.EqdepFacts]
p:149 [in Coq.ZArith.BinInt]
P:149 [in Coq.Arith.Wf_nat]
P:149 [in Coq.Init.Logic]
p:149 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
p:15 [in Coq.Arith.Div2]
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.Numbers.NatInt.NZAdd]
p:15 [in Coq.Numbers.Integer.Abstract.ZMul]
P:150 [in Coq.Logic.EqdepFacts]
p:150 [in Coq.PArith.BinPos]
p:150 [in Coq.btauto.Algebra]
p:151 [in Coq.Logic.Eqdep_dec]
p:151 [in Coq.ZArith.BinInt]
p:151 [in Coq.Init.Specif]
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:153 [in Coq.Logic.Eqdep_dec]
P:153 [in Coq.Logic.EqdepFacts]
p:153 [in Coq.btauto.Algebra]
p:153 [in Coq.Init.Specif]
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.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.Numbers.Cyclic.Int63.Uint63]
P:156 [in Coq.Init.Specif]
p:156 [in Coq.Vectors.Fin]
p:157 [in Coq.PArith.BinPos]
p:157 [in Coq.btauto.Algebra]
p:157 [in Coq.ZArith.Zorder]
p:157 [in Coq.Structures.GenericMinMax]
p:158 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
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.micromega.RingMicromega]
p:159 [in Coq.btauto.Algebra]
p:159 [in Coq.setoid_ring.Ncring_polynom]
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.Init.Specif]
p:160 [in Coq.ZArith.Zorder]
p:160 [in Coq.Structures.GenericMinMax]
p:160 [in Coq.PArith.BinPosDef]
p:161 [in Coq.Logic.Eqdep_dec]
p:161 [in Coq.btauto.Algebra]
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.FSets.FSetCompat]
p:164 [in Coq.Vectors.VectorDef]
p:165 [in Coq.Vectors.Fin]
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.Init.Specif]
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:169 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:169 [in Coq.PArith.BinPos]
P:169 [in Coq.Init.Specif]
p:17 [in Coq.Arith.Div2]
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.Arith.Gt]
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.micromega.RingMicromega]
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.NArith.Ndigits]
p:172 [in Coq.Vectors.Fin]
p:172 [in Coq.setoid_ring.Ncring_polynom]
P:173 [in Coq.micromega.ZifyClasses]
P:173 [in Coq.Logic.EqdepFacts]
p:173 [in Coq.PArith.BinPos]
p:174 [in Coq.Logic.EqdepFacts]
p:174 [in Coq.PArith.BinPos]
p:174 [in Coq.Init.Specif]
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.Logic.EqdepFacts]
P:175 [in Coq.Logic.ChoiceFacts]
P:175 [in Coq.omega.OmegaLemmas]
p:175 [in Coq.Vectors.Fin]
p:175 [in Coq.ZArith.Znumtheory]
p:176 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:176 [in Coq.ZArith.BinInt]
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.Init.Specif]
P:177 [in Coq.ssr.ssrfun]
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:179 [in Coq.Logic.EqdepFacts]
p:179 [in Coq.ZArith.BinInt]
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.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.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.ssrfun]
P:180 [in Coq.omega.OmegaLemmas]
p:180 [in Coq.ZArith.Zorder]
p:180 [in Coq.Structures.GenericMinMax]
p:180 [in Coq.ZArith.Znumtheory]
p:181 [in Coq.PArith.BinPos]
p:181 [in Coq.ZArith.BinInt]
p:181 [in Coq.Init.Specif]
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.ZArith.Znumtheory]
p:182 [in Coq.QArith.QArith_base]
p:183 [in Coq.PArith.BinPos]
P:183 [in Coq.Logic.ChoiceFacts]
P:183 [in Coq.omega.OmegaLemmas]
p:183 [in Coq.ZArith.Zorder]
p:183 [in Coq.Structures.GenericMinMax]
P:183 [in Coq.Init.Logic]
P:183 [in Coq.Logic.ClassicalFacts]
p:183 [in Coq.Vectors.VectorDef]
p:184 [in Coq.MSets.MSetProperties]
P:184 [in Coq.Init.Specif]
P:184 [in Coq.ssr.ssrbool]
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.ssr.ssrfun]
p:186 [in Coq.ZArith.Zorder]
P:186 [in Coq.setoid_ring.Ncring_polynom]
p:186 [in Coq.ZArith.Znumtheory]
p:187 [in Coq.PArith.BinPos]
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:189 [in Coq.micromega.EnvRing]
p:189 [in Coq.Init.Specif]
p:189 [in Coq.FSets.FMapFullAVL]
p:189 [in Coq.ZArith.Zorder]
P:189 [in Coq.Init.Logic]
P:19 [in Coq.Logic.Classical_Pred_Type]
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.Numbers.Natural.Abstract.NLcm0]
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.Arith.Mult]
p:19 [in Coq.Numbers.Natural.Abstract.NGcd]
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.Zorder]
p:192 [in Coq.Structures.OrderedType]
P:192 [in Coq.Structures.GenericMinMax]
p:192 [in Coq.ZArith.Znumtheory]
p:193 [in Coq.Vectors.VectorSpec]
p:193 [in Coq.ZArith.BinInt]
P:193 [in Coq.Init.Specif]
P:194 [in Coq.Logic.Hurkens]
P:194 [in Coq.ssr.ssrfun]
p:194 [in Coq.setoid_ring.Ncring_polynom]
p:195 [in Coq.PArith.BinPos]
p:195 [in Coq.ZArith.Znumtheory]
p:196 [in Coq.ZArith.BinInt]
P:196 [in Coq.setoid_ring.Ring_polynom]
P:196 [in Coq.micromega.EnvRing]
P:196 [in Coq.omega.OmegaLemmas]
p:196 [in Coq.ZArith.Zorder]
p:196 [in Coq.ZArith.Znumtheory]
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:199 [in Coq.ZArith.Znumtheory]
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.Arith.Gt]
P:20 [in Coq.ZArith.Zcomplements]
P:20 [in Coq.Logic.WKL]
p:20 [in Coq.Logic.Adjointification]
P:20 [in Coq.Logic.WeakFan]
p:200 [in Coq.FSets.FMapFacts]
P:200 [in Coq.Logic.Hurkens]
P:200 [in Coq.omega.OmegaLemmas]
p:200 [in Coq.PArith.BinPosDef]
p:200 [in Coq.ZArith.Znumtheory]
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.Init.Specif]
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:203 [in Coq.ZArith.Znumtheory]
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.ZArith.Znumtheory]
p:205 [in Coq.micromega.ZMicromega]
p:206 [in Coq.Logic.EqdepFacts]
p:206 [in Coq.PArith.BinPos]
P:206 [in Coq.Init.Specif]
p:207 [in Coq.PArith.BinPos]
p:207 [in Coq.Reals.PSeries_reg]
p:207 [in Coq.PArith.BinPosDef]
P:208 [in Coq.Logic.EqdepFacts]
P:208 [in Coq.micromega.EnvRing]
P:208 [in Coq.FSets.FSetInterface]
p:208 [in Coq.PArith.BinPosDef]
p: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.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.Arith.Mult]
p:21 [in Coq.Logic.Adjointification]
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:210 [in Coq.ZArith.Znumtheory]
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.micromega.ZMicromega]
p:213 [in Coq.Logic.EqdepFacts]
p:213 [in Coq.PArith.BinPos]
p:213 [in Coq.micromega.EnvRing]
p:213 [in Coq.Init.Specif]
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:218 [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.Numbers.Natural.Abstract.NLcm0]
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.Numbers.Natural.Abstract.NGcd]
p:22 [in Coq.Logic.Adjointification]
p:22 [in Coq.Numbers.Cyclic.Int63.Sint63]
p:22 [in Coq.ZArith.Zcompare]
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:222 [in Coq.Logic.EqdepFacts]
P:222 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:222 [in Coq.micromega.ZMicromega]
p:223 [in Coq.Init.Specif]
p:224 [in Coq.ZArith.BinInt]
P:224 [in Coq.setoid_ring.Ring_polynom]
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.ZArith.BinInt]
P:225 [in Coq.FSets.FSetInterface]
p:226 [in Coq.Logic.EqdepFacts]
p:226 [in Coq.ZArith.BinInt]
p:226 [in Coq.micromega.ZMicromega]
p:227 [in Coq.PArith.BinPos]
p:227 [in Coq.ZArith.BinInt]
P:227 [in Coq.micromega.EnvRing]
P:227 [in Coq.Logic.ClassicalFacts]
P:228 [in Coq.setoid_ring.Ring_polynom]
P:228 [in Coq.Structures.GenericMinMax]
p:228 [in Coq.ZArith.Znumtheory]
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.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.Init.Specif]
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.Structures.GenericMinMax]
P:232 [in Coq.Vectors.VectorSpec]
P:232 [in Coq.Logic.EqdepFacts]
p:232 [in Coq.PArith.BinPos]
p:232 [in Coq.ZArith.Znumtheory]
p:232 [in Coq.micromega.ZMicromega]
p:233 [in Coq.Logic.EqdepFacts]
p:233 [in Coq.ZArith.Znumtheory]
P:234 [in Coq.setoid_ring.Ring_polynom]
P:234 [in Coq.micromega.EnvRing]
p:234 [in Coq.Init.Specif]
p:235 [in Coq.PArith.BinPos]
P:235 [in Coq.Bool.Bool]
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:237 [in Coq.Init.Specif]
P:238 [in Coq.Vectors.VectorSpec]
P:238 [in Coq.Bool.Bool]
P:239 [in Coq.setoid_ring.Ring_polynom]
P:239 [in Coq.Structures.GenericMinMax]
P:239 [in Coq.Logic.ClassicalFacts]
p:239 [in Coq.micromega.ZMicromega]
p:24 [in Coq.micromega.Ztac]
p:24 [in Coq.Numbers.Natural.Abstract.NSub]
p:24 [in Coq.PArith.BinPos]
P:24 [in Coq.Logic.Epsilon]
p:24 [in Coq.PArith.Pnat]
P:24 [in Coq.Logic.JMeq]
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.Init.Specif]
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.micromega.ZMicromega]
p:245 [in Coq.PArith.BinPos]
P:245 [in Coq.setoid_ring.Ring_polynom]
P:245 [in Coq.micromega.EnvRing]
P:245 [in Coq.Init.Specif]
P:246 [in Coq.Logic.EqdepFacts]
p:247 [in Coq.Logic.EqdepFacts]
p:247 [in Coq.PArith.BinPos]
P:248 [in Coq.setoid_ring.Ring_polynom]
P:248 [in Coq.micromega.EnvRing]
p:248 [in Coq.setoid_ring.Field_theory]
p:248 [in Coq.micromega.ZMicromega]
P:249 [in Coq.Vectors.VectorSpec]
p:249 [in Coq.PArith.BinPos]
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.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.Numbers.Natural.Abstract.NGcd]
p:25 [in Coq.QArith.QArith_base]
P:25 [in Coq.Logic.WeakFan]
p:250 [in Coq.Init.Specif]
p:250 [in Coq.QArith.QArith_base]
P:251 [in Coq.setoid_ring.Ring_polynom]
P:251 [in Coq.micromega.EnvRing]
P:252 [in Coq.Logic.EqdepFacts]
p:252 [in Coq.setoid_ring.Field_theory]
P:253 [in Coq.setoid_ring.Ring_polynom]
P:253 [in Coq.Init.Specif]
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.Reals.SeqProp]
p:254 [in Coq.QArith.QArith_base]
p:255 [in Coq.Init.Specif]
p:255 [in Coq.Reals.SeqProp]
P:256 [in Coq.setoid_ring.Ring_polynom]
p:256 [in Coq.NArith.BinNat]
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.micromega.ZMicromega]
p:258 [in Coq.Logic.EqdepFacts]
P:258 [in Coq.setoid_ring.Ring_polynom]
p:258 [in Coq.Reals.SeqProp]
p:258 [in Coq.QArith.QArith_base]
p:259 [in Coq.setoid_ring.Ring_polynom]
p:259 [in Coq.NArith.BinNat]
p:259 [in Coq.micromega.ZMicromega]
p:26 [in Coq.Reals.Runcountable]
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.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.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.NArith.BinNat]
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.Arith.PeanoNat]
P:265 [in Coq.Vectors.VectorDef]
p:266 [in Coq.PArith.BinPos]
p:266 [in Coq.micromega.EnvRing]
P:267 [in Coq.Logic.EqdepFacts]
p:267 [in Coq.Init.Specif]
p:268 [in Coq.PArith.BinPos]
P:268 [in Coq.micromega.EnvRing]
p:268 [in Coq.micromega.ZMicromega]
p:269 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:269 [in Coq.Logic.EqdepFacts]
P:269 [in Coq.Init.Specif]
p:27 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:27 [in Coq.QArith.Qcanon]
p:27 [in Coq.Numbers.Natural.Abstract.NSub]
p:27 [in Coq.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.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:270 [in Coq.PArith.BinPos]
P:270 [in Coq.MSets.MSetProperties]
P:270 [in Coq.Arith.PeanoNat]
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.FSets.FMapPositive]
p:272 [in Coq.PArith.BinPos]
p:273 [in Coq.Logic.EqdepFacts]
P:273 [in Coq.setoid_ring.Ring_polynom]
P:273 [in Coq.Logic.Hurkens]
p:273 [in Coq.FSets.FMapPositive]
p:274 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:274 [in Coq.PArith.BinPos]
p:274 [in Coq.Init.Specif]
p:275 [in Coq.FSets.FMapFacts]
P:275 [in Coq.Arith.PeanoNat]
p:275 [in Coq.FSets.FMapPositive]
p:276 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:276 [in Coq.PArith.BinPos]
p:276 [in Coq.ssr.ssrbool]
p:277 [in Coq.ZArith.BinInt]
p:277 [in Coq.Init.Specif]
p:278 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
p:278 [in Coq.PArith.BinPos]
P:278 [in Coq.setoid_ring.Ring_polynom]
p:278 [in Coq.micromega.EnvRing]
P:279 [in Coq.Init.Specif]
p:279 [in Coq.micromega.ZMicromega]
p:28 [in Coq.Logic.Eqdep_dec]
P:28 [in Coq.Logic.ClassicalEpsilon]
p:28 [in Coq.PArith.Pnat]
P:28 [in Coq.Logic.JMeq]
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.Reals.Rlogic]
p:28 [in Coq.Numbers.NatInt.NZAdd]
p:280 [in Coq.PArith.BinPos]
p:280 [in Coq.ZArith.BinInt]
P:280 [in Coq.Arith.PeanoNat]
p:281 [in Coq.micromega.EnvRing]
p:282 [in Coq.PArith.BinPos]
p:282 [in Coq.micromega.RingMicromega]
p:282 [in Coq.ssr.ssrbool]
p:282 [in Coq.FSets.FMapWeakList]
p:283 [in Coq.NArith.BinNat]
P:283 [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.micromega.RingMicromega]
p:285 [in Coq.ZArith.BinInt]
P:285 [in Coq.Init.Specif]
P:285 [in Coq.Sorting.Permutation]
p:285 [in Coq.Reals.Rtopology]
p:285 [in Coq.Lists.SetoidList]
p:286 [in Coq.PArith.BinPos]
p:286 [in Coq.QArith.QArith_base]
p:287 [in Coq.FSets.FSetBridge]
P:287 [in Coq.Vectors.VectorDef]
p:287 [in Coq.QArith.QArith_base]
p:288 [in Coq.PArith.BinPos]
p:288 [in Coq.micromega.RingMicromega]
P:288 [in Coq.FSets.FMapFacts]
p:288 [in Coq.micromega.ZMicromega]
p:288 [in Coq.Lists.SetoidList]
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.ZArith.Wf_Z]
P:29 [in Coq.Reals.Rsqrt_def]
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.FSets.FMapList]
p:290 [in Coq.micromega.ZMicromega]
p:290 [in Coq.Lists.SetoidList]
p:291 [in Coq.PArith.BinPos]
P:291 [in Coq.Init.Specif]
P:291 [in Coq.NArith.BinNat]
p:291 [in Coq.QArith.QArith_base]
p:292 [in Coq.Lists.SetoidList]
p:293 [in Coq.Vectors.VectorSpec]
p:293 [in Coq.QArith.QArith_base]
p:294 [in Coq.PArith.BinPos]
p:294 [in Coq.ZArith.BinInt]
p:294 [in Coq.Lists.SetoidList]
p:295 [in Coq.Reals.Rtopology]
p:296 [in Coq.PArith.BinPos]
P:296 [in Coq.micromega.EnvRing]
p:296 [in Coq.Init.Specif]
p:297 [in Coq.ssr.ssrbool]
P:298 [in Coq.Vectors.VectorDef]
p:299 [in Coq.PArith.BinPos]
p:299 [in Coq.Init.Specif]
P:299 [in Coq.Logic.Hurkens]
P:3 [in Coq.Arith.Le]
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.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.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.QArith.Qpower]
p:30 [in Coq.Numbers.Cyclic.Int63.Uint63]
P:30 [in Coq.Vectors.VectorDef]
P:300 [in Coq.Logic.ChoiceFacts]
p:301 [in Coq.PArith.BinPos]
P:301 [in Coq.Init.Specif]
P:302 [in Coq.Logic.Hurkens]
P:302 [in Coq.Arith.PeanoNat]
p:303 [in Coq.PArith.BinPos]
P:303 [in Coq.Logic.ChoiceFacts]
p:303 [in Coq.NArith.BinNat]
P:303 [in Coq.Init.Logic]
P:304 [in Coq.Lists.SetoidList]
p:305 [in Coq.PArith.BinPos]
P:305 [in Coq.Logic.Hurkens]
p:305 [in Coq.Reals.Rtopology]
p:305 [in Coq.micromega.ZMicromega]
p:306 [in Coq.ZArith.BinInt]
p:306 [in Coq.Init.Specif]
P:307 [in Coq.FSets.FSetBridge]
p:307 [in Coq.PArith.BinPos]
p:307 [in Coq.ZArith.BinInt]
p:307 [in Coq.ssr.ssrbool]
P:307 [in Coq.Arith.PeanoNat]
P:308 [in Coq.Logic.Hurkens]
p:308 [in Coq.NArith.BinNat]
p:309 [in Coq.PArith.BinPos]
p:309 [in Coq.ZArith.BinInt]
p:309 [in Coq.Init.Specif]
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.FSets.FSetProperties]
P:310 [in Coq.FSets.FSetBridge]
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:311 [in Coq.NArith.BinNat]
p:312 [in Coq.ZArith.BinInt]
P:312 [in Coq.Lists.List]
p:313 [in Coq.PArith.BinPos]
p:313 [in Coq.ZArith.BinInt]
p:313 [in Coq.Reals.Rtopology]
P:313 [in Coq.Init.Logic]
p:314 [in Coq.ZArith.BinInt]
p:315 [in Coq.PArith.BinPos]
p:315 [in Coq.ZArith.BinInt]
p:316 [in Coq.ZArith.BinInt]
P:316 [in Coq.Lists.List]
P:316 [in Coq.NArith.BinNat]
p:317 [in Coq.PArith.BinPos]
P:317 [in Coq.Logic.ChoiceFacts]
p:317 [in Coq.Init.Specif]
p:318 [in Coq.ZArith.BinInt]
p:319 [in Coq.PArith.BinPos]
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.Logic.JMeq]
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.Logic.WKL]
p:32 [in Coq.Numbers.Natural.Abstract.NGcd]
p:32 [in Coq.Numbers.NatInt.NZAdd]
p:320 [in Coq.ZArith.BinInt]
P:320 [in Coq.Logic.ChoiceFacts]
p:320 [in Coq.Init.Specif]
p:321 [in Coq.PArith.BinPos]
P:321 [in Coq.NArith.BinNat]
p:322 [in Coq.ZArith.BinInt]
P:322 [in Coq.Init.Specif]
p:323 [in Coq.PArith.BinPos]
p:323 [in Coq.ZArith.BinInt]
P:323 [in Coq.FSets.FMapFacts]
P:323 [in Coq.Init.Logic]
p:325 [in Coq.PArith.BinPos]
p:325 [in Coq.ZArith.BinInt]
p:326 [in Coq.PArith.BinPos]
p:326 [in Coq.setoid_ring.Ring_polynom]
p:327 [in Coq.ZArith.BinInt]
p:327 [in Coq.Init.Specif]
p:328 [in Coq.PArith.BinPos]
p:329 [in Coq.PArith.BinPos]
p:329 [in Coq.ZArith.BinInt]
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.ZArith.Wf_Z]
P:33 [in Coq.Reals.Rsqrt_def]
P:33 [in Coq.ssr.ssrbool]
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:330 [in Coq.Init.Specif]
P:330 [in Coq.Init.Logic]
p:331 [in Coq.PArith.BinPos]
p:331 [in Coq.setoid_ring.Ring_polynom]
P:331 [in Coq.FSets.FMapFacts]
p:331 [in Coq.Init.Specif]
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.Vectors.VectorSpec]
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.Vectors.VectorSpec]
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.Logic.Diaconescu]
p:34 [in Coq.micromega.Refl]
p:34 [in Coq.ZArith.Zcompare]
p:340 [in Coq.ZArith.BinInt]
P:340 [in Coq.setoid_ring.Ring_polynom]
p:340 [in Coq.micromega.EnvRing]
P:340 [in Coq.Init.Specif]
p:341 [in Coq.setoid_ring.Ring_polynom]
P:341 [in Coq.Logic.ChoiceFacts]
p:342 [in Coq.ZArith.BinInt]
p:343 [in Coq.ZArith.BinInt]
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:346 [in Coq.Init.Specif]
P:348 [in Coq.Vectors.VectorSpec]
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.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.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.Logic.ChoiceFacts]
p:357 [in Coq.ZArith.BinInt]
P:357 [in Coq.micromega.EnvRing]
p:358 [in Coq.PArith.BinPos]
p:358 [in Coq.ZArith.BinInt]
P:358 [in Coq.micromega.EnvRing]
P:358 [in Coq.Logic.ChoiceFacts]
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.Numbers.Natural.Abstract.NLcm0]
p:36 [in Coq.PArith.Pnat]
P:36 [in Coq.Logic.JMeq]
p:36 [in Coq.Numbers.Natural.Abstract.NLcm]
P:36 [in Coq.Reals.Rsqrt_def]
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.ZArith.BinInt]
P:360 [in Coq.Logic.ChoiceFacts]
p:360 [in Coq.Init.Specif]
p:361 [in Coq.PArith.BinPos]
p:361 [in Coq.ZArith.BinInt]
p:361 [in Coq.Reals.Rtopology]
P:362 [in Coq.FSets.FMapFacts]
P:362 [in Coq.micromega.EnvRing]
p: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.Init.Specif]
p:364 [in Coq.Reals.Rtopology]
p:365 [in Coq.ZArith.BinInt]
p:366 [in Coq.PArith.BinPos]
p:367 [in Coq.ZArith.BinInt]
p:367 [in Coq.Init.Specif]
p:368 [in Coq.micromega.EnvRing]
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.EqdepFacts]
p:37 [in Coq.PArith.BinPos]
p:37 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
P:37 [in Coq.ZArith.Wf_Z]
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.Reals.ClassicalDedekindReals]
p:37 [in Coq.ZArith.Zcompare]
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.Init.Specif]
p:372 [in Coq.micromega.ZMicromega]
p:373 [in Coq.ZArith.BinInt]
p:374 [in Coq.PArith.BinPos]
p:374 [in Coq.ZArith.BinInt]
P:374 [in Coq.Init.Specif]
P:374 [in Coq.Init.Logic]
p:375 [in Coq.ZArith.BinInt]
p:376 [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.ZArith.BinInt]
p:378 [in Coq.Init.Specif]
p:379 [in Coq.ZArith.BinInt]
p:379 [in Coq.FSets.FMapWeakList]
p:38 [in Coq.Reals.Cauchy_prod]
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:382 [in Coq.Init.Logic]
p:383 [in Coq.ZArith.BinInt]
p:384 [in Coq.PArith.BinPos]
p:384 [in Coq.Init.Specif]
p:385 [in Coq.ZArith.BinInt]
P:386 [in Coq.Init.Specif]
p:387 [in Coq.PArith.BinPos]
p:388 [in Coq.ZArith.BinInt]
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.NLcm0]
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:390 [in Coq.PArith.BinPos]
p:390 [in Coq.ZArith.BinInt]
p:391 [in Coq.Init.Specif]
p:394 [in Coq.PArith.BinPos]
P:394 [in Coq.Init.Specif]
P:394 [in Coq.Init.Logic]
p:396 [in Coq.micromega.ZMicromega]
p:397 [in Coq.PArith.BinPos]
p:398 [in Coq.Init.Specif]
P:398 [in Coq.Init.Logic]
p:4 [in Coq.Arith.Le]
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.Reals.Cauchy_prod]
p:40 [in Coq.PArith.Pnat]
P:40 [in Coq.Logic.JMeq]
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:401 [in Coq.Init.Specif]
p:403 [in Coq.PArith.BinPos]
P:404 [in Coq.Init.Logic]
p:406 [in Coq.PArith.BinPos]
p:406 [in Coq.Init.Specif]
P:408 [in Coq.Init.Logic]
P:409 [in Coq.Init.Specif]
p:41 [in Coq.Numbers.Integer.Abstract.ZAdd]
P:41 [in Coq.Sets.Finite_sets_facts]
p:41 [in Coq.PArith.BinPos]
p:41 [in Coq.ZArith.BinInt]
p:41 [in Coq.Numbers.Integer.Abstract.ZGcd]
P:41 [in Coq.setoid_ring.Ring_polynom]
p:41 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
P:41 [in Coq.micromega.EnvRing]
p:41 [in Coq.btauto.Algebra]
P:41 [in Coq.ZArith.Wf_Z]
P:41 [in Coq.ssr.ssrbool]
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.Structures.EqualitiesFacts]
p:410 [in Coq.PArith.BinPos]
p:410 [in Coq.MSets.MSetRBT]
p:412 [in Coq.MSets.MSetRBT]
p:413 [in Coq.PArith.BinPos]
p:413 [in Coq.Init.Specif]
p:414 [in Coq.ZArith.BinInt]
P:414 [in Coq.Init.Logic]
p:414 [in Coq.micromega.ZMicromega]
p:416 [in Coq.PArith.BinPos]
P:416 [in Coq.Init.Specif]
p:417 [in Coq.ssr.ssrbool]
P:418 [in Coq.setoid_ring.Ring_polynom]
p:42 [in Coq.Reals.Cauchy_prod]
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:420 [in Coq.PArith.BinPos]
P:420 [in Coq.Logic.ChoiceFacts]
p:420 [in Coq.ssr.ssrbool]
p:421 [in Coq.Init.Specif]
p:422 [in Coq.PArith.BinPos]
P:422 [in Coq.Logic.ChoiceFacts]
p:422 [in Coq.ssr.ssrbool]
P:424 [in Coq.Init.Specif]
p:425 [in Coq.PArith.BinPos]
p:425 [in Coq.ssr.ssrbool]
P:425 [in Coq.Init.Logic]
p:426 [in Coq.PArith.BinPos]
P:426 [in Coq.setoid_ring.Ring_polynom]
p:426 [in Coq.setoid_ring.Field_theory]
p:426 [in Coq.ssr.ssrbool]
p:427 [in Coq.PArith.BinPos]
p:428 [in Coq.PArith.BinPos]
p:429 [in Coq.Init.Specif]
p:429 [in Coq.setoid_ring.Field_theory]
p:429 [in Coq.ssr.ssrbool]
p:43 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:43 [in Coq.Reals.Cauchy_prod]
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.Logic.Adjointification]
p:43 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:430 [in Coq.PArith.BinPos]
p:430 [in Coq.ssr.ssrbool]
P:432 [in Coq.Init.Specif]
p:433 [in Coq.PArith.BinPos]
p:433 [in Coq.ssr.ssrbool]
p:433 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:435 [in Coq.ZArith.BinInt]
P:435 [in Coq.setoid_ring.Ring_polynom]
p:435 [in Coq.setoid_ring.Field_theory]
p:436 [in Coq.PArith.BinPos]
p:437 [in Coq.Init.Specif]
P:437 [in Coq.Init.Logic]
p:438 [in Coq.PArith.BinPos]
p:438 [in Coq.ZArith.BinInt]
p:438 [in Coq.setoid_ring.Field_theory]
p:439 [in Coq.FSets.FMapFacts]
p:439 [in Coq.Init.Logic]
P:44 [in Coq.Relations.Operators_Properties]
p:44 [in Coq.Reals.Cauchy_prod]
P:44 [in Coq.Sets.Finite_sets_facts]
p:44 [in Coq.PArith.BinPos]
P:44 [in Coq.Logic.JMeq]
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:440 [in Coq.PArith.BinPos]
p:440 [in Coq.setoid_ring.Ring_polynom]
p:440 [in Coq.Init.Specif]
p:441 [in Coq.FSets.FMapFacts]
p:441 [in Coq.ssr.ssrbool]
P:441 [in Coq.Init.Logic]
P:442 [in Coq.Init.Specif]
p:443 [in Coq.PArith.BinPos]
p:443 [in Coq.setoid_ring.Ring_polynom]
p:444 [in Coq.ZArith.BinInt]
P:444 [in Coq.Logic.ChoiceFacts]
p:444 [in Coq.ssr.ssrbool]
p:445 [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:447 [in Coq.ssr.ssrbool]
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.FSets.FMapList]
p:45 [in Coq.Reals.Cauchy_prod]
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.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:450 [in Coq.ssr.ssrbool]
p:450 [in Coq.Init.Logic]
p:452 [in Coq.PArith.BinPos]
p:453 [in Coq.ssr.ssrbool]
p:453 [in Coq.FSets.FMapList]
P:454 [in Coq.Init.Specif]
p:454 [in Coq.ssr.ssrbool]
p:455 [in Coq.PArith.BinPos]
p:456 [in Coq.ZArith.BinInt]
p:456 [in Coq.Init.Logic]
p:458 [in Coq.FSets.FMapWeakList]
p:459 [in Coq.Init.Specif]
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:460 [in Coq.Init.Logic]
p:462 [in Coq.Init.Specif]
p:463 [in Coq.PArith.BinPos]
p:463 [in Coq.ZArith.BinInt]
P:464 [in Coq.Init.Specif]
p:464 [in Coq.FSets.FMapWeakList]
p:464 [in Coq.Init.Logic]
p:465 [in Coq.FSets.FMapWeakList]
p:466 [in Coq.PArith.BinPos]
p:466 [in Coq.ZArith.BinInt]
p:466 [in Coq.setoid_ring.Field_theory]
P:466 [in Coq.Init.Logic]
P:468 [in Coq.setoid_ring.Ring_polynom]
p:468 [in Coq.setoid_ring.Field_theory]
p:468 [in Coq.ssr.ssrbool]
p:469 [in Coq.ZArith.BinInt]
p:469 [in Coq.Init.Specif]
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.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:470 [in Coq.Init.Logic]
p:472 [in Coq.ZArith.BinInt]
p:472 [in Coq.Init.Specif]
P:472 [in Coq.Init.Logic]
P:474 [in Coq.Init.Specif]
p:475 [in Coq.ZArith.BinInt]
p:475 [in Coq.FSets.FMapWeakList]
p:475 [in Coq.FSets.FMapList]
p:476 [in Coq.FSets.FMapWeakList]
p:476 [in Coq.FSets.FMapList]
p:477 [in Coq.PArith.BinPos]
P:477 [in Coq.setoid_ring.Ring_polynom]
p:477 [in Coq.ssr.ssrbool]
p:477 [in Coq.Init.Logic]
p:479 [in Coq.PArith.BinPos]
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.Init.Specif]
p:480 [in Coq.setoid_ring.Field_theory]
P:480 [in Coq.Init.Logic]
p:481 [in Coq.PArith.BinPos]
p:483 [in Coq.PArith.BinPos]
p:483 [in Coq.Init.Specif]
p:484 [in Coq.Init.Logic]
p:485 [in Coq.PArith.BinPos]
P:485 [in Coq.setoid_ring.Ring_polynom]
P:485 [in Coq.Init.Specif]
p:486 [in Coq.PArith.BinPos]
p:487 [in Coq.ZArith.BinInt]
P:487 [in Coq.Init.Logic]
p:488 [in Coq.setoid_ring.Ring_polynom]
p:49 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
P:49 [in Coq.Logic.Eqdep_dec]
p:49 [in Coq.Structures.OrdersLists]
P:49 [in Coq.FSets.FSetBridge]
p:49 [in Coq.Logic.EqdepFacts]
p:49 [in Coq.Numbers.HexadecimalPos]
P:49 [in Coq.setoid_ring.Ring_polynom]
p:49 [in Coq.ZArith.Zpow_facts]
p:49 [in Coq.Arith.Wf_nat]
P:49 [in Coq.ssr.ssrbool]
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:490 [in Coq.Init.Specif]
p:492 [in Coq.setoid_ring.Ring_polynom]
p:492 [in Coq.Init.Logic]
p:493 [in Coq.Init.Specif]
p:494 [in Coq.PArith.BinPos]
p:494 [in Coq.Init.Specif]
p:495 [in Coq.PArith.BinPos]
P:495 [in Coq.Init.Logic]
p:495 [in Coq.FSets.FMapList]
p:496 [in Coq.setoid_ring.Ring_polynom]
p:496 [in Coq.ssr.ssrbool]
p:496 [in Coq.FSets.FMapList]
P:497 [in Coq.Init.Specif]
p:498 [in Coq.FSets.FMapFacts]
p:499 [in Coq.setoid_ring.Ring_polynom]
p:499 [in Coq.Init.Logic]
p:5 [in Coq.Arith.Le]
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.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.Arith.Wf_nat]
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.Reals.Cos_rel]
P:501 [in Coq.setoid_ring.Ring_polynom]
P:502 [in Coq.Init.Logic]
P:503 [in Coq.Init.Specif]
p:504 [in Coq.ZArith.BinInt]
p:507 [in Coq.ZArith.BinInt]
p:507 [in Coq.Init.Logic]
P:509 [in Coq.Init.Specif]
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.Init.Logic]
p:511 [in Coq.setoid_ring.Ring_polynom]
p:511 [in Coq.Init.Specif]
p:512 [in Coq.ZArith.BinInt]
p:514 [in Coq.PArith.BinPos]
p:514 [in Coq.ZArith.BinInt]
p:515 [in Coq.setoid_ring.Ring_polynom]
p:515 [in Coq.Reals.RIneq]
p:515 [in Coq.Init.Logic]
p:516 [in Coq.ZArith.BinInt]
p:517 [in Coq.PArith.BinPos]
p:517 [in Coq.Init.Specif]
p:518 [in Coq.setoid_ring.Ring_polynom]
P:518 [in Coq.Init.Logic]
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.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:522 [in Coq.Init.Logic]
p:523 [in Coq.PArith.BinPos]
p:523 [in Coq.setoid_ring.Ring_polynom]
p:523 [in Coq.Init.Specif]
P:524 [in Coq.Init.Logic]
p:525 [in Coq.setoid_ring.Ring_polynom]
P:525 [in Coq.Init.Specif]
P:525 [in Coq.ssr.ssrbool]
p:526 [in Coq.PArith.BinPos]
P:527 [in Coq.setoid_ring.Ring_polynom]
p:527 [in Coq.Init.Specif]
p:529 [in Coq.PArith.BinPos]
p:529 [in Coq.Init.Logic]
P:53 [in Coq.FSets.FSetBridge]
p:53 [in Coq.PArith.BinPos]
P:53 [in Coq.setoid_ring.Ring_polynom]
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.Vectors.VectorDef]
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:533 [in Coq.Init.Logic]
p:534 [in Coq.Reals.RIneq]
p:535 [in Coq.PArith.BinPos]
P:535 [in Coq.ssr.ssrbool]
P:535 [in Coq.Init.Logic]
P:536 [in Coq.Init.Specif]
p:536 [in Coq.Reals.RIneq]
p:537 [in Coq.Reals.RIneq]
p:538 [in Coq.Reals.RIneq]
p:539 [in Coq.Init.Specif]
p:539 [in Coq.Reals.RIneq]
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.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:541 [in Coq.PArith.BinPos]
P:541 [in Coq.Init.Logic]
P:543 [in Coq.ssr.ssrbool]
p:544 [in Coq.Init.Specif]
P:546 [in Coq.Init.Specif]
P:547 [in Coq.Init.Logic]
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:552 [in Coq.Init.Specif]
p:552 [in Coq.Init.Logic]
p:555 [in Coq.PArith.BinPos]
P:555 [in Coq.Init.Specif]
p:555 [in Coq.Init.Logic]
p:557 [in Coq.PArith.BinPos]
P:557 [in Coq.Init.Logic]
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.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.Lists.SetoidList]
p:561 [in Coq.PArith.BinPos]
p:561 [in Coq.Init.Specif]
p:562 [in Coq.PArith.BinPos]
p:562 [in Coq.Init.Logic]
P:563 [in Coq.Init.Specif]
p:564 [in Coq.PArith.BinPos]
p:565 [in Coq.Init.Logic]
p:567 [in Coq.PArith.BinPos]
P:567 [in Coq.Init.Logic]
p:569 [in Coq.Init.Specif]
p:57 [in Coq.Numbers.Natural.Abstract.NSub]
p:57 [in Coq.Numbers.Integer.Abstract.ZAdd]
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:572 [in Coq.PArith.BinPos]
p:573 [in Coq.Init.Logic]
p:575 [in Coq.PArith.BinPos]
p:576 [in Coq.Init.Logic]
p:577 [in Coq.Init.Specif]
P:578 [in Coq.Init.Logic]
P:579 [in Coq.Init.Specif]
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:585 [in Coq.Init.Logic]
p:586 [in Coq.Init.Logic]
p:587 [in Coq.Init.Specif]
p:588 [in Coq.Init.Specif]
P:589 [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.ZArith.Int]
p:59 [in Coq.PArith.BinPosDef]
p:59 [in Coq.Reals.Abstract.ConstructiveSum]
p:59 [in Coq.rtauto.Rtauto]
P:591 [in Coq.Init.Specif]
P:593 [in Coq.ssr.ssrbool]
p:594 [in Coq.FSets.FMapWeakList]
p:595 [in Coq.PArith.BinPos]
P:595 [in Coq.ssr.ssrbool]
P:595 [in Coq.Init.Logic]
p:597 [in Coq.Init.Specif]
P:597 [in Coq.ssr.ssrbool]
p:598 [in Coq.PArith.BinPos]
p:598 [in Coq.Init.Specif]
P:599 [in Coq.ssr.ssrbool]
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: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.Numbers.NaryFunctions]
P:60 [in Coq.Classes.Morphisms]
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:60 [in Coq.Numbers.Natural.Abstract.NGcd]
P:601 [in Coq.Init.Specif]
P:601 [in Coq.Init.Logic]
P:602 [in Coq.ssr.ssrbool]
p:603 [in Coq.PArith.BinPos]
p:603 [in Coq.Init.Logic]
P:605 [in Coq.ssr.ssrbool]
p:606 [in Coq.PArith.BinPos]
p:608 [in Coq.PArith.BinPos]
p:609 [in Coq.PArith.BinPos]
p:609 [in Coq.Init.Specif]
P:609 [in Coq.ssr.ssrbool]
p:609 [in Coq.Init.Logic]
p:61 [in Coq.nsatz.NsatzTactic]
p:61 [in Coq.Logic.EqdepFacts]
p:61 [in Coq.Numbers.Natural.Abstract.NLcm0]
p:61 [in Coq.Arith.Wf_nat]
P:61 [in Coq.Logic.FunctionalExtensionality]
p:61 [in Coq.Numbers.Natural.Abstract.NLcm]
P:61 [in Coq.Reals.Rsqrt_def]
p:61 [in Coq.Numbers.NatInt.NZGcd]
p:61 [in Coq.ZArith.Int]
p:61 [in Coq.Init.Datatypes]
p:61 [in Coq.setoid_ring.Ring_theory]
p:61 [in Coq.Numbers.NatInt.NZMulOrder]
P:61 [in Coq.Logic.WKL]
p:61 [in Coq.PArith.BinPosDef]
p:610 [in Coq.PArith.BinPos]
p:611 [in Coq.PArith.BinPos]
P:611 [in Coq.Init.Logic]
p:613 [in Coq.PArith.BinPos]
P:613 [in Coq.Init.Specif]
P:613 [in Coq.ssr.ssrbool]
p:613 [in Coq.Init.Logic]
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.Lists.List]
p:616 [in Coq.FSets.FMapFacts]
P:617 [in Coq.ssr.ssrbool]
p:618 [in Coq.Lists.List]
p:618 [in Coq.FSets.FMapFacts]
p:619 [in Coq.PArith.BinPos]
p:619 [in Coq.Init.Specif]
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.JMeq]
P:62 [in Coq.Logic.Diaconescu]
P:62 [in Coq.FSets.FSetProperties]
p:620 [in Coq.FSets.FMapFacts]
p:620 [in Coq.Init.Logic]
p:622 [in Coq.FSets.FMapFacts]
P:622 [in Coq.Init.Logic]
P:623 [in Coq.Init.Specif]
P:623 [in Coq.ssr.ssrbool]
p:624 [in Coq.FSets.FMapFacts]
p:626 [in Coq.FSets.FMapFacts]
P:626 [in Coq.ssr.ssrbool]
p:626 [in Coq.Init.Logic]
p:627 [in Coq.FSets.FMapFacts]
p:628 [in Coq.FSets.FMapFacts]
P:628 [in Coq.Init.Logic]
p:63 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:63 [in Coq.Logic.ConstructiveEpsilon]
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:63 [in Coq.Numbers.Natural.Abstract.NGcd]
P:630 [in Coq.ssr.ssrbool]
p:630 [in Coq.Init.Logic]
p:631 [in Coq.Init.Specif]
P:635 [in Coq.Init.Specif]
p:636 [in Coq.Init.Logic]
P:639 [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.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:642 [in Coq.Init.Logic]
p:643 [in Coq.Init.Specif]
P:647 [in Coq.Init.Specif]
p:647 [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.Natural.Abstract.NLcm0]
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:650 [in Coq.Init.Specif]
p:653 [in Coq.Init.Logic]
p:658 [in Coq.Init.Specif]
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.MSets.MSetWeakList]
p:66 [in Coq.NArith.Ndigits]
p:66 [in Coq.Structures.EqualitiesFacts]
p:66 [in Coq.Numbers.DecimalPos]
p:66 [in Coq.Numbers.Natural.Abstract.NGcd]
p:66 [in Coq.Reals.Cos_rel]
P:660 [in Coq.Init.Specif]
p:660 [in Coq.Init.Logic]
P:663 [in Coq.FSets.FMapFacts]
P:665 [in Coq.Init.Logic]
p:666 [in Coq.Init.Specif]
p:667 [in Coq.Init.Specif]
P:669 [in Coq.Init.Specif]
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.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:671 [in Coq.Init.Logic]
P:674 [in Coq.Init.Logic]
p:676 [in Coq.Init.Specif]
P:68 [in Coq.Lists.Streams]
p:68 [in Coq.Numbers.Natural.Abstract.NSub]
p:68 [in Coq.PArith.BinPos]
p:68 [in Coq.Numbers.NaryFunctions]
P:68 [in Coq.Logic.JMeq]
p:68 [in Coq.Numbers.NatInt.NZGcd]
P:68 [in Coq.Logic.WKL]
p:680 [in Coq.Init.Specif]
p:680 [in Coq.Init.Logic]
P:682 [in Coq.Init.Specif]
P:682 [in Coq.Init.Logic]
p:688 [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.Strings.String]
p:69 [in Coq.Arith.Wf_nat]
p:69 [in Coq.Logic.JMeq]
P:69 [in Coq.MSets.MSetWeakList]
p:69 [in Coq.ZArith.Zpower]
p:69 [in Coq.Numbers.DecimalPos]
p:69 [in Coq.Numbers.Natural.Abstract.NGcd]
P:69 [in Coq.FSets.FSetProperties]
P:690 [in Coq.Init.Specif]
P:690 [in Coq.Init.Logic]
P:693 [in Coq.FSets.FMapFacts]
p:696 [in Coq.Init.Logic]
P:698 [in Coq.Init.Specif]
P:698 [in Coq.Init.Logic]
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.Numbers.Natural.Abstract.NAddOrder]
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.Logic.Adjointification]
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.Numbers.NaryFunctions]
P:70 [in Coq.Arith.Wf_nat]
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:705 [in Coq.Init.Specif]
p:706 [in Coq.Init.Logic]
p:707 [in Coq.Init.Logic]
p:709 [in Coq.Init.Specif]
P:709 [in Coq.MSets.MSetRBT]
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:710 [in Coq.Init.Logic]
P:711 [in Coq.Init.Specif]
P:711 [in Coq.MSets.MSetRBT]
p:716 [in Coq.Init.Logic]
p:717 [in Coq.Init.Logic]
p:718 [in Coq.Init.Specif]
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.Classes.CMorphisms]
p:72 [in Coq.ZArith.Zpower]
P:72 [in Coq.setoid_ring.Ncring_polynom]
p:72 [in Coq.btauto.Reflect]
p:72 [in Coq.rtauto.Rtauto]
P:720 [in Coq.Init.Logic]
p:722 [in Coq.Init.Specif]
P:724 [in Coq.Init.Specif]
p:726 [in Coq.Init.Logic]
P:729 [in Coq.ssr.ssrbool]
p:73 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:73 [in Coq.Numbers.Natural.Abstract.NSub]
p:73 [in Coq.Arith.Arith_prebase]
p:73 [in Coq.PArith.BinPos]
p:73 [in Coq.Numbers.HexadecimalPos]
P:73 [in Coq.Reals.MVT]
p:73 [in Coq.Strings.String]
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.Init.Logic]
p:73 [in Coq.PArith.BinPosDef]
P:730 [in Coq.Init.Logic]
p:733 [in Coq.Init.Specif]
p:737 [in Coq.Init.Specif]
p:738 [in Coq.Init.Logic]
P:739 [in Coq.Init.Specif]
p:74 [in Coq.Logic.ConstructiveEpsilon]
P:74 [in Coq.Arith.Wf_nat]
P:74 [in Coq.Logic.JMeq]
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:742 [in Coq.Init.Logic]
p:746 [in Coq.Init.Specif]
p:747 [in Coq.Init.Specif]
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.PArith.BinPosDef]
p:750 [in Coq.Init.Specif]
p:750 [in Coq.Init.Logic]
p:751 [in Coq.Init.Specif]
P:754 [in Coq.Init.Logic]
P:755 [in Coq.Init.Specif]
p:76 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:76 [in Coq.Numbers.Natural.Abstract.NSub]
p:76 [in Coq.Arith.Arith_prebase]
P:76 [in Coq.setoid_ring.Ring_polynom]
p:76 [in Coq.btauto.Algebra]
p:76 [in Coq.NArith.BinNat]
p:76 [in Coq.Structures.GenericMinMax]
P:76 [in Coq.setoid_ring.Ncring_polynom]
p:762 [in Coq.Init.Logic]
P:763 [in Coq.Init.Specif]
P:766 [in Coq.Init.Logic]
p:769 [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:771 [in Coq.Init.Specif]
p:774 [in Coq.Init.Specif]
p:777 [in Coq.Init.Logic]
P:779 [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.Abstract.ConstructiveLimits]
p:78 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:781 [in Coq.Init.Logic]
p:782 [in Coq.Init.Specif]
P:787 [in Coq.ssr.ssrbool]
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.NArith.BinNat]
p:79 [in Coq.Structures.GenericMinMax]
p:790 [in Coq.Init.Specif]
p:790 [in Coq.Init.Logic]
P:792 [in Coq.ssr.ssrbool]
P:795 [in Coq.Init.Specif]
P:795 [in Coq.Init.Logic]
p:798 [in Coq.Init.Logic]
p:799 [in Coq.Init.Specif]
p:8 [in Coq.Logic.EqdepFacts]
p:8 [in Coq.Floats.FloatLemmas]
p:8 [in Coq.Reals.ArithProp]
p:8 [in Coq.PArith.Pnat]
p:8 [in Coq.ZArith.Zmin]
P:8 [in Coq.ZArith.Wf_Z]
p:8 [in Coq.Arith.Plus]
P:8 [in Coq.Reals.Rbasic_fun]
p:8 [in Coq.Arith.Gt]
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:800 [in Coq.Init.Specif]
P:800 [in Coq.ssr.ssrbool]
p:802 [in Coq.Init.Logic]
p:805 [in Coq.Init.Specif]
p:806 [in Coq.Init.Specif]
P:808 [in Coq.Init.Specif]
P:808 [in Coq.ssr.ssrbool]
p:81 [in Coq.Arith.Arith_prebase]
p:81 [in Coq.Arith.Wf_nat]
p:81 [in Coq.btauto.Algebra]
P:81 [in Coq.Logic.FunctionalExtensionality]
P:81 [in Coq.Logic.ClassicalFacts]
p:81 [in Coq.Numbers.Cyclic.Int63.Uint63]
p:81 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
p:811 [in Coq.Init.Logic]
P:813 [in Coq.Init.Logic]
p:814 [in Coq.Init.Specif]
P:817 [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.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:820 [in Coq.Init.Logic]
P:822 [in Coq.Init.Logic]
p:823 [in Coq.Init.Specif]
P:825 [in Coq.Init.Specif]
p:828 [in Coq.Init.Logic]
p:83 [in Coq.Init.Specif]
P:830 [in Coq.Init.Logic]
p:831 [in Coq.Init.Specif]
P:833 [in Coq.Init.Specif]
p:837 [in Coq.Init.Logic]
p:839 [in Coq.Init.Specif]
P:84 [in Coq.Logic.Eqdep_dec]
p:84 [in Coq.Arith.Arith_prebase]
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.Init.Logic]
P:841 [in Coq.Init.Specif]
p:841 [in Coq.Init.Logic]
p:842 [in Coq.Init.Logic]
P:844 [in Coq.Init.Logic]
p:849 [in Coq.Init.Specif]
p:85 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
p:85 [in Coq.Logic.ConstructiveEpsilon]
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.Rsqrt_def]
p:85 [in Coq.micromega.OrderedRing]
p:85 [in Coq.Structures.GenericMinMax]
p:85 [in Coq.Numbers.NatInt.NZDiv]
p:850 [in Coq.Init.Specif]
P:852 [in Coq.Init.Logic]
P:853 [in Coq.Init.Specif]
p:859 [in Coq.Init.Specif]
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:860 [in Coq.Init.Specif]
P:860 [in Coq.Init.Logic]
P:863 [in Coq.Init.Specif]
p:867 [in Coq.Init.Logic]
p:87 [in Coq.Program.Wf]
p:87 [in Coq.Numbers.Integer.Abstract.ZAdd]
p:87 [in Coq.PArith.BinPos]
p:87 [in Coq.ZArith.Zorder]
p:87 [in Coq.Vectors.VectorDef]
p:871 [in Coq.Init.Specif]
p:871 [in Coq.Init.Logic]
P:873 [in Coq.Init.Logic]
P:875 [in Coq.Init.Specif]
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:880 [in Coq.Init.Logic]
p:881 [in Coq.Init.Specif]
p:884 [in Coq.Init.Logic]
P:885 [in Coq.Init.Specif]
P:886 [in Coq.Init.Logic]
p:89 [in Coq.Arith.Arith_prebase]
P:89 [in Coq.PArith.BinPos]
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:893 [in Coq.Init.Specif]
p:895 [in Coq.Init.Logic]
P:897 [in Coq.Init.Specif]
p:899 [in Coq.Init.Logic]
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.Arith.Mult]
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.Numbers.NaryFunctions]
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:90 [in Coq.Init.Logic]
P:901 [in Coq.Init.Logic]
p:905 [in Coq.Init.Specif]
p:908 [in Coq.Init.Logic]
P:909 [in Coq.Init.Specif]
p:909 [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:912 [in Coq.Init.Specif]
p:912 [in Coq.Init.Logic]
p:913 [in Coq.Init.Logic]
P:917 [in Coq.Init.Logic]
p:92 [in Coq.Reals.Abstract.ConstructiveReals]
p:92 [in Coq.Numbers.Natural.Abstract.NSub]
p:92 [in Coq.Arith.Arith_prebase]
P:92 [in Coq.setoid_ring.Ring_polynom]
p:92 [in Coq.Numbers.NaryFunctions]
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:920 [in Coq.Init.Specif]
P:922 [in Coq.Init.Specif]
P:925 [in Coq.Init.Logic]
p:928 [in Coq.Init.Specif]
p:929 [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:931 [in Coq.Init.Specif]
P:933 [in Coq.Init.Logic]
p:936 [in Coq.Init.Logic]
p:938 [in Coq.Init.Specif]
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:942 [in Coq.Init.Specif]
P:944 [in Coq.Init.Specif]
p:944 [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.PArith.BinPosDef]
p:950 [in Coq.Init.Logic]
P:952 [in Coq.Init.Specif]
P:955 [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.Init.Logic]
p:96 [in Coq.PArith.BinPosDef]
P:96 [in Coq.FSets.FSetProperties]
P:960 [in Coq.Init.Specif]
p:960 [in Coq.Init.Logic]
p:965 [in Coq.Init.Logic]
p:966 [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.Arith.Arith_prebase]
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.Ranalysis5]
p:97 [in Coq.Reals.Abstract.ConstructiveMinMax]
p:971 [in Coq.Init.Specif]
P:973 [in Coq.Init.Specif]
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:984 [in Coq.Init.Specif]
P:986 [in Coq.Init.Specif]
P:987 [in Coq.Lists.List]
p:99 [in Coq.Numbers.Integer.Abstract.ZAdd]
P:99 [in Coq.Logic.FunctionalExtensionality]
P:99 [in Coq.Sorting.CPermutation]
p:99 [in Coq.QArith.Qpower]
P:991 [in Coq.Lists.List]
P:995 [in Coq.Lists.List]
p:995 [in Coq.Init.Specif]
P:999 [in Coq.Lists.List]
p:999 [in Coq.Init.Specif]
| 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 | (73252 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 | (1016 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 | (47569 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 | (800 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 | (1555 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 | (592 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 | (11846 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 | (959 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 | (629 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 | (308 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 | (475 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 | (494 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 | (912 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 | (1503 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 | (4428 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 | (166 entries) |