| 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) |
F (binder)
fab:33 [in Coq.Numbers.NaryFunctions]fct:113 [in Coq.micromega.Tauto]
fct:645 [in Coq.micromega.Tauto]
fe1:291 [in Coq.setoid_ring.Field_theory]
fe1:324 [in Coq.setoid_ring.Field_theory]
fe1:332 [in Coq.setoid_ring.Field_theory]
fe1:341 [in Coq.setoid_ring.Field_theory]
fe1:348 [in Coq.setoid_ring.Field_theory]
fe1:354 [in Coq.setoid_ring.Field_theory]
fe1:365 [in Coq.setoid_ring.Field_theory]
fe2:292 [in Coq.setoid_ring.Field_theory]
fe2:325 [in Coq.setoid_ring.Field_theory]
fe2:333 [in Coq.setoid_ring.Field_theory]
fe2:342 [in Coq.setoid_ring.Field_theory]
fe2:349 [in Coq.setoid_ring.Field_theory]
fe2:355 [in Coq.setoid_ring.Field_theory]
fe2:366 [in Coq.setoid_ring.Field_theory]
fe:289 [in Coq.setoid_ring.Field_theory]
fe:298 [in Coq.setoid_ring.Field_theory]
fe:313 [in Coq.setoid_ring.Field_theory]
fe:319 [in Coq.setoid_ring.Field_theory]
ff2:351 [in Coq.micromega.Tauto]
ff:47 [in Coq.micromega.QMicromega]
fF:82 [in Coq.ssr.ssrbool]
ff:87 [in Coq.micromega.RMicromega]
ff:99 [in Coq.micromega.RMicromega]
fg_id:38 [in Coq.Logic.Adjointification]
fg_id:17 [in Coq.Logic.Adjointification]
filter:97 [in Coq.Reals.Abstract.ConstructiveSum]
first_index:49 [in Coq.Reals.Runcountable]
fi:91 [in Coq.FSets.FSetPositive]
fi:91 [in Coq.MSets.MSetPositive]
flex:49 [in Coq.ssr.ssreflect]
fl:21 [in Coq.btauto.Reflect]
fl:24 [in Coq.btauto.Reflect]
fl:4 [in Coq.funind.Recdef]
fl:74 [in Coq.btauto.Reflect]
fn':434 [in Coq.Reals.Ranalysis5]
fn1:19 [in Coq.Lists.StreamMemo]
fn:1 [in Coq.Reals.Rtrigo_reg]
fn:1 [in Coq.Reals.Rtrigo1]
fn:1 [in Coq.Reals.SeqSeries]
fn:101 [in Coq.Reals.PSeries_reg]
fn:117 [in Coq.Reals.PSeries_reg]
fn:126 [in Coq.Reals.PSeries_reg]
fn:132 [in Coq.Reals.PSeries_reg]
fn:14 [in Coq.Program.Subset]
fn:144 [in Coq.Reals.PartSum]
fn:158 [in Coq.Reals.PartSum]
fn:17 [in Coq.Lists.StreamMemo]
fn:43 [in Coq.Reals.PSeries_reg]
fn:433 [in Coq.Reals.Ranalysis5]
fn:51 [in Coq.Reals.PSeries_reg]
fn:59 [in Coq.Reals.PSeries_reg]
fn:61 [in Coq.Reals.PSeries_reg]
fn:68 [in Coq.Reals.PSeries_reg]
fn:9 [in Coq.Program.Subset]
fn:90 [in Coq.Reals.PSeries_reg]
fold:242 [in Coq.FSets.FSetBridge]
found:22 [in Coq.Logic.ConstructiveEpsilon]
found:24 [in Coq.Logic.ConstructiveEpsilon]
found:66 [in Coq.Logic.ConstructiveEpsilon]
found:67 [in Coq.Logic.ConstructiveEpsilon]
fo:119 [in Coq.ssr.ssrfun]
fo:315 [in Coq.ssr.ssrfun]
frame:126 [in Coq.ssr.ssreflect]
fr:22 [in Coq.btauto.Reflect]
fr:25 [in Coq.btauto.Reflect]
fr:324 [in Coq.micromega.ZMicromega]
fr:381 [in Coq.micromega.ZMicromega]
fr:389 [in Coq.micromega.ZMicromega]
fr:393 [in Coq.micromega.ZMicromega]
fr:75 [in Coq.btauto.Reflect]
fS2':32 [in Coq.NArith.BinNat]
fS2:25 [in Coq.NArith.BinNat]
fS2:319 [in Coq.NArith.BinNat]
fS2:324 [in Coq.NArith.BinNat]
fT:81 [in Coq.ssr.ssrbool]
fv:419 [in Coq.setoid_ring.Ring_polynom]
fv:427 [in Coq.setoid_ring.Ring_polynom]
fv:434 [in Coq.setoid_ring.Ring_polynom]
fv:470 [in Coq.setoid_ring.Ring_polynom]
fv:478 [in Coq.setoid_ring.Ring_polynom]
fv:486 [in Coq.setoid_ring.Ring_polynom]
fv:502 [in Coq.setoid_ring.Ring_polynom]
fv:528 [in Coq.setoid_ring.Ring_polynom]
fv:67 [in Coq.nsatz.NsatzTactic]
fxnz:128 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
F_sub:130 [in Coq.Program.Wf]
f_sub:34 [in Coq.Program.Wf]
f_eq_g:423 [in Coq.Reals.Ranalysis5]
f_decr:417 [in Coq.Reals.Ranalysis5]
f_eq_g:406 [in Coq.Reals.Ranalysis5]
f_incr:400 [in Coq.Reals.Ranalysis5]
f_derivable:355 [in Coq.Reals.Ranalysis5]
f_decr:353 [in Coq.Reals.Ranalysis5]
f_eq_g:348 [in Coq.Reals.Ranalysis5]
f_derivable:337 [in Coq.Reals.Ranalysis5]
f_incr:335 [in Coq.Reals.Ranalysis5]
f_eq_g:330 [in Coq.Reals.Ranalysis5]
f_adjoint:33 [in Coq.Logic.Adjointification]
f_adjoint_at_gb:19 [in Coq.Logic.Adjointification]
f'':331 [in Coq.ssr.ssrfun]
f'':672 [in Coq.ssr.ssrbool]
f'':673 [in Coq.ssr.ssrbool]
f'':675 [in Coq.ssr.ssrbool]
f':120 [in Coq.micromega.RingMicromega]
f':146 [in Coq.micromega.Tauto]
f':155 [in Coq.Reals.PSeries_reg]
f':192 [in Coq.Reals.MVT]
f':218 [in Coq.micromega.Tauto]
f':24 [in Coq.Numbers.DecimalQ]
f':24 [in Coq.Numbers.HexadecimalQ]
f':247 [in Coq.micromega.Tauto]
f':253 [in Coq.micromega.Tauto]
f':259 [in Coq.micromega.Tauto]
f':265 [in Coq.micromega.Tauto]
f':27 [in Coq.FSets.FSetFacts]
f':310 [in Coq.ssr.ssrfun]
f':311 [in Coq.ssr.ssrfun]
f':313 [in Coq.ssr.ssrfun]
f':317 [in Coq.ssr.ssrfun]
f':319 [in Coq.ssr.ssrfun]
f':321 [in Coq.ssr.ssrfun]
f':329 [in Coq.ssr.ssrfun]
f':33 [in Coq.MSets.MSetFacts]
f':330 [in Coq.ssr.ssrfun]
f':338 [in Coq.ssr.ssrfun]
f':361 [in Coq.micromega.ZMicromega]
f':41 [in Coq.Reals.MVT]
f':44 [in Coq.NArith.BinNat]
f':553 [in Coq.micromega.Tauto]
f':556 [in Coq.micromega.Tauto]
f':59 [in Coq.Reals.MVT]
f':740 [in Coq.ssr.ssrbool]
f':751 [in Coq.ssr.ssrbool]
f':765 [in Coq.ssr.ssrbool]
f':95 [in Coq.ssr.ssrfun]
f0:20 [in Coq.Lists.StreamMemo]
f0:21 [in Coq.NArith.BinNat]
f0:317 [in Coq.NArith.BinNat]
f0:322 [in Coq.NArith.BinNat]
f0:37 [in Coq.NArith.BinNat]
F0:66 [in Coq.Reals.NewtonInt]
F0:85 [in Coq.Reals.NewtonInt]
F0:91 [in Coq.Reals.NewtonInt]
f1:1 [in Coq.Reals.Ranalysis1]
f1:1 [in Coq.Reals.Ranalysis3]
f1:106 [in Coq.Reals.Ranalysis1]
f1:106 [in Coq.micromega.RingMicromega]
f1:109 [in Coq.Reals.Ranalysis1]
f1:12 [in Coq.Reals.Ranalysis1]
f1:122 [in Coq.micromega.RingMicromega]
f1:126 [in Coq.micromega.RingMicromega]
f1:14 [in Coq.Reals.Ranalysis2]
f1:149 [in Coq.micromega.Tauto]
f1:15 [in Coq.Reals.Ranalysis1]
f1:157 [in Coq.micromega.Tauto]
f1:159 [in Coq.micromega.Tauto]
f1:169 [in Coq.micromega.Tauto]
f1:173 [in Coq.micromega.Tauto]
f1:177 [in Coq.micromega.Tauto]
f1:181 [in Coq.micromega.Tauto]
f1:209 [in Coq.Reals.Ranalysis1]
f1:21 [in Coq.Reals.Ranalysis1]
f1:22 [in Coq.Reals.Ranalysis3]
f1:229 [in Coq.micromega.Tauto]
f1:25 [in Coq.Reals.Ranalysis3]
f1:251 [in Coq.Reals.Ranalysis1]
f1:264 [in Coq.Reals.Ranalysis1]
f1:277 [in Coq.Reals.Ranalysis1]
f1:28 [in Coq.Reals.Ranalysis3]
f1:307 [in Coq.micromega.Tauto]
f1:312 [in Coq.micromega.Tauto]
f1:314 [in Coq.Reals.Ranalysis1]
f1:317 [in Coq.micromega.Tauto]
f1:322 [in Coq.micromega.Tauto]
f1:330 [in Coq.Reals.Ranalysis1]
f1:333 [in Coq.Reals.Ranalysis1]
f1:335 [in Coq.micromega.Tauto]
f1:336 [in Coq.Reals.Ranalysis1]
f1:339 [in Coq.micromega.Tauto]
f1:344 [in Coq.micromega.Tauto]
f1:345 [in Coq.Reals.Ranalysis1]
f1:347 [in Coq.micromega.Tauto]
f1:349 [in Coq.Reals.Ranalysis1]
f1:35 [in Coq.Reals.Ranalysis2]
f1:351 [in Coq.Reals.Ranalysis1]
f1:352 [in Coq.micromega.Tauto]
f1:353 [in Coq.Reals.Ranalysis1]
f1:358 [in Coq.micromega.Tauto]
f1:359 [in Coq.Reals.Ranalysis1]
f1:361 [in Coq.micromega.Tauto]
f1:371 [in Coq.micromega.Tauto]
f1:372 [in Coq.micromega.Tauto]
f1:376 [in Coq.Reals.Ranalysis1]
f1:376 [in Coq.micromega.Tauto]
f1:380 [in Coq.micromega.Tauto]
f1:381 [in Coq.Reals.Ranalysis1]
f1:386 [in Coq.Reals.Ranalysis1]
f1:403 [in Coq.micromega.Tauto]
f1:407 [in Coq.micromega.Tauto]
f1:411 [in Coq.micromega.Tauto]
f1:418 [in Coq.micromega.Tauto]
f1:450 [in Coq.micromega.Tauto]
f1:452 [in Coq.micromega.Tauto]
f1:459 [in Coq.micromega.Tauto]
f1:46 [in Coq.Reals.Ranalysis2]
f1:469 [in Coq.micromega.Tauto]
f1:479 [in Coq.micromega.Tauto]
f1:489 [in Coq.micromega.Tauto]
f1:5 [in Coq.Reals.Ranalysis2]
f1:588 [in Coq.micromega.Tauto]
f1:6 [in Coq.Reals.Ranalysis1]
f1:60 [in Coq.Reals.Ranalysis1]
f1:605 [in Coq.micromega.Tauto]
f1:65 [in Coq.Reals.Ranalysis1]
F1:67 [in Coq.Reals.NewtonInt]
f1:68 [in Coq.Reals.Ranalysis1]
f1:7 [in Coq.Numbers.Natural.Abstract.NIso]
f1:71 [in Coq.Floats.SpecFloat]
f1:79 [in Coq.Floats.SpecFloat]
f1:81 [in Coq.Floats.SpecFloat]
f1:82 [in Coq.Reals.Ranalysis1]
f1:83 [in Coq.Floats.SpecFloat]
f1:84 [in Coq.Reals.Ranalysis1]
F1:86 [in Coq.Reals.NewtonInt]
f1:87 [in Coq.Reals.Ranalysis1]
f1:87 [in Coq.ssr.ssreflect]
F1:92 [in Coq.Reals.NewtonInt]
f1:94 [in Coq.Reals.Ranalysis1]
f1:97 [in Coq.Reals.Ranalysis1]
f1:99 [in Coq.Reals.Ranalysis1]
f1:99 [in Coq.micromega.RingMicromega]
f2':30 [in Coq.NArith.BinNat]
f2:100 [in Coq.Reals.Ranalysis1]
f2:100 [in Coq.micromega.RingMicromega]
f2:107 [in Coq.Reals.Ranalysis1]
f2:107 [in Coq.micromega.RingMicromega]
f2:110 [in Coq.Reals.Ranalysis1]
f2:123 [in Coq.micromega.RingMicromega]
f2:127 [in Coq.micromega.RingMicromega]
f2:13 [in Coq.Reals.Ranalysis1]
f2:15 [in Coq.Reals.Ranalysis2]
f2:150 [in Coq.micromega.Tauto]
f2:158 [in Coq.micromega.Tauto]
f2:16 [in Coq.Reals.Ranalysis1]
f2:160 [in Coq.micromega.Tauto]
f2:170 [in Coq.micromega.Tauto]
f2:174 [in Coq.micromega.Tauto]
f2:178 [in Coq.micromega.Tauto]
f2:182 [in Coq.micromega.Tauto]
f2:2 [in Coq.Reals.Ranalysis1]
f2:2 [in Coq.Reals.Ranalysis3]
f2:210 [in Coq.Reals.Ranalysis1]
f2:22 [in Coq.Reals.Ranalysis1]
f2:23 [in Coq.NArith.BinNat]
f2:23 [in Coq.Reals.Ranalysis3]
f2:230 [in Coq.micromega.Tauto]
f2:25 [in Coq.Reals.Ranalysis2]
f2:252 [in Coq.Reals.Ranalysis1]
f2:26 [in Coq.Reals.Ranalysis3]
f2:265 [in Coq.Reals.Ranalysis1]
f2:278 [in Coq.Reals.Ranalysis1]
f2:29 [in Coq.Reals.Ranalysis3]
f2:308 [in Coq.micromega.Tauto]
f2:313 [in Coq.micromega.Tauto]
f2:315 [in Coq.Reals.Ranalysis1]
f2:318 [in Coq.NArith.BinNat]
f2:323 [in Coq.NArith.BinNat]
f2:323 [in Coq.micromega.Tauto]
f2:331 [in Coq.Reals.Ranalysis1]
f2:334 [in Coq.Reals.Ranalysis1]
f2:336 [in Coq.micromega.Tauto]
f2:337 [in Coq.Reals.Ranalysis1]
f2:340 [in Coq.micromega.Tauto]
f2:345 [in Coq.micromega.Tauto]
f2:346 [in Coq.Reals.Ranalysis1]
f2:348 [in Coq.micromega.Tauto]
f2:350 [in Coq.Reals.Ranalysis1]
f2:352 [in Coq.Reals.Ranalysis1]
f2:354 [in Coq.Reals.Ranalysis1]
f2:359 [in Coq.micromega.Tauto]
f2:36 [in Coq.Reals.Ranalysis2]
f2:360 [in Coq.Reals.Ranalysis1]
f2:362 [in Coq.micromega.Tauto]
f2:377 [in Coq.Reals.Ranalysis1]
f2:377 [in Coq.micromega.Tauto]
f2:381 [in Coq.micromega.Tauto]
f2:382 [in Coq.Reals.Ranalysis1]
f2:387 [in Coq.Reals.Ranalysis1]
f2:404 [in Coq.micromega.Tauto]
f2:408 [in Coq.micromega.Tauto]
f2:412 [in Coq.micromega.Tauto]
f2:419 [in Coq.micromega.Tauto]
f2:451 [in Coq.micromega.Tauto]
f2:453 [in Coq.micromega.Tauto]
f2:460 [in Coq.micromega.Tauto]
f2:47 [in Coq.Reals.Ranalysis2]
f2:470 [in Coq.micromega.Tauto]
f2:480 [in Coq.micromega.Tauto]
f2:490 [in Coq.micromega.Tauto]
f2:590 [in Coq.micromega.Tauto]
f2:6 [in Coq.Reals.Ranalysis2]
f2:606 [in Coq.micromega.Tauto]
f2:61 [in Coq.Reals.Ranalysis1]
f2:66 [in Coq.Reals.Ranalysis1]
f2:69 [in Coq.Reals.Ranalysis1]
f2:7 [in Coq.Reals.Ranalysis1]
f2:72 [in Coq.Floats.SpecFloat]
f2:78 [in Coq.PArith.BinPos]
f2:8 [in Coq.Numbers.Natural.Abstract.NIso]
f2:80 [in Coq.Floats.SpecFloat]
f2:82 [in Coq.Floats.SpecFloat]
f2:83 [in Coq.Reals.Ranalysis1]
f2:84 [in Coq.Floats.SpecFloat]
f2:85 [in Coq.Reals.Ranalysis1]
f2:88 [in Coq.Reals.Ranalysis1]
f2:88 [in Coq.ssr.ssreflect]
f2:95 [in Coq.Reals.Ranalysis1]
f2:98 [in Coq.Reals.Ranalysis1]
f:1 [in Coq.Numbers.Natural.Abstract.NIso]
f:1 [in Coq.Reals.Ranalysis4]
f:1 [in Coq.Floats.FloatLemmas]
f:1 [in Coq.Reals.MVT]
f:1 [in Coq.Reals.Rprod]
f:1 [in Coq.Floats.FloatOps]
f:1 [in Coq.Reals.RiemannInt]
f:1 [in Coq.Reals.NewtonInt]
f:1 [in Coq.Reals.Ranalysis5]
f:1 [in Coq.Logic.PropFacts]
f:10 [in Coq.Reals.Ranalysis1]
f:10 [in Coq.Init.Decimal]
f:10 [in Coq.Logic.SetoidChoice]
f:10 [in Coq.Init.Hexadecimal]
f:10 [in Coq.Reals.NewtonInt]
f:10 [in Coq.Sets.Uniset]
f:10 [in Coq.Sets.Image]
f:10 [in Coq.Numbers.Natural.Abstract.NStrongRec]
f:100 [in Coq.MSets.MSetEqProperties]
f:100 [in Coq.FSets.FSetEqProperties]
f:100 [in Coq.MSets.MSetRBT]
f:100 [in Coq.Reals.Rtopology]
f:101 [in Coq.Reals.Ranalysis1]
F:101 [in Coq.rtauto.Bintree]
f:101 [in Coq.Reals.RiemannInt_SF]
f:1011 [in Coq.Init.Specif]
f:102 [in Coq.Reals.Ranalysis1]
f:102 [in Coq.FSets.FMapFacts]
f:102 [in Coq.MSets.MSetWeakList]
f:102 [in Coq.ssr.ssrfun]
f:102 [in Coq.Reals.NewtonInt]
f:102 [in Coq.FSets.FSetPositive]
f:102 [in Coq.MSets.MSetRBT]
f:102 [in Coq.micromega.ZMicromega]
f:102 [in Coq.FSets.FSetCompat]
f:1031 [in Coq.Lists.List]
f:104 [in Coq.Reals.Ranalysis1]
f:104 [in Coq.Reals.RiemannInt_SF]
f:104 [in Coq.micromega.Tauto]
f:104 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:1042 [in Coq.Lists.List]
f:1046 [in Coq.Lists.List]
f:105 [in Coq.Reals.MVT]
f:105 [in Coq.FSets.FMapInterface]
f:105 [in Coq.micromega.RMicromega]
f:105 [in Coq.FSets.FSetCompat]
f:1057 [in Coq.Lists.List]
f:106 [in Coq.Reals.Rtopology]
f:106 [in Coq.Structures.GenericMinMax]
f:106 [in Coq.QArith.QArith_base]
f:1068 [in Coq.Lists.List]
f:107 [in Coq.Reals.Rderiv]
f:107 [in Coq.Classes.Morphisms]
f:107 [in Coq.Logic.FunctionalExtensionality]
f:107 [in Coq.Logic.ClassicalFacts]
f:107 [in Coq.Lists.SetoidList]
f:107 [in Coq.FSets.FSetCompat]
f:1078 [in Coq.Lists.List]
f:108 [in Coq.Reals.MVT]
f:108 [in Coq.Reals.NewtonInt]
f:1083 [in Coq.Init.Specif]
f:1084 [in Coq.Lists.List]
f:1089 [in Coq.Init.Specif]
f:109 [in Coq.Reals.MVT]
f:109 [in Coq.FSets.FMapFacts]
f:109 [in Coq.Logic.FinFun]
f:109 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:1094 [in Coq.Init.Specif]
f:11 [in Coq.Floats.PrimFloat]
f:11 [in Coq.Numbers.DecimalQ]
f:11 [in Coq.Numbers.Natural.Abstract.NAxioms]
f:11 [in Coq.Program.Combinators]
f:11 [in Coq.Numbers.HexadecimalQ]
f:11 [in Coq.Reals.ClassicalDedekindReals]
f:110 [in Coq.MSets.MSetRBT]
f:110 [in Coq.Reals.Rlimit]
f:110 [in Coq.FSets.FSetCompat]
f:1103 [in Coq.Init.Specif]
f:111 [in Coq.Reals.Ranalysis1]
f:111 [in Coq.Logic.ChoiceFacts]
f:111 [in Coq.Reals.Rtopology]
f:111 [in Coq.Structures.GenericMinMax]
f:111 [in Coq.Reals.RList]
f:112 [in Coq.Reals.RiemannInt]
f:112 [in Coq.Logic.FinFun]
f:112 [in Coq.Lists.SetoidList]
f:113 [in Coq.PArith.BinPos]
f:113 [in Coq.FSets.FMapInterface]
f:113 [in Coq.Reals.Rtopology]
f:113 [in Coq.Numbers.Integer.Abstract.ZBits]
f:113 [in Coq.FSets.FSetCompat]
f:114 [in Coq.Logic.ClassicalFacts]
f:114 [in Coq.Reals.Abstract.ConstructiveMinMax]
f:114 [in Coq.micromega.Tauto]
f:114 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:115 [in Coq.Reals.Rderiv]
f:115 [in Coq.micromega.RMicromega]
f:116 [in Coq.FSets.FSetDecide]
f:116 [in Coq.MSets.MSetEqProperties]
f:116 [in Coq.MSets.MSetDecide]
f:116 [in Coq.FSets.FMapAVL]
f:116 [in Coq.FSets.FSetEqProperties]
f:116 [in Coq.FSets.FSetCompat]
f:117 [in Coq.Reals.Ranalysis1]
f:117 [in Coq.Logic.ChoiceFacts]
f:117 [in Coq.Reals.Ranalysis5]
f:118 [in Coq.Reals.MVT]
f:118 [in Coq.Reals.Rlimit]
f:118 [in Coq.micromega.RMicromega]
f:118 [in Coq.Logic.FinFun]
f:119 [in Coq.micromega.RingMicromega]
f:119 [in Coq.Vectors.Fin]
f:119 [in Coq.micromega.Tauto]
f:119 [in Coq.FSets.FSetCompat]
f:12 [in Coq.Reals.Rderiv]
f:12 [in Coq.Wellfounded.Well_Ordering]
f:12 [in Coq.Init.Decimal]
f:12 [in Coq.Floats.PrimFloat]
f:12 [in Coq.Init.Hexadecimal]
f:12 [in Coq.rtauto.Bintree]
F:12 [in Coq.micromega.DeclConstant]
f:12 [in Coq.Logic.Adjointification]
f:12 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:120 [in Coq.Reals.Ranalysis1]
f:120 [in Coq.MSets.MSetProperties]
f:120 [in Coq.FSets.FSetProperties]
f:120 [in Coq.Logic.FinFun]
f:120 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:121 [in Coq.Numbers.DecimalFacts]
f:121 [in Coq.FSets.FMapInterface]
f:121 [in Coq.FSets.FMapFullAVL]
f:121 [in Coq.Reals.Rpower]
f:121 [in Coq.Numbers.HexadecimalFacts]
f:121 [in Coq.FSets.FSetCompat]
f:1211 [in Coq.FSets.FMapAVL]
f:1213 [in Coq.Lists.List]
f:1215 [in Coq.FSets.FMapAVL]
f:122 [in Coq.FSets.FSetDecide]
f:122 [in Coq.MSets.MSetDecide]
f:122 [in Coq.FSets.FMapAVL]
f:122 [in Coq.NArith.BinNatDef]
f:122 [in Coq.Init.Logic]
f:1220 [in Coq.FSets.FMapAVL]
f:1226 [in Coq.FSets.FMapAVL]
f:123 [in Coq.Reals.Ranalysis1]
f:123 [in Coq.Numbers.DecimalFacts]
f:123 [in Coq.FSets.FMapFullAVL]
f:123 [in Coq.Numbers.HexadecimalFacts]
f:123 [in Coq.Reals.RiemannInt_SF]
f:123 [in Coq.Logic.FinFun]
f:124 [in Coq.micromega.RingMicromega]
f:124 [in Coq.Classes.RelationClasses]
f:125 [in Coq.Reals.Ranalysis1]
f:125 [in Coq.Classes.RelationClasses]
f:125 [in Coq.Logic.ChoiceFacts]
f:125 [in Coq.FSets.FMapFullAVL]
f:125 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:126 [in Coq.MSets.MSetEqProperties]
f:126 [in Coq.Reals.Abstract.ConstructiveLimits]
f:126 [in Coq.FSets.FSetEqProperties]
f:126 [in Coq.Reals.RiemannInt_SF]
f:127 [in Coq.Reals.Rpower]
f:127 [in Coq.Logic.FinFun]
f:128 [in Coq.Reals.Ranalysis1]
f:128 [in Coq.FSets.FSetDecide]
f:128 [in Coq.micromega.RingMicromega]
f:128 [in Coq.MSets.MSetProperties]
f:128 [in Coq.Reals.MVT]
f:128 [in Coq.MSets.MSetDecide]
f:128 [in Coq.FSets.FMapAVL]
f:128 [in Coq.FSets.FSetProperties]
f:129 [in Coq.PArith.BinPos]
f:13 [in Coq.Logic.ChoiceFacts]
f:13 [in Coq.ssr.ssrfun]
f:13 [in Coq.Arith.PeanoNat]
f:13 [in Coq.Numbers.Cyclic.Int31.Int31]
f:13 [in Coq.Logic.FinFun]
f:130 [in Coq.MSets.MSetInterface]
f:130 [in Coq.Classes.RelationClasses]
f:130 [in Coq.Init.Nat]
f:130 [in Coq.QArith.QArith_base]
f:131 [in Coq.Vectors.VectorSpec]
f:131 [in Coq.Reals.Ranalysis1]
f:131 [in Coq.micromega.RingMicromega]
f:131 [in Coq.Classes.RelationClasses]
f:131 [in Coq.FSets.FMapFullAVL]
f:131 [in Coq.Reals.Abstract.ConstructiveLimits]
f:131 [in Coq.micromega.ZMicromega]
f:131 [in Coq.Logic.FinFun]
f:132 [in Coq.MSets.MSetEqProperties]
f:132 [in Coq.FSets.FSetEqProperties]
f:133 [in Coq.MSets.MSetInterface]
f:133 [in Coq.micromega.RingMicromega]
f:133 [in Coq.Reals.Rsqrt_def]
f:134 [in Coq.Floats.SpecFloat]
f:134 [in Coq.Reals.RiemannInt]
f:135 [in Coq.Reals.MVT]
f:136 [in Coq.MSets.MSetInterface]
f:136 [in Coq.MSets.MSetProperties]
f:136 [in Coq.Floats.SpecFloat]
f:136 [in Coq.FSets.FSetProperties]
f:136 [in Coq.Logic.FinFun]
f:1372 [in Coq.FSets.FMapAVL]
f:1374 [in Coq.FSets.FMapAVL]
f:1376 [in Coq.FSets.FMapAVL]
f:138 [in Coq.Vectors.VectorSpec]
f:138 [in Coq.micromega.ZMicromega]
f:138 [in Coq.Logic.FinFun]
f:1382 [in Coq.FSets.FMapAVL]
f:139 [in Coq.Floats.SpecFloat]
F:139 [in Coq.Logic.Hurkens]
f:139 [in Coq.micromega.Tauto]
f:14 [in Coq.Logic.Hurkens]
f:14 [in Coq.Reals.NewtonInt]
f:14 [in Coq.Sets.Multiset]
f:14 [in Coq.Sets.Image]
f:140 [in Coq.MSets.MSetProperties]
f:140 [in Coq.Reals.MVT]
f:140 [in Coq.FSets.FSetProperties]
f:140 [in Coq.Logic.FinFun]
f:141 [in Coq.Reals.RiemannInt_SF]
f:142 [in Coq.Reals.PSeries_reg]
f:142 [in Coq.Reals.RiemannInt_SF]
F:143 [in Coq.Arith.Wf_nat]
f:143 [in Coq.Logic.FunctionalExtensionality]
F:143 [in Coq.Logic.Hurkens]
f:143 [in Coq.micromega.Tauto]
f:143 [in Coq.Logic.FinFun]
f:1438 [in Coq.FSets.FMapAVL]
f:144 [in Coq.Reals.Ranalysis1]
f:144 [in Coq.Sorting.PermutSetoid]
f:145 [in Coq.Reals.Rderiv]
f:145 [in Coq.Vectors.VectorSpec]
f:145 [in Coq.MSets.MSetWeakList]
f:145 [in Coq.Logic.Hurkens]
f:145 [in Coq.micromega.Tauto]
f:146 [in Coq.Reals.MVT]
f:146 [in Coq.Logic.FinFun]
f:147 [in Coq.Logic.FunctionalExtensionality]
f:147 [in Coq.micromega.ZMicromega]
f:1475 [in Coq.FSets.FMapAVL]
f:148 [in Coq.Floats.SpecFloat]
f:148 [in Coq.MSets.MSetWeakList]
f:148 [in Coq.Reals.PSeries_reg]
f:148 [in Coq.Logic.ClassicalFacts]
f:148 [in Coq.Logic.FinFun]
f:148 [in Coq.Lists.SetoidList]
f:1480 [in Coq.FSets.FMapAVL]
f:1486 [in Coq.FSets.FMapAVL]
f:1492 [in Coq.FSets.FMapAVL]
f:1499 [in Coq.FSets.FMapAVL]
f:15 [in Coq.Logic.SetoidChoice]
f:15 [in Coq.Logic.FunctionalExtensionality]
f:15 [in Coq.Reals.RiemannInt]
f:15 [in Coq.Logic.ClassicalChoice]
f:15 [in Coq.Logic.IndefiniteDescription]
f:15 [in Coq.Sets.Image]
f:150 [in Coq.MSets.MSetWeakList]
f:150 [in Coq.Lists.ListSet]
f:1506 [in Coq.FSets.FMapAVL]
f:151 [in Coq.Reals.RiemannInt_SF]
f:152 [in Coq.Vectors.VectorSpec]
f:152 [in Coq.ssr.ssrfun]
f:153 [in Coq.MSets.MSetWeakList]
F:154 [in Coq.Logic.Hurkens]
f:154 [in Coq.Reals.PSeries_reg]
f:154 [in Coq.Lists.SetoidList]
f:155 [in Coq.Reals.MVT]
f:155 [in Coq.Logic.ClassicalFacts]
f:156 [in Coq.Reals.Ranalysis1]
f:156 [in Coq.MSets.MSetWeakList]
F:158 [in Coq.Logic.Hurkens]
f:158 [in Coq.Lists.ListSet]
f:158 [in Coq.Reals.RiemannInt_SF]
f:159 [in Coq.MSets.MSetWeakList]
f:159 [in Coq.micromega.ZMicromega]
f:16 [in Coq.MSets.MSetWeakList]
f:16 [in Coq.Logic.ClassicalUniqueChoice]
f:16 [in Coq.Numbers.Natural.Abstract.NAxioms]
f:161 [in Coq.Vectors.VectorSpec]
f:161 [in Coq.Reals.Ranalysis1]
f:161 [in Coq.MSets.MSetWeakList]
F:161 [in Coq.Logic.Hurkens]
f:162 [in Coq.Reals.Ranalysis5]
f:164 [in Coq.ssr.ssrfun]
f:164 [in Coq.micromega.ZMicromega]
f:165 [in Coq.MSets.MSetWeakList]
f:165 [in Coq.Reals.RiemannInt_SF]
f:165 [in Coq.micromega.Tauto]
f:166 [in Coq.Reals.Ranalysis1]
f:166 [in Coq.micromega.RingMicromega]
f:166 [in Coq.ssr.ssrfun]
F:167 [in Coq.Logic.Hurkens]
f:169 [in Coq.MSets.MSetInterface]
f:169 [in Coq.MSets.MSetWeakList]
F:169 [in Coq.Logic.Hurkens]
f:17 [in Coq.Wellfounded.Well_Ordering]
f:17 [in Coq.Numbers.NaryFunctions]
f:17 [in Coq.Floats.FloatOps]
f:17 [in Coq.rtauto.Bintree]
F:17 [in Coq.micromega.DeclConstant]
f:17 [in Coq.MSets.MSetGenTree]
f:17 [in Coq.Sets.Image]
f:17 [in Coq.Program.Basics]
f:17 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:170 [in Coq.Vectors.VectorSpec]
f:170 [in Coq.Reals.Ranalysis1]
f:170 [in Coq.Reals.Rfunctions]
f:171 [in Coq.micromega.ZMicromega]
f:172 [in Coq.Reals.MVT]
f:172 [in Coq.FSets.FMapFacts]
f:172 [in Coq.MSets.MSetWeakList]
f:173 [in Coq.micromega.ZMicromega]
f:174 [in Coq.Reals.Ranalysis1]
f:174 [in Coq.Init.Logic]
f:175 [in Coq.MSets.MSetWeakList]
f:176 [in Coq.Reals.Rfunctions]
f:176 [in Coq.Reals.RiemannInt_SF]
f:177 [in Coq.PArith.BinPos]
f:177 [in Coq.FSets.FMapFacts]
f:178 [in Coq.Reals.Ranalysis1]
F:178 [in Coq.Logic.Hurkens]
f:178 [in Coq.MSets.MSetRBT]
f:178 [in Coq.Reals.Ranalysis5]
f:178 [in Coq.FSets.FSetCompat]
f:179 [in Coq.FSets.FMapPositive]
f:179 [in Coq.FSets.FSetCompat]
f:18 [in Coq.Program.Wf]
f:18 [in Coq.Reals.Ranalysis4]
f:18 [in Coq.Numbers.DecimalQ]
f:18 [in Coq.Logic.ChoiceFacts]
f:18 [in Coq.Reals.NewtonInt]
f:18 [in Coq.Reals.Ranalysis5]
f:18 [in Coq.Numbers.HexadecimalQ]
f:18 [in Coq.Reals.ClassicalDedekindReals]
f:18 [in Coq.btauto.Reflect]
f:180 [in Coq.FSets.FMapFacts]
f:180 [in Coq.FSets.FSetCompat]
F:181 [in Coq.Logic.Hurkens]
f:181 [in Coq.Reals.RiemannInt_SF]
f:181 [in Coq.FSets.FSetCompat]
f:182 [in Coq.Reals.Ranalysis1]
f:183 [in Coq.Reals.Rfunctions]
f:183 [in Coq.FSets.FMapFacts]
f:183 [in Coq.MSets.MSetRBT]
f:183 [in Coq.FSets.FMapPositive]
F:183 [in Coq.Reals.Rtopology]
f:183 [in Coq.micromega.ZMicromega]
f:183 [in Coq.FSets.FSetCompat]
F:184 [in Coq.Logic.Hurkens]
f:184 [in Coq.Structures.GenericMinMax]
F:184 [in Coq.Logic.ClassicalFacts]
f:184 [in Coq.Reals.RiemannInt_SF]
f:185 [in Coq.PArith.BinPos]
f:185 [in Coq.micromega.ZMicromega]
f:185 [in Coq.FSets.FSetCompat]
f:186 [in Coq.Reals.Ranalysis1]
f:186 [in Coq.Reals.RiemannInt]
F:186 [in Coq.Logic.ClassicalFacts]
f:186 [in Coq.micromega.Tauto]
f:187 [in Coq.FSets.FMapFullAVL]
F:187 [in Coq.Logic.Hurkens]
f:187 [in Coq.Structures.GenericMinMax]
f:188 [in Coq.Reals.RiemannInt_SF]
f:189 [in Coq.Reals.Ranalysis1]
f:189 [in Coq.PArith.BinPos]
f:189 [in Coq.Reals.Rfunctions]
f:189 [in Coq.Classes.Morphisms]
f:189 [in Coq.FSets.FMapPositive]
f:19 [in Coq.Reals.Ranalysis1]
f:19 [in Coq.Sets.Image]
f:19 [in Coq.Reals.ClassicalDedekindReals]
f:19 [in Coq.btauto.Reflect]
f:190 [in Coq.Reals.RiemannInt]
f:190 [in Coq.ssr.ssrfun]
f:191 [in Coq.Reals.MVT]
f:191 [in Coq.micromega.Tauto]
f:191 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:192 [in Coq.FSets.FMapFacts]
f:192 [in Coq.MSets.MSetRBT]
f:192 [in Coq.Logic.ClassicalFacts]
f:193 [in Coq.PArith.BinPos]
f:194 [in Coq.Reals.Ranalysis1]
f:195 [in Coq.Init.Specif]
f:195 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:196 [in Coq.MSets.MSetRBT]
f:197 [in Coq.micromega.RingMicromega]
f:197 [in Coq.Logic.ChoiceFacts]
f:197 [in Coq.FSets.FMapPositive]
f:197 [in Coq.Init.Logic]
f:197 [in Coq.micromega.Tauto]
f:198 [in Coq.PArith.BinPos]
f:198 [in Coq.Logic.ClassicalFacts]
f:198 [in Coq.Vectors.VectorDef]
f:199 [in Coq.Classes.Morphisms]
f:199 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
F:2 [in Coq.micromega.DeclConstant]
f:2 [in Coq.Reals.Abstract.ConstructiveSum]
f:2 [in Coq.Logic.Adjointification]
f:20 [in Coq.Reals.Ranalysis4]
f:20 [in Coq.Logic.ExtensionalityFacts]
f:20 [in Coq.Logic.Hurkens]
f:20 [in Coq.Reals.NewtonInt]
f:200 [in Coq.ssr.ssrfun]
f:200 [in Coq.Reals.Rtopology]
f:201 [in Coq.Reals.Ranalysis1]
f:201 [in Coq.PArith.BinPos]
f:201 [in Coq.micromega.RingMicromega]
f:201 [in Coq.MSets.MSetRBT]
f:202 [in Coq.Reals.RiemannInt]
f:202 [in Coq.ssr.ssrfun]
f:202 [in Coq.Classes.CMorphisms]
f:203 [in Coq.FSets.FMapPositive]
f:203 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:204 [in Coq.Classes.Morphisms]
f:204 [in Coq.Reals.RiemannInt]
f:204 [in Coq.Reals.Rtopology]
f:204 [in Coq.Reals.RiemannInt_SF]
f:205 [in Coq.Reals.Ranalysis1]
f:206 [in Coq.Init.Logic]
f:207 [in Coq.Reals.Ranalysis1]
f:208 [in Coq.micromega.RingMicromega]
f:208 [in Coq.Reals.RiemannInt]
f:209 [in Coq.PArith.BinPos]
f:209 [in Coq.FSets.FMapPositive]
f:209 [in Coq.micromega.Tauto]
f:209 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:21 [in Coq.Logic.FunctionalExtensionality]
f:21 [in Coq.ssr.ssrfun]
f:21 [in Coq.rtauto.Bintree]
f:21 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:210 [in Coq.Reals.RiemannInt_SF]
f:211 [in Coq.Logic.Hurkens]
f:212 [in Coq.Classes.Morphisms]
f:212 [in Coq.Logic.Hurkens]
f:212 [in Coq.Classes.CMorphisms]
f:213 [in Coq.Logic.Hurkens]
f:214 [in Coq.Logic.Hurkens]
f:214 [in Coq.FSets.FMapPositive]
f:214 [in Coq.Structures.GenericMinMax]
f:215 [in Coq.Logic.Hurkens]
f:215 [in Coq.micromega.Tauto]
f:216 [in Coq.Logic.Hurkens]
f:216 [in Coq.Vectors.VectorDef]
f:217 [in Coq.MSets.MSetList]
f:217 [in Coq.Logic.Hurkens]
f:217 [in Coq.Classes.CMorphisms]
f:217 [in Coq.MSets.MSetRBT]
f:217 [in Coq.Reals.Rtopology]
f:217 [in Coq.Structures.GenericMinMax]
f:217 [in Coq.micromega.Tauto]
f:218 [in Coq.Logic.Hurkens]
f:218 [in Coq.Init.Logic]
f:22 [in Coq.Classes.RelationPairs]
f:22 [in Coq.Reals.RiemannInt]
f:22 [in Coq.Reals.NewtonInt]
f:22 [in Coq.Sets.Image]
f:22 [in Coq.Program.Basics]
f:220 [in Coq.Structures.GenericMinMax]
F:221 [in Coq.Logic.Hurkens]
f:221 [in Coq.MSets.MSetRBT]
f:222 [in Coq.MSets.MSetList]
f:222 [in Coq.Classes.CMorphisms]
F:223 [in Coq.Logic.Hurkens]
f:223 [in Coq.Structures.GenericMinMax]
f:223 [in Coq.Reals.Abstract.ConstructiveSum]
f:224 [in Coq.FSets.FMapFullAVL]
f:225 [in Coq.MSets.MSetList]
F:225 [in Coq.Logic.Hurkens]
f:225 [in Coq.MSets.MSetPositive]
f:225 [in Coq.Reals.Rtopology]
f:226 [in Coq.MSets.MSetInterface]
f:226 [in Coq.MSets.MSetRBT]
f:226 [in Coq.Reals.RiemannInt_SF]
f:226 [in Coq.micromega.Tauto]
F:227 [in Coq.Logic.Hurkens]
f:227 [in Coq.Vectors.VectorDef]
f:229 [in Coq.MSets.MSetInterface]
f:229 [in Coq.micromega.RingMicromega]
f:229 [in Coq.MSets.MSetList]
f:229 [in Coq.FSets.FMapFullAVL]
f:229 [in Coq.Sorting.Permutation]
f:23 [in Coq.Numbers.DecimalQ]
f:23 [in Coq.Numbers.HexadecimalQ]
f:23 [in Coq.FSets.FSetFacts]
f:23 [in Coq.Reals.ClassicalDedekindReals]
f:230 [in Coq.Classes.CMorphisms]
f:231 [in Coq.MSets.MSetInterface]
f:231 [in Coq.micromega.RingMicromega]
f:231 [in Coq.Reals.RiemannInt]
f:231 [in Coq.MSets.MSetList]
f:232 [in Coq.Reals.Ranalysis1]
f:232 [in Coq.micromega.RingMicromega]
f:232 [in Coq.Sorting.Permutation]
f:233 [in Coq.MSets.MSetInterface]
f:233 [in Coq.Init.Logic]
f:233 [in Coq.Reals.RiemannInt_SF]
f:234 [in Coq.Reals.RiemannInt]
f:234 [in Coq.MSets.MSetList]
f:234 [in Coq.FSets.FMapWeakList]
f:235 [in Coq.Reals.Ranalysis1]
f:235 [in Coq.MSets.MSetInterface]
f:235 [in Coq.FSets.FMapFullAVL]
f:235 [in Coq.Sorting.Permutation]
f:236 [in Coq.FSets.FSetBridge]
f:237 [in Coq.MSets.MSetList]
f:238 [in Coq.Reals.Ranalysis1]
f:238 [in Coq.Classes.CMorphisms]
f:239 [in Coq.FSets.FSetBridge]
f:239 [in Coq.Sorting.Permutation]
f:24 [in Coq.Reals.Ranalysis1]
f:24 [in Coq.ssr.ssrfun]
f:24 [in Coq.Logic.ClassicalUniqueChoice]
f:24 [in Coq.Reals.RiemannInt_SF]
f:24 [in Coq.micromega.Tauto]
f:24 [in Coq.rtauto.Rtauto]
f:240 [in Coq.Reals.RiemannInt]
f:240 [in Coq.FSets.FSetInterface]
f:240 [in Coq.FSets.FMapPositive]
f:240 [in Coq.FSets.FMapWeakList]
f:241 [in Coq.MSets.MSetList]
f:241 [in Coq.FSets.FMapFullAVL]
f:241 [in Coq.Reals.Abstract.ConstructiveSum]
f:241 [in Coq.micromega.Tauto]
f:242 [in Coq.Reals.Ranalysis5]
f:242 [in Coq.FSets.FMapList]
f:243 [in Coq.Reals.Ranalysis1]
f:243 [in Coq.Sorting.Permutation]
f:244 [in Coq.FSets.FMapWeakList]
f:244 [in Coq.Reals.RiemannInt_SF]
f:244 [in Coq.Vectors.VectorDef]
f:245 [in Coq.MSets.MSetList]
f:246 [in Coq.Reals.Ranalysis1]
f:246 [in Coq.FSets.FSetBridge]
f:247 [in Coq.MSets.MSetInterface]
f:247 [in Coq.MSets.MSetPositive]
f:247 [in Coq.Reals.Abstract.ConstructiveSum]
f:248 [in Coq.MSets.MSetList]
f:248 [in Coq.FSets.FMapFullAVL]
f:248 [in Coq.FSets.FMapList]
f:249 [in Coq.FSets.FSetBridge]
f:249 [in Coq.FSets.FMapWeakList]
f:249 [in Coq.Init.Logic]
f:25 [in Coq.Floats.FloatLemmas]
f:25 [in Coq.Classes.RelationPairs]
f:25 [in Coq.Reals.RiemannInt]
f:25 [in Coq.Sets.Image]
f:25 [in Coq.Sets.Infinite_sets]
f:25 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:251 [in Coq.FSets.FSetBridge]
f:251 [in Coq.MSets.MSetList]
f:251 [in Coq.FSets.FMapPositive]
f:251 [in Coq.Reals.Abstract.ConstructiveSum]
f:251 [in Coq.micromega.ZMicromega]
f:252 [in Coq.FSets.FMapList]
f:252 [in Coq.Reals.RiemannInt_SF]
f:253 [in Coq.FSets.FSetBridge]
f:253 [in Coq.MSets.MSetList]
f:253 [in Coq.MSets.MSetPositive]
f:254 [in Coq.MSets.MSetPositive]
f:254 [in Coq.FSets.FMapWeakList]
f:255 [in Coq.Reals.RiemannInt]
f:255 [in Coq.FSets.FMapFullAVL]
f:255 [in Coq.Reals.Ranalysis5]
f:256 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
f:257 [in Coq.FSets.FMapList]
f:257 [in Coq.Reals.RiemannInt_SF]
f:257 [in Coq.Lists.SetoidList]
f:258 [in Coq.FSets.FMapPositive]
f:258 [in Coq.Logic.ClassicalFacts]
f:259 [in Coq.FSets.FSetBridge]
f:259 [in Coq.Logic.EqdepFacts]
f:259 [in Coq.micromega.RingMicromega]
f:259 [in Coq.Sorting.Permutation]
f:259 [in Coq.MSets.MSetPositive]
f:259 [in Coq.Lists.SetoidList]
f:26 [in Coq.Reals.Ranalysis1]
f:26 [in Coq.Numbers.NaryFunctions]
f:26 [in Coq.Logic.ExtensionalityFacts]
F:26 [in Coq.Logic.Hurkens]
f:26 [in Coq.Logic.ClassicalUniqueChoice]
f:26 [in Coq.Reals.NewtonInt]
f:26 [in Coq.Logic.ClassicalDescription]
f:26 [in Coq.FSets.FSetFacts]
f:261 [in Coq.MSets.MSetPositive]
f:261 [in Coq.Reals.RiemannInt_SF]
f:262 [in Coq.FSets.FSetBridge]
f:262 [in Coq.FSets.FMapList]
f:262 [in Coq.Lists.SetoidList]
f:263 [in Coq.micromega.RingMicromega]
f:265 [in Coq.FSets.FSetBridge]
f:265 [in Coq.NArith.BinNat]
f:265 [in Coq.Sorting.Permutation]
f:266 [in Coq.FSets.FSetBridge]
f:266 [in Coq.micromega.RingMicromega]
f:266 [in Coq.MSets.MSetPositive]
f:269 [in Coq.micromega.RingMicromega]
f:269 [in Coq.MSets.MSetPositive]
f:27 [in Coq.Reals.MVT]
f:27 [in Coq.Logic.ChoiceFacts]
f:27 [in Coq.Classes.CMorphisms]
f:27 [in Coq.Reals.ClassicalDedekindReals]
f:270 [in Coq.FSets.FSetBridge]
f:271 [in Coq.Reals.RiemannInt_SF]
f:271 [in Coq.micromega.Tauto]
f:272 [in Coq.MSets.MSetPositive]
f:273 [in Coq.FSets.FSetBridge]
f:273 [in Coq.NArith.BinNat]
f:273 [in Coq.Reals.Rtopology]
f:274 [in Coq.Logic.EqdepFacts]
f:274 [in Coq.FSets.FMapFacts]
f:274 [in Coq.MSets.MSetPositive]
f:275 [in Coq.FSets.FSetBridge]
f:276 [in Coq.Init.Specif]
f:276 [in Coq.Lists.SetoidList]
F:277 [in Coq.Logic.Hurkens]
f:277 [in Coq.NArith.BinNat]
f:277 [in Coq.Reals.RiemannInt_SF]
f:279 [in Coq.FSets.FSetBridge]
f:28 [in Coq.Classes.RelationPairs]
f:28 [in Coq.MSets.MSetFacts]
f:28 [in Coq.MSets.MSetWeakList]
f:28 [in Coq.ssr.ssrfun]
f:28 [in Coq.Logic.ClassicalFacts]
F:28 [in Coq.rtauto.Rtauto]
F:280 [in Coq.Logic.Hurkens]
f:280 [in Coq.FSets.FMapWeakList]
f:281 [in Coq.ssr.ssrbool]
f:281 [in Coq.NArith.BinNat]
f:282 [in Coq.FSets.FSetBridge]
f:282 [in Coq.FSets.FMapPositive]
f:283 [in Coq.MSets.MSetProperties]
f:283 [in Coq.Reals.RiemannInt_SF]
f:283 [in Coq.FSets.FSetProperties]
f:284 [in Coq.FSets.FSetBridge]
f:284 [in Coq.Init.Logic]
f:286 [in Coq.FSets.FMapFacts]
F:286 [in Coq.Logic.Hurkens]
f:286 [in Coq.NArith.BinNat]
f:286 [in Coq.Reals.Rtopology]
F:288 [in Coq.Logic.Hurkens]
f:288 [in Coq.FSets.FMapList]
f:289 [in Coq.FSets.FSetBridge]
f:289 [in Coq.FSets.FMapFacts]
f:289 [in Coq.NArith.BinNat]
f:289 [in Coq.Reals.RiemannInt_SF]
f:29 [in Coq.MSets.MSetProperties]
f:29 [in Coq.Floats.FloatLemmas]
f:29 [in Coq.Numbers.Natural.Abstract.NDefOps]
f:29 [in Coq.Classes.CEquivalence]
f:29 [in Coq.Lists.ListDec]
f:29 [in Coq.FSets.FSetProperties]
f:29 [in Coq.Classes.Equivalence]
F:290 [in Coq.Logic.Hurkens]
f:291 [in Coq.FSets.FSetBridge]
f:291 [in Coq.MSets.MSetProperties]
f:291 [in Coq.Logic.Hurkens]
f:291 [in Coq.FSets.FSetProperties]
F:293 [in Coq.Logic.Hurkens]
f:294 [in Coq.Reals.Ranalysis1]
f:294 [in Coq.Logic.Hurkens]
f:294 [in Coq.Reals.RiemannInt_SF]
f:295 [in Coq.micromega.ZMicromega]
f:296 [in Coq.Reals.Rtopology]
f:296 [in Coq.micromega.Tauto]
f:297 [in Coq.NArith.BinNat]
f:297 [in Coq.micromega.ZMicromega]
f:298 [in Coq.Reals.Ranalysis1]
f:298 [in Coq.micromega.RingMicromega]
f:298 [in Coq.Reals.RiemannInt]
f:298 [in Coq.Init.Specif]
f:298 [in Coq.Lists.SetoidList]
f:299 [in Coq.Reals.Ranalysis5]
f:3 [in Coq.Reals.Ranalysis4]
f:3 [in Coq.Logic.ExtensionalityFacts]
f:3 [in Coq.Logic.FunctionalExtensionality]
f:3 [in Coq.Relations.Relations]
f:3 [in Coq.Program.Combinators]
f:3 [in Coq.ZArith.Zmisc]
f:3 [in Coq.Logic.FinFun]
f:30 [in Coq.MSets.MSetFacts]
f:30 [in Coq.Reals.NewtonInt]
f:30 [in Coq.Reals.RiemannInt_SF]
f:30 [in Coq.micromega.Tauto]
f:30 [in Coq.Reals.ClassicalDedekindReals]
f:30 [in Coq.Sets.Infinite_sets]
f:300 [in Coq.Reals.RiemannInt_SF]
f:300 [in Coq.micromega.Tauto]
f:301 [in Coq.FSets.FSetPositive]
f:301 [in Coq.Lists.SetoidList]
f:303 [in Coq.micromega.RingMicromega]
f:303 [in Coq.micromega.Tauto]
f:304 [in Coq.MSets.MSetGenTree]
f:305 [in Coq.Reals.Ranalysis1]
f:306 [in Coq.Reals.Rtopology]
f:306 [in Coq.Init.Logic]
f:306 [in Coq.Reals.RiemannInt_SF]
f:307 [in Coq.MSets.MSetGenTree]
f:308 [in Coq.Init.Specif]
f:308 [in Coq.Reals.Ranalysis5]
f:309 [in Coq.Lists.SetoidList]
f:31 [in Coq.Reals.Ranalysis1]
f:31 [in Coq.Classes.RelationPairs]
F:31 [in Coq.Logic.Hurkens]
f:31 [in Coq.NArith.Nnat]
f:31 [in Coq.Logic.ClassicalFacts]
f:31 [in Coq.FSets.FSetFacts]
F:31 [in Coq.btauto.Reflect]
f:31 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:310 [in Coq.micromega.RingMicromega]
f:310 [in Coq.MSets.MSetGenTree]
f:312 [in Coq.FSets.FMapFacts]
f:313 [in Coq.ssr.ssrbool]
f:313 [in Coq.Reals.RiemannInt_SF]
f:314 [in Coq.Reals.RiemannInt_SF]
F:315 [in Coq.Reals.Rtopology]
f:315 [in Coq.Reals.Ranalysis5]
f:315 [in Coq.Init.Logic]
f:317 [in Coq.Reals.Ranalysis1]
f:317 [in Coq.Reals.Rtopology]
f:317 [in Coq.MSets.MSetGenTree]
f:319 [in Coq.Vectors.VectorSpec]
f:319 [in Coq.Init.Specif]
f:32 [in Coq.MSets.MSetProperties]
f:32 [in Coq.Logic.ExtensionalityFacts]
f:32 [in Coq.MSets.MSetFacts]
f:32 [in Coq.MSets.MSetWeakList]
f:32 [in Coq.FSets.FSetProperties]
f:320 [in Coq.Reals.Ranalysis1]
f:320 [in Coq.Reals.Rtopology]
f:322 [in Coq.Reals.Ranalysis1]
f:322 [in Coq.Reals.Ranalysis5]
f:322 [in Coq.Reals.RiemannInt_SF]
f:323 [in Coq.FSets.FSetPositive]
f:324 [in Coq.Vectors.VectorSpec]
f:324 [in Coq.Reals.Ranalysis1]
f:324 [in Coq.FSets.FMapFacts]
f:324 [in Coq.Reals.Rtopology]
f:326 [in Coq.Reals.Ranalysis1]
f:326 [in Coq.micromega.Tauto]
f:327 [in Coq.FSets.FMapPositive]
f:328 [in Coq.Reals.Ranalysis1]
F:328 [in Coq.Logic.Hurkens]
f:328 [in Coq.Reals.RiemannInt_SF]
f:329 [in Coq.Init.Specif]
f:329 [in Coq.FSets.FSetPositive]
f:329 [in Coq.Reals.RiemannInt_SF]
f:33 [in Coq.Floats.FloatLemmas]
f:33 [in Coq.Logic.Hurkens]
f:33 [in Coq.Reals.ClassicalDedekindReals]
f:33 [in Coq.Logic.FinFun]
F:33 [in Coq.rtauto.Rtauto]
f:330 [in Coq.Vectors.VectorSpec]
f:330 [in Coq.Reals.RiemannInt]
F:331 [in Coq.Logic.Hurkens]
f:331 [in Coq.micromega.Tauto]
f:332 [in Coq.FSets.FMapFacts]
f:332 [in Coq.FSets.FSetPositive]
f:333 [in Coq.FSets.FMapWeakList]
f:334 [in Coq.FSets.FMapPositive]
f:335 [in Coq.FSets.FSetPositive]
f:336 [in Coq.FSets.FSetPositive]
f:336 [in Coq.Reals.RiemannInt_SF]
F:337 [in Coq.Logic.Hurkens]
f:337 [in Coq.FSets.FMapWeakList]
f:338 [in Coq.Init.Logic]
f:339 [in Coq.Reals.RiemannInt]
f:339 [in Coq.ssr.ssrbool]
F:339 [in Coq.Logic.Hurkens]
f:34 [in Coq.Reals.Ranalysis1]
f:34 [in Coq.Classes.RelationPairs]
f:34 [in Coq.Logic.ClassicalFacts]
f:34 [in Coq.Reals.ClassicalDedekindReals]
f:340 [in Coq.Reals.Ranalysis5]
f:341 [in Coq.Reals.Ranalysis1]
f:341 [in Coq.Logic.Hurkens]
f:341 [in Coq.FSets.FSetPositive]
f:343 [in Coq.Logic.Hurkens]
f:343 [in Coq.Init.Logic]
f:344 [in Coq.FSets.FSetPositive]
f:345 [in Coq.FSets.FMapFacts]
F:345 [in Coq.Logic.Hurkens]
f:345 [in Coq.Reals.RiemannInt_SF]
f:346 [in Coq.FSets.FSetPositive]
f:346 [in Coq.FSets.FMapWeakList]
f:347 [in Coq.Reals.Ranalysis1]
F:347 [in Coq.Logic.Hurkens]
f:348 [in Coq.Reals.Ranalysis1]
F:349 [in Coq.Logic.Hurkens]
f:349 [in Coq.FSets.FMapWeakList]
f:35 [in Coq.Reals.RiemannInt]
f:351 [in Coq.ssr.ssrbool]
F:351 [in Coq.Logic.Hurkens]
f:351 [in Coq.FSets.FSetPositive]
f:352 [in Coq.FSets.FMapWeakList]
f:352 [in Coq.Init.Logic]
f:353 [in Coq.Reals.RiemannInt_SF]
f:354 [in Coq.FSets.FSetPositive]
f:356 [in Coq.Reals.Ranalysis1]
f:356 [in Coq.FSets.FMapWeakList]
f:356 [in Coq.Reals.Ranalysis5]
f:356 [in Coq.Reals.RiemannInt_SF]
f:357 [in Coq.FSets.FSetPositive]
f:358 [in Coq.Init.Logic]
f:36 [in Coq.Numbers.DecimalQ]
f:36 [in Coq.MSets.MSetWeakList]
F:36 [in Coq.Logic.Hurkens]
f:36 [in Coq.Reals.Rlimit]
f:36 [in Coq.Numbers.HexadecimalQ]
F:36 [in Coq.rtauto.Rtauto]
f:360 [in Coq.FSets.FSetPositive]
f:360 [in Coq.FSets.FMapWeakList]
f:362 [in Coq.FSets.FSetPositive]
f:363 [in Coq.FSets.FMapWeakList]
f:364 [in Coq.Reals.Ranalysis1]
f:364 [in Coq.Reals.Ranalysis5]
f:365 [in Coq.Init.Logic]
f:365 [in Coq.Reals.RiemannInt_SF]
f:365 [in Coq.micromega.Tauto]
f:366 [in Coq.Logic.ChoiceFacts]
f:367 [in Coq.Reals.Ranalysis1]
f:369 [in Coq.Logic.ChoiceFacts]
f:37 [in Coq.Sorting.PermutEq]
f:37 [in Coq.Reals.Ranalysis1]
f:37 [in Coq.Numbers.HexadecimalPos]
f:37 [in Coq.Floats.FloatLemmas]
f:37 [in Coq.Classes.Morphisms]
f:37 [in Coq.Classes.RelationPairs]
f:37 [in Coq.Logic.ChoiceFacts]
f:37 [in Coq.Numbers.DecimalPos]
f:37 [in Coq.Reals.RiemannInt_SF]
f:37 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:370 [in Coq.Reals.Ranalysis1]
f:371 [in Coq.micromega.ZMicromega]
f:373 [in Coq.Reals.Ranalysis1]
f:373 [in Coq.Reals.Ranalysis5]
f:373 [in Coq.Reals.RiemannInt_SF]
f:373 [in Coq.micromega.Tauto]
f:374 [in Coq.FSets.FMapList]
f:374 [in Coq.micromega.ZMicromega]
f:374 [in Coq.micromega.Tauto]
f:376 [in Coq.Reals.RiemannInt_SF]
f:377 [in Coq.Reals.RiemannInt]
f:378 [in Coq.FSets.FMapWeakList]
f:378 [in Coq.FSets.FMapList]
f:38 [in Coq.PArith.Pnat]
f:38 [in Coq.Logic.ExtensionalityFacts]
f:38 [in Coq.Logic.Hurkens]
f:38 [in Coq.micromega.Tauto]
f:38 [in Coq.Sets.Infinite_sets]
f:38 [in Coq.Logic.FinFun]
f:381 [in Coq.Reals.Rtopology]
f:382 [in Coq.Reals.Ranalysis5]
f:387 [in Coq.FSets.FMapList]
f:388 [in Coq.micromega.Tauto]
f:389 [in Coq.micromega.Tauto]
f:39 [in Coq.FSets.FSetBridge]
f:39 [in Coq.Numbers.DecimalQ]
f:39 [in Coq.NArith.BinNat]
f:39 [in Coq.MSets.MSetGenTree]
f:39 [in Coq.Logic.ClassicalDescription]
f:39 [in Coq.Numbers.HexadecimalQ]
f:390 [in Coq.FSets.FMapList]
f:391 [in Coq.Reals.Ranalysis5]
f:393 [in Coq.Reals.Ranalysis1]
f:393 [in Coq.micromega.Tauto]
f:394 [in Coq.micromega.Tauto]
f:395 [in Coq.FSets.FMapList]
f:395 [in Coq.micromega.Tauto]
f:396 [in Coq.micromega.Tauto]
f:398 [in Coq.FSets.FMapList]
f:398 [in Coq.micromega.Tauto]
f:4 [in Coq.Reals.Rderiv]
f:4 [in Coq.Logic.ExtensionalFunctionRepresentative]
f:4 [in Coq.Reals.Ranalysis1]
f:4 [in Coq.Floats.FloatLemmas]
f:4 [in Coq.Classes.RelationPairs]
f:4 [in Coq.Floats.FloatOps]
f:4 [in Coq.ZArith.Zpow_alt]
f:4 [in Coq.Sets.Image]
f:4 [in Coq.btauto.Reflect]
f:40 [in Coq.Reals.Ranalysis1]
f:40 [in Coq.Numbers.HexadecimalPos]
f:40 [in Coq.Reals.MVT]
f:40 [in Coq.MSets.MSetWeakList]
f:40 [in Coq.ssr.ssrfun]
f:40 [in Coq.Structures.GenericMinMax]
f:40 [in Coq.Numbers.DecimalPos]
f:40 [in Coq.Sets.Infinite_sets]
F:40 [in Coq.rtauto.Rtauto]
f:400 [in Coq.MSets.MSetRBT]
f:400 [in Coq.Reals.Rtopology]
f:400 [in Coq.micromega.Tauto]
f:402 [in Coq.FSets.FMapList]
f:404 [in Coq.MSets.MSetRBT]
f:406 [in Coq.FSets.FMapList]
f:408 [in Coq.Reals.Ranalysis5]
f:41 [in Coq.Classes.CMorphisms]
f:41 [in Coq.Sets.Image]
f:410 [in Coq.FSets.FMapList]
f:413 [in Coq.FSets.FMapList]
f:414 [in Coq.Lists.List]
f:416 [in Coq.Reals.RiemannInt]
f:419 [in Coq.MSets.MSetRBT]
f:42 [in Coq.Logic.ClassicalEpsilon]
f:42 [in Coq.Numbers.NaryFunctions]
f:42 [in Coq.Logic.ChoiceFacts]
f:42 [in Coq.Init.Datatypes]
f:42 [in Coq.Reals.RiemannInt_SF]
f:42 [in Coq.micromega.Tauto]
f:42 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:422 [in Coq.MSets.MSetRBT]
f:423 [in Coq.Reals.RiemannInt]
f:425 [in Coq.MSets.MSetRBT]
f:426 [in Coq.Reals.Ranalysis1]
f:426 [in Coq.micromega.Tauto]
f:427 [in Coq.MSets.MSetRBT]
f:428 [in Coq.Lists.List]
f:428 [in Coq.Reals.RiemannInt]
f:428 [in Coq.Logic.ChoiceFacts]
f:43 [in Coq.Reals.Ranalysis1]
f:43 [in Coq.Init.Wf]
f:43 [in Coq.MSets.MSetGenTree]
f:43 [in Coq.Reals.Ratan]
f:43 [in Coq.Logic.FinFun]
f:430 [in Coq.Reals.Ranalysis1]
f:430 [in Coq.Logic.ChoiceFacts]
f:430 [in Coq.MSets.MSetRBT]
f:431 [in Coq.setoid_ring.Field_theory]
f:432 [in Coq.Logic.ChoiceFacts]
f:433 [in Coq.Logic.ChoiceFacts]
f:434 [in Coq.Lists.List]
f:435 [in Coq.Reals.Ranalysis1]
f:435 [in Coq.Reals.RiemannInt]
f:435 [in Coq.MSets.MSetRBT]
f:435 [in Coq.Reals.Ranalysis5]
f:435 [in Coq.micromega.Tauto]
f:438 [in Coq.MSets.MSetRBT]
f:439 [in Coq.Init.Specif]
f:44 [in Coq.Reals.PSeries_reg]
f:440 [in Coq.Lists.List]
f:440 [in Coq.MSets.MSetRBT]
f:441 [in Coq.Reals.Ranalysis1]
f:442 [in Coq.Reals.RiemannInt]
f:442 [in Coq.micromega.ZMicromega]
f:443 [in Coq.MSets.MSetRBT]
f:445 [in Coq.micromega.ZMicromega]
f:446 [in Coq.Lists.List]
f:446 [in Coq.MSets.MSetRBT]
f:446 [in Coq.FSets.FMapList]
f:449 [in Coq.Reals.Ranalysis1]
f:449 [in Coq.micromega.Tauto]
f:45 [in Coq.MSets.MSetList]
f:45 [in Coq.Vectors.Fin]
f:45 [in Coq.Classes.SetoidDec]
f:45 [in Coq.Structures.GenericMinMax]
f:45 [in Coq.Reals.Rlimit]
f:45 [in Coq.Sets.Image]
F:45 [in Coq.rtauto.Rtauto]
f:450 [in Coq.FSets.FMapFacts]
f:450 [in Coq.Reals.RiemannInt]
f:451 [in Coq.Init.Logic]
f:452 [in Coq.Lists.List]
f:454 [in Coq.Reals.RiemannInt]
f:454 [in Coq.micromega.Tauto]
f:455 [in Coq.Reals.Ranalysis1]
f:455 [in Coq.FSets.FMapFacts]
f:457 [in Coq.Init.Logic]
f:458 [in Coq.Lists.List]
f:458 [in Coq.Reals.RiemannInt]
f:46 [in Coq.Classes.Morphisms]
f:46 [in Coq.Classes.CMorphisms]
f:46 [in Coq.Reals.NewtonInt]
f:46 [in Coq.Logic.FinFun]
f:460 [in Coq.FSets.FMapFacts]
f:461 [in Coq.Init.Specif]
f:462 [in Coq.Reals.RiemannInt]
f:465 [in Coq.FSets.FMapFacts]
f:47 [in Coq.Reals.Ranalysis1]
F:47 [in Coq.Arith.Wf_nat]
f:47 [in Coq.Logic.ChoiceFacts]
f:47 [in Coq.ssr.ssrfun]
f:47 [in Coq.Reals.Rlimit]
f:47 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:471 [in Coq.Init.Specif]
f:48 [in Coq.Logic.FunctionalExtensionality]
f:48 [in Coq.MSets.MSetList]
f:48 [in Coq.NArith.BinNat]
F:48 [in Coq.Reals.NewtonInt]
f:48 [in Coq.Sets.Image]
f:48 [in Coq.PArith.BinPosDef]
f:482 [in Coq.Init.Specif]
f:49 [in Coq.Logic.JMeq]
f:49 [in Coq.micromega.ZMicromega]
f:492 [in Coq.Init.Specif]
f:494 [in Coq.Lists.List]
f:497 [in Coq.Reals.RiemannInt]
f:499 [in Coq.micromega.Tauto]
f:5 [in Coq.Reals.NewtonInt]
F:5 [in Coq.micromega.DeclConstant]
f:5 [in Coq.Program.Basics]
f:5 [in Coq.Numbers.Natural.Abstract.NStrongRec]
f:50 [in Coq.Floats.FloatAxioms]
f:50 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:500 [in Coq.Lists.List]
f:504 [in Coq.Reals.RiemannInt]
f:505 [in Coq.FSets.FMapWeakList]
f:506 [in Coq.Lists.List]
f:507 [in Coq.FSets.FMapWeakList]
f:508 [in Coq.ssr.ssrbool]
f:509 [in Coq.FSets.FMapWeakList]
f:51 [in Coq.Reals.Ranalysis1]
F:51 [in Coq.Arith.Wf_nat]
F:51 [in Coq.btauto.Algebra]
f:51 [in Coq.NArith.BinNat]
f:51 [in Coq.Reals.Rlimit]
f:51 [in Coq.Logic.FinFun]
F:51 [in Coq.rtauto.Rtauto]
f:511 [in Coq.Reals.RiemannInt]
f:515 [in Coq.FSets.FMapWeakList]
f:518 [in Coq.micromega.Tauto]
f:519 [in Coq.Lists.List]
f:52 [in Coq.MSets.MSetProperties]
f:52 [in Coq.Classes.RelationPairs]
f:52 [in Coq.MSets.MSetList]
f:52 [in Coq.Sets.Image]
f:52 [in Coq.FSets.FSetProperties]
f:52 [in Coq.Floats.FloatAxioms]
f:52 [in Coq.rtauto.Rtauto]
f:520 [in Coq.ssr.ssrbool]
f:525 [in Coq.FSets.FMapList]
f:526 [in Coq.Reals.RiemannInt]
f:527 [in Coq.FSets.FMapList]
f:529 [in Coq.FSets.FMapList]
f:53 [in Coq.Reals.Ranalysis1]
f:53 [in Coq.Reals.RiemannInt]
f:53 [in Coq.Vectors.Fin]
f:53 [in Coq.Reals.RiemannInt_SF]
f:53 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:530 [in Coq.ssr.ssrbool]
f:531 [in Coq.Init.Logic]
f:532 [in Coq.Reals.RiemannInt]
f:535 [in Coq.FSets.FMapList]
f:538 [in Coq.ssr.ssrbool]
f:54 [in Coq.micromega.RingMicromega]
f:54 [in Coq.Logic.FunctionalExtensionality]
f:54 [in Coq.Logic.FinFun]
f:540 [in Coq.micromega.Tauto]
f:541 [in Coq.Reals.RiemannInt]
f:544 [in Coq.Reals.RiemannInt]
f:545 [in Coq.FSets.FMapFacts]
f:547 [in Coq.Reals.RiemannInt]
f:547 [in Coq.micromega.Tauto]
f:548 [in Coq.ssr.ssrbool]
f:55 [in Coq.Reals.Ranalysis1]
f:55 [in Coq.Logic.Hurkens]
f:55 [in Coq.micromega.QMicromega]
f:55 [in Coq.Reals.Rlimit]
F:55 [in Coq.rtauto.Rtauto]
f:550 [in Coq.ssr.ssrbool]
f:550 [in Coq.micromega.Tauto]
f:552 [in Coq.micromega.Tauto]
f:553 [in Coq.PArith.BinPos]
f:553 [in Coq.Reals.RiemannInt]
f:554 [in Coq.Init.Logic]
f:555 [in Coq.micromega.Tauto]
f:557 [in Coq.Reals.RiemannInt]
f:56 [in Coq.Init.Peano]
f:56 [in Coq.Logic.ChoiceFacts]
f:56 [in Coq.MSets.MSetList]
f:56 [in Coq.Vectors.Fin]
f:56 [in Coq.Sets.Image]
f:56 [in Coq.Reals.RiemannInt_SF]
f:56 [in Coq.Floats.FloatAxioms]
f:561 [in Coq.FSets.FMapFacts]
f:564 [in Coq.Init.Logic]
f:569 [in Coq.Reals.RiemannInt]
f:57 [in Coq.MSets.MSetInterface]
f:57 [in Coq.NArith.BinNat]
f:57 [in Coq.Reals.NewtonInt]
f:57 [in Coq.micromega.ZMicromega]
f:575 [in Coq.Init.Logic]
f:576 [in Coq.Reals.RiemannInt]
f:577 [in Coq.Lists.List]
f:58 [in Coq.Reals.MVT]
f:58 [in Coq.Numbers.NaryFunctions]
f:58 [in Coq.Logic.FunctionalExtensionality]
F:58 [in Coq.rtauto.Rtauto]
f:581 [in Coq.Lists.List]
f:584 [in Coq.Init.Logic]
f:585 [in Coq.Lists.List]
f:587 [in Coq.FSets.FMapFacts]
f:589 [in Coq.Lists.List]
f:589 [in Coq.FSets.FMapFacts]
F:59 [in Coq.Arith.Wf_nat]
f:59 [in Coq.Logic.ChoiceFacts]
f:59 [in Coq.Vectors.Fin]
f:59 [in Coq.Numbers.Natural.Abstract.NOrder]
f:59 [in Coq.micromega.ZMicromega]
f:590 [in Coq.FSets.FMapFacts]
f:592 [in Coq.Lists.List]
f:592 [in Coq.FSets.FMapFacts]
f:592 [in Coq.FSets.FMapWeakList]
f:593 [in Coq.FSets.FMapFacts]
f:595 [in Coq.FSets.FMapFacts]
f:596 [in Coq.FSets.FMapFacts]
f:598 [in Coq.FSets.FMapFacts]
f:6 [in Coq.Wellfounded.Well_Ordering]
f:6 [in Coq.Numbers.NatInt.NZDomain]
f:6 [in Coq.Program.Combinators]
f:60 [in Coq.MSets.MSetList]
f:60 [in Coq.NArith.BinNat]
f:60 [in Coq.Sets.Image]
f:606 [in Coq.FSets.FMapWeakList]
f:61 [in Coq.Reals.Ranalysis2]
f:611 [in Coq.FSets.FMapWeakList]
f:613 [in Coq.FSets.FMapList]
f:616 [in Coq.micromega.Tauto]
f:617 [in Coq.FSets.FMapWeakList]
f:62 [in Coq.Init.Peano]
f:62 [in Coq.Reals.RiemannInt]
f:62 [in Coq.FSets.FMapInterface]
F:62 [in Coq.Logic.Hurkens]
f:62 [in Coq.Classes.EquivDec]
f:62 [in Coq.NArith.Ndigits]
f:62 [in Coq.Reals.Rlimit]
f:62 [in Coq.Logic.FinFun]
f:623 [in Coq.FSets.FMapWeakList]
f:625 [in Coq.micromega.Tauto]
f:627 [in Coq.FSets.FMapList]
f:63 [in Coq.Reals.Ranalysis1]
f:63 [in Coq.MSets.MSetProperties]
F:63 [in Coq.Arith.Wf_nat]
f:63 [in Coq.NArith.Nnat]
f:63 [in Coq.Reals.Rtopology]
f:63 [in Coq.FSets.FSetProperties]
f:63 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:630 [in Coq.FSets.FMapWeakList]
f:632 [in Coq.FSets.FMapList]
f:633 [in Coq.micromega.Tauto]
f:635 [in Coq.ssr.ssrbool]
f:637 [in Coq.FSets.FMapWeakList]
f:638 [in Coq.FSets.FMapList]
f:64 [in Coq.Reals.Rderiv]
f:64 [in Coq.ssr.ssrfun]
f:64 [in Coq.Reals.RiemannInt_SF]
f:641 [in Coq.ssr.ssrbool]
f:642 [in Coq.micromega.Tauto]
f:643 [in Coq.MSets.MSetAVL]
f:644 [in Coq.FSets.FMapList]
f:646 [in Coq.MSets.MSetAVL]
f:648 [in Coq.MSets.MSetAVL]
f:648 [in Coq.micromega.Tauto]
f:65 [in Coq.Classes.Morphisms]
f:65 [in Coq.Reals.NewtonInt]
f:65 [in Coq.Reals.RList]
f:651 [in Coq.MSets.MSetAVL]
f:651 [in Coq.FSets.FMapList]
f:653 [in Coq.MSets.MSetAVL]
f:655 [in Coq.Init.Logic]
f:656 [in Coq.MSets.MSetAVL]
f:658 [in Coq.MSets.MSetAVL]
f:658 [in Coq.FSets.FMapList]
f:66 [in Coq.Reals.Ranalysis2]
f:66 [in Coq.MSets.MSetEqProperties]
f:66 [in Coq.Reals.MVT]
f:66 [in Coq.FSets.FSetEqProperties]
f:66 [in Coq.Reals.Ranalysis5]
f:66 [in Coq.Numbers.Cyclic.Int63.Uint63]
f:661 [in Coq.MSets.MSetAVL]
f:662 [in Coq.Init.Logic]
f:664 [in Coq.MSets.MSetAVL]
f:67 [in Coq.Numbers.NaryFunctions]
f:67 [in Coq.Reals.RiemannInt_SF]
f:67 [in Coq.micromega.Tauto]
f:678 [in Coq.MSets.MSetRBT]
f:679 [in Coq.Init.Specif]
F:68 [in Coq.Logic.Hurkens]
f:68 [in Coq.Reals.Rtopology]
f:68 [in Coq.Reals.Ratan]
f:68 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:680 [in Coq.MSets.MSetRBT]
f:682 [in Coq.FSets.FMapFacts]
f:69 [in Coq.Logic.ChoiceFacts]
f:69 [in Coq.ssr.ssrfun]
f:69 [in Coq.Reals.Rlimit]
f:690 [in Coq.MSets.MSetRBT]
f:691 [in Coq.FSets.FMapFacts]
f:692 [in Coq.MSets.MSetRBT]
f:694 [in Coq.MSets.MSetRBT]
f:7 [in Coq.Reals.Rderiv]
f:7 [in Coq.Floats.PrimFloat]
f:7 [in Coq.Floats.FloatOps]
f:7 [in Coq.Classes.CRelationClasses]
f:7 [in Coq.btauto.Reflect]
f:70 [in Coq.MSets.MSetProperties]
f:70 [in Coq.Logic.Hurkens]
f:70 [in Coq.NArith.BinNat]
f:70 [in Coq.Reals.RiemannInt_SF]
f:70 [in Coq.FSets.FSetProperties]
f:701 [in Coq.FSets.FMapFacts]
f:708 [in Coq.Init.Specif]
f:71 [in Coq.Reals.Ranalysis1]
F:71 [in Coq.Arith.Wf_nat]
f:71 [in Coq.Reals.Rtopology]
f:712 [in Coq.Lists.List]
f:716 [in Coq.ssr.ssrbool]
f:72 [in Coq.PArith.BinPos]
f:72 [in Coq.Numbers.Natural.Abstract.NBits]
f:72 [in Coq.micromega.Tauto]
f:721 [in Coq.Init.Specif]
f:722 [in Coq.Lists.List]
f:722 [in Coq.ssr.ssrbool]
f:727 [in Coq.ssr.ssrbool]
f:73 [in Coq.Reals.Ranalysis1]
f:73 [in Coq.Reals.Rseries]
f:73 [in Coq.Reals.Rtopology]
f:736 [in Coq.Init.Specif]
f:738 [in Coq.ssr.ssrbool]
f:74 [in Coq.Numbers.NaryFunctions]
f:74 [in Coq.Reals.RiemannInt]
f:74 [in Coq.NArith.BinNat]
f:74 [in Coq.Reals.Rlimit]
F:74 [in Coq.rtauto.Rtauto]
f:749 [in Coq.Init.Specif]
f:749 [in Coq.ssr.ssrbool]
F:75 [in Coq.Arith.Wf_nat]
f:75 [in Coq.Init.Datatypes]
f:76 [in Coq.Reals.Rderiv]
f:76 [in Coq.ssr.ssrfun]
f:76 [in Coq.Reals.Ranalysis5]
f:763 [in Coq.ssr.ssrbool]
f:77 [in Coq.Reals.Rseries]
f:77 [in Coq.FSets.FSetInterface]
f:77 [in Coq.ssr.ssrfun]
f:77 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:78 [in Coq.Reals.Ranalysis1]
f:78 [in Coq.Reals.MVT]
f:78 [in Coq.Logic.FunctionalExtensionality]
f:78 [in Coq.micromega.QMicromega]
f:79 [in Coq.Reals.Rsqrt_def]
f:79 [in Coq.Reals.RiemannInt]
f:79 [in Coq.ssr.ssrfun]
f:79 [in Coq.micromega.QMicromega]
f:79 [in Coq.Sorting.CPermutation]
f:79 [in Coq.Logic.FinFun]
f:8 [in Coq.Reals.Ranalysis4]
f:8 [in Coq.Floats.PrimFloat]
f:8 [in Coq.Floats.FloatOps]
f:8 [in Coq.Logic.ClassicalUniqueChoice]
F:8 [in Coq.micromega.DeclConstant]
f:8 [in Coq.Numbers.Natural.Abstract.NStrongRec]
f:8 [in Coq.Logic.FinFun]
f:80 [in Coq.Numbers.NaryFunctions]
f:81 [in Coq.Reals.MVT]
f:81 [in Coq.Logic.ChoiceFacts]
f:81 [in Coq.Numbers.Natural.Abstract.NBits]
f:81 [in Coq.MSets.MSetRBT]
f:81 [in Coq.Init.Datatypes]
f:81 [in Coq.Reals.RiemannInt_SF]
f:82 [in Coq.MSets.MSetProperties]
f:82 [in Coq.micromega.QMicromega]
f:82 [in Coq.Sorting.CPermutation]
f:82 [in Coq.FSets.FSetProperties]
f:82 [in Coq.Logic.FinFun]
f:83 [in Coq.PArith.BinPos]
f:83 [in Coq.micromega.RingMicromega]
F:83 [in Coq.Arith.Wf_nat]
f:83 [in Coq.Reals.Rlimit]
f:83 [in Coq.Reals.RiemannInt_SF]
f:84 [in Coq.Reals.MVT]
f:84 [in Coq.Reals.RiemannInt]
f:84 [in Coq.Reals.NewtonInt]
f:84 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:840 [in Coq.Init.Logic]
f:85 [in Coq.Floats.SpecFloat]
f:85 [in Coq.Reals.MVT]
f:85 [in Coq.FSets.FMapFacts]
f:85 [in Coq.FSets.FMapInterface]
f:85 [in Coq.Logic.FinFun]
f:86 [in Coq.ssr.ssrfun]
f:86 [in Coq.Reals.Rtopology]
f:86 [in Coq.PArith.BinPosDef]
f:865 [in Coq.Lists.List]
F:87 [in Coq.Arith.Wf_nat]
f:87 [in Coq.setoid_ring.Field_theory]
f:87 [in Coq.MSets.MSetAVL]
f:870 [in Coq.Init.Logic]
f:88 [in Coq.ZArith.BinIntDef]
f:88 [in Coq.PArith.BinPos]
f:88 [in Coq.FSets.FMapAVL]
f:88 [in Coq.Numbers.Cyclic.Int31.Int31]
f:88 [in Coq.Sorting.CPermutation]
f:88 [in Coq.Reals.Rlimit]
f:883 [in Coq.Init.Logic]
f:89 [in Coq.micromega.RingMicromega]
f:89 [in Coq.FSets.FMapFacts]
f:89 [in Coq.Logic.FunctionalExtensionality]
f:89 [in Coq.Logic.FinFun]
f:89 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:898 [in Coq.Init.Logic]
f:9 [in Coq.Floats.PrimFloat]
f:9 [in Coq.Classes.RelationPairs]
f:9 [in Coq.Logic.FunctionalExtensionality]
f:9 [in Coq.Reals.RiemannInt]
f:9 [in Coq.Relations.Relations]
f:9 [in Coq.Arith.PeanoNat]
f:9 [in Coq.Reals.Ratan]
f:90 [in Coq.ssr.ssrfun]
f:90 [in Coq.Reals.Rpower]
f:90 [in Coq.Reals.NewtonInt]
f:901 [in Coq.Lists.List]
f:91 [in Coq.Logic.ChoiceFacts]
f:91 [in Coq.FSets.FMapInterface]
f:91 [in Coq.ssr.ssrfun]
f:91 [in Coq.Classes.CMorphisms]
f:91 [in Coq.Reals.Rtopology]
f:91 [in Coq.Reals.PSeries_reg]
f:91 [in Coq.Reals.RiemannInt_SF]
f:911 [in Coq.Init.Logic]
f:92 [in Coq.FSets.FMapFacts]
f:92 [in Coq.Numbers.Integer.Abstract.ZBits]
f:92 [in Coq.micromega.ZMicromega]
f:93 [in Coq.Reals.Rsqrt_def]
f:93 [in Coq.MSets.MSetAVL]
f:93 [in Coq.Reals.Rtopology]
f:93 [in Coq.FSets.FSetCompat]
f:94 [in Coq.Reals.Rderiv]
f:94 [in Coq.Reals.MVT]
f:94 [in Coq.Logic.FunctionalExtensionality]
f:94 [in Coq.ssr.ssrfun]
f:94 [in Coq.MSets.MSetRBT]
f:94 [in Coq.Reals.RiemannInt_SF]
f:94 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:941 [in Coq.Init.Specif]
f:95 [in Coq.micromega.RingMicromega]
f:96 [in Coq.Reals.Ranalysis1]
f:96 [in Coq.FSets.FMapFacts]
f:96 [in Coq.Reals.Rpower]
F:96 [in Coq.rtauto.Bintree]
f:96 [in Coq.Reals.NewtonInt]
f:96 [in Coq.micromega.RMicromega]
f:97 [in Coq.MSets.MSetEqProperties]
f:97 [in Coq.Reals.MVT]
f:97 [in Coq.setoid_ring.Field_theory]
f:97 [in Coq.FSets.FSetEqProperties]
f:97 [in Coq.Reals.Rtopology]
f:97 [in Coq.Reals.RList]
f:970 [in Coq.Init.Specif]
f:98 [in Coq.Reals.MVT]
f:98 [in Coq.FSets.FMapInterface]
f:983 [in Coq.Lists.List]
f:983 [in Coq.Init.Specif]
f:99 [in Coq.Numbers.NaryFunctions]
f:99 [in Coq.Reals.Rtopology]
f:99 [in Coq.Reals.Rlimit]
f:99 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
f:99 [in Coq.FSets.FSetCompat]
f:998 [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) |