| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (68863 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (985 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (44709 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (761 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1497 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (570 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11380 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (976 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (603 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (298 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (460 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (476 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (811 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1157 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4018 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (162 entries) |
R (binder)
radd:290 [in Coq.setoid_ring.Ring_theory]radd:443 [in Coq.setoid_ring.Field_theory]
RA':50 [in Coq.Classes.Morphisms]
RA':52 [in Coq.Classes.Morphisms]
RA':52 [in Coq.Classes.CMorphisms]
RA':54 [in Coq.Classes.CMorphisms]
RA:105 [in Coq.Classes.RelationClasses]
RA:112 [in Coq.Classes.Morphisms]
RA:114 [in Coq.Classes.CRelationClasses]
RA:128 [in Coq.Classes.CMorphisms]
RA:17 [in Coq.Classes.RelationPairs]
RA:42 [in Coq.Classes.RelationPairs]
RA:49 [in Coq.Classes.Morphisms]
RA:51 [in Coq.Classes.CMorphisms]
RA:53 [in Coq.Classes.Morphisms]
RA:55 [in Coq.Classes.CMorphisms]
RA:81 [in Coq.Classes.Morphisms]
RA:84 [in Coq.Classes.Morphisms]
RA:88 [in Coq.Classes.CMorphisms]
RB':56 [in Coq.Classes.Morphisms]
RB':59 [in Coq.Classes.CMorphisms]
RB:113 [in Coq.Classes.Morphisms]
RB:129 [in Coq.Classes.CMorphisms]
RB:18 [in Coq.Classes.RelationPairs]
RB:43 [in Coq.Classes.RelationPairs]
RB:55 [in Coq.Classes.Morphisms]
RB:58 [in Coq.Classes.CMorphisms]
RB:85 [in Coq.Classes.Morphisms]
RB:89 [in Coq.Classes.CMorphisms]
Rcr:11 [in Coq.setoid_ring.Integral_domain]
RC:114 [in Coq.Classes.Morphisms]
RC:130 [in Coq.Classes.CMorphisms]
RC:86 [in Coq.Classes.Morphisms]
RC:90 [in Coq.Classes.CMorphisms]
rdiv:445 [in Coq.setoid_ring.Field_theory]
rect:14 [in Coq.Vectors.VectorDef]
rect:60 [in Coq.Vectors.VectorDef]
rec:112 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
rec:120 [in Coq.Numbers.Cyclic.Int31.Int31]
rec:125 [in Coq.Numbers.Cyclic.Int31.Int31]
rec:133 [in Coq.Numbers.Cyclic.Int31.Int31]
rec:140 [in Coq.Numbers.Cyclic.Int31.Int31]
rec:164 [in Coq.Numbers.Cyclic.Int63.Int63]
rec:165 [in Coq.Numbers.Cyclic.Int31.Int31]
rec:169 [in Coq.Numbers.Cyclic.Int63.Int63]
rec:171 [in Coq.Numbers.Cyclic.Int31.Int31]
rec:179 [in Coq.Numbers.Cyclic.Int63.Int63]
rec:185 [in Coq.Numbers.Cyclic.Int63.Int63]
rec:305 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
rec:310 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
rec:315 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
rec:320 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
rec:331 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
rec:337 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
rec:388 [in Coq.Numbers.Cyclic.Int63.Int63]
rec:393 [in Coq.Numbers.Cyclic.Int63.Int63]
rec:399 [in Coq.Numbers.Cyclic.Int63.Int63]
rec:40 [in Coq.Numbers.Cyclic.Int31.Int31]
rec:416 [in Coq.Numbers.Cyclic.Int63.Int63]
rec:422 [in Coq.Numbers.Cyclic.Int63.Int63]
rec:66 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
rec:91 [in Coq.Numbers.Cyclic.Int31.Int31]
reflb:36 [in Coq.Classes.CEquivalence]
reflb:36 [in Coq.Classes.Equivalence]
repr:3 [in Coq.Logic.ExtensionalFunctionRepresentative]
reqb:284 [in Coq.setoid_ring.Ring_theory]
req:283 [in Coq.setoid_ring.Ring_theory]
req:294 [in Coq.setoid_ring.Ring_theory]
req:447 [in Coq.setoid_ring.Field_theory]
rest:11 [in Coq.Strings.OctalString]
rest:11 [in Coq.Strings.HexString]
rest:11 [in Coq.Strings.BinaryString]
rest:15 [in Coq.Strings.OctalString]
rest:15 [in Coq.Strings.HexString]
rest:15 [in Coq.Strings.BinaryString]
rest:7 [in Coq.Strings.OctalString]
rest:7 [in Coq.Strings.HexString]
rest:7 [in Coq.Strings.BinaryString]
rest:77 [in Coq.ssr.ssreflect]
rest:82 [in Coq.ssr.ssreflect]
rest:86 [in Coq.ssr.ssreflect]
result:122 [in Coq.ssr.ssreflect]
result:127 [in Coq.ssr.ssreflect]
result:135 [in Coq.ssr.ssreflect]
res:102 [in Coq.Numbers.Cyclic.Int31.Int31]
res:157 [in Coq.setoid_ring.Ncring_polynom]
res:174 [in Coq.setoid_ring.Ncring_polynom]
res:250 [in Coq.setoid_ring.Field_theory]
res:329 [in Coq.setoid_ring.Ring_polynom]
res:338 [in Coq.setoid_ring.Ring_polynom]
res:343 [in Coq.micromega.EnvRing]
res:352 [in Coq.micromega.EnvRing]
rF:188 [in Coq.ssr.ssrfun]
rf:90 [in Coq.FSets.FSetPositive]
rf:90 [in Coq.MSets.MSetPositive]
rhs:204 [in Coq.micromega.RingMicromega]
rhs:208 [in Coq.micromega.RingMicromega]
rhs:210 [in Coq.micromega.RingMicromega]
rhs:215 [in Coq.micromega.RingMicromega]
rhs:217 [in Coq.micromega.RingMicromega]
rhs:221 [in Coq.micromega.RingMicromega]
rhs:224 [in Coq.micromega.RingMicromega]
rhs:227 [in Coq.micromega.RingMicromega]
rhs:28 [in Coq.micromega.QMicromega]
rhs:310 [in Coq.micromega.RingMicromega]
rhs:38 [in Coq.micromega.ZMicromega]
rhs:63 [in Coq.micromega.RMicromega]
rhs:66 [in Coq.micromega.ZMicromega]
rhs:69 [in Coq.micromega.ZMicromega]
rhs:72 [in Coq.micromega.ZMicromega]
rhs:80 [in Coq.micromega.ZMicromega]
rhs:82 [in Coq.micromega.ZMicromega]
Rh:171 [in Coq.setoid_ring.Ncring]
Rh:22 [in Coq.setoid_ring.Ncring_polynom]
Rid:12 [in Coq.nsatz.NsatzTactic]
Rid:28 [in Coq.setoid_ring.Integral_domain]
right:582 [in Coq.Lists.List]
ring_eq:8 [in Coq.setoid_ring.Ncring]
ring0:2 [in Coq.setoid_ring.Ncring]
ring1:3 [in Coq.setoid_ring.Ncring]
rinv:446 [in Coq.setoid_ring.Field_theory]
rI:289 [in Coq.setoid_ring.Ring_theory]
rI:442 [in Coq.setoid_ring.Field_theory]
Ri:53 [in Coq.Classes.RelationPairs]
rl:346 [in Coq.MSets.MSetRBT]
rl:356 [in Coq.MSets.MSetRBT]
rl:60 [in Coq.MSets.MSetAVL]
rl:61 [in Coq.MSets.MSetAVL]
rl:73 [in Coq.FSets.FMapAVL]
rl:74 [in Coq.FSets.FMapAVL]
rmnz:192 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
rmnz:314 [in Coq.Reals.Abstract.ConstructiveReals]
rmul:291 [in Coq.setoid_ring.Ring_theory]
rmul:444 [in Coq.setoid_ring.Field_theory]
rnz:157 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
rnz:166 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
rnz:184 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
rnz:186 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
rnz:282 [in Coq.Reals.Abstract.ConstructiveReals]
rnz:71 [in Coq.Reals.Abstract.ConstructiveReals]
rnz:74 [in Coq.Reals.Abstract.ConstructiveReals]
ropp:293 [in Coq.setoid_ring.Ring_theory]
Rops_wd:169 [in Coq.micromega.RingMicromega]
Rops_wd:165 [in Coq.micromega.RingMicromega]
rOp:191 [in Coq.ssr.ssrfun]
rO:288 [in Coq.setoid_ring.Ring_theory]
rO:441 [in Coq.setoid_ring.Field_theory]
Ro:54 [in Coq.Classes.RelationPairs]
Ro:81 [in Coq.setoid_ring.Ncring]
rP:195 [in Coq.ssr.ssrfun]
rP:202 [in Coq.ssr.ssrfun]
rP:410 [in Coq.setoid_ring.Ring_polynom]
rP:417 [in Coq.setoid_ring.Ring_polynom]
rP:425 [in Coq.setoid_ring.Ring_polynom]
rP:432 [in Coq.setoid_ring.Ring_polynom]
rP:462 [in Coq.setoid_ring.Ring_polynom]
rP:469 [in Coq.setoid_ring.Ring_polynom]
Rr:10 [in Coq.setoid_ring.Cring]
Rr:170 [in Coq.setoid_ring.Ncring]
rR:198 [in Coq.ssr.ssrfun]
Rr:198 [in Coq.setoid_ring.Ncring]
rR:205 [in Coq.ssr.ssrfun]
Rr:209 [in Coq.setoid_ring.Ncring_tac]
Rr:219 [in Coq.setoid_ring.Ncring_tac]
Rr:234 [in Coq.setoid_ring.Ncring_tac]
Rr:249 [in Coq.setoid_ring.Ncring_tac]
Rr:262 [in Coq.setoid_ring.Ncring_tac]
Rr:27 [in Coq.setoid_ring.Cring]
Rr:30 [in Coq.setoid_ring.Ncring_tac]
rr:348 [in Coq.MSets.MSetRBT]
rr:358 [in Coq.MSets.MSetRBT]
rr:63 [in Coq.MSets.MSetAVL]
rr:76 [in Coq.FSets.FMapAVL]
Rsth:448 [in Coq.setoid_ring.Field_theory]
rst_f':116 [in Coq.micromega.Tauto]
rsub:292 [in Coq.setoid_ring.Ring_theory]
rT:12 [in Coq.ssr.ssrfun]
rT:20 [in Coq.ssr.ssrfun]
rT:23 [in Coq.ssr.ssrfun]
rT:280 [in Coq.ssr.ssrbool]
rT:318 [in Coq.ssr.ssrbool]
rT:37 [in Coq.ssr.ssreflect]
rT:38 [in Coq.ssr.ssrfun]
rT:581 [in Coq.ssr.ssrbool]
rT:587 [in Coq.ssr.ssrbool]
rT:59 [in Coq.ssr.ssrfun]
rT:69 [in Coq.Numbers.Cyclic.Int63.Int63]
rt:89 [in Coq.FSets.FSetPositive]
rt:89 [in Coq.MSets.MSetPositive]
rU:45 [in Coq.Logic.Berardi]
Rwf:125 [in Coq.Program.Wf]
rxnz:195 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
rxnz:318 [in Coq.Reals.Abstract.ConstructiveReals]
rx:347 [in Coq.MSets.MSetRBT]
rx:357 [in Coq.MSets.MSetRBT]
rynz:196 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
rynz:319 [in Coq.Reals.Abstract.ConstructiveReals]
R''':162 [in Coq.Classes.Morphisms]
R''':191 [in Coq.Classes.CMorphisms]
R'':165 [in Coq.Classes.Morphisms]
R'':195 [in Coq.Classes.CMorphisms]
R':102 [in Coq.Logic.ChoiceFacts]
R':115 [in Coq.Classes.Morphisms]
R':118 [in Coq.Classes.Morphisms]
R':12 [in Coq.Sets.Relations_1]
R':120 [in Coq.Logic.ChoiceFacts]
R':120 [in Coq.Classes.CRelationClasses]
R':124 [in Coq.Classes.Morphisms]
R':124 [in Coq.Classes.CRelationClasses]
R':125 [in Coq.Classes.Morphisms]
R':128 [in Coq.Classes.CRelationClasses]
R':129 [in Coq.Classes.Morphisms]
R':132 [in Coq.Classes.CMorphisms]
R':138 [in Coq.Classes.RelationClasses]
R':140 [in Coq.Classes.RelationClasses]
R':140 [in Coq.Classes.CMorphisms]
R':147 [in Coq.Classes.RelationClasses]
R':149 [in Coq.Classes.RelationClasses]
R':15 [in Coq.Sets.Relations_3_facts]
R':152 [in Coq.Classes.CMorphisms]
R':154 [in Coq.Classes.CMorphisms]
r':158 [in Coq.Numbers.Cyclic.Int63.Int63]
R':159 [in Coq.Classes.CMorphisms]
R':16 [in Coq.Sets.Relations_1]
R':163 [in Coq.Classes.RelationClasses]
R':164 [in Coq.Classes.Morphisms]
R':165 [in Coq.Classes.RelationClasses]
R':19 [in Coq.Sets.Relations_1_facts]
R':193 [in Coq.Classes.Morphisms]
R':194 [in Coq.Classes.CMorphisms]
R':20 [in Coq.Classes.CEquivalence]
R':20 [in Coq.Classes.Equivalence]
R':22 [in Coq.Sets.Relations_1_facts]
R':228 [in Coq.Classes.CMorphisms]
r':235 [in Coq.ZArith.Zdiv]
R':236 [in Coq.Classes.CMorphisms]
r':237 [in Coq.ZArith.Zdiv]
R':24 [in Coq.Classes.CMorphisms]
R':25 [in Coq.Classes.Morphisms]
R':25 [in Coq.Sets.Relations_1_facts]
R':27 [in Coq.Classes.CEquivalence]
R':27 [in Coq.Classes.Equivalence]
R':28 [in Coq.Sets.Relations_1_facts]
R':33 [in Coq.Classes.Morphisms]
R':33 [in Coq.Classes.CMorphisms]
R':387 [in Coq.Init.Logic]
R':4 [in Coq.Logic.RelationalChoice]
R':5 [in Coq.Logic.ChoiceFacts]
R':5 [in Coq.Numbers.Cyclic.Int63.Ring63]
R':5 [in Coq.Numbers.Cyclic.Int31.Ring31]
R':59 [in Coq.Classes.Morphisms]
R':60 [in Coq.Classes.RelationClasses]
R':62 [in Coq.Classes.CMorphisms]
r':63 [in Coq.NArith.BinNatDef]
R':66 [in Coq.Classes.Morphisms]
r':66 [in Coq.NArith.BinNatDef]
R':69 [in Coq.Classes.CRelationClasses]
R':70 [in Coq.Classes.CMorphisms]
R':79 [in Coq.Classes.Morphisms]
R':83 [in Coq.Classes.CMorphisms]
r':91 [in Coq.PArith.BinPosDef]
r':92 [in Coq.MSets.MSetAVL]
r':96 [in Coq.ZArith.BinIntDef]
r':99 [in Coq.ZArith.BinIntDef]
r0:114 [in Coq.Reals.RList]
R0:153 [in Coq.Classes.Morphisms]
R0:183 [in Coq.Classes.CMorphisms]
r0:195 [in Coq.Reals.RiemannInt_SF]
r0:197 [in Coq.Reals.RiemannInt_SF]
r0:217 [in Coq.Reals.RiemannInt_SF]
r0:219 [in Coq.Reals.RiemannInt_SF]
r1nz:190 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r1nz:312 [in Coq.Reals.Abstract.ConstructiveReals]
r1:1 [in Coq.Reals.ROrderedType]
R1:1 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
R1:10 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:102 [in Coq.Reals.RIneq]
R1:102 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:105 [in Coq.Reals.RIneq]
R1:107 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:108 [in Coq.Reals.RIneq]
r1:11 [in Coq.Reals.RIneq]
r1:110 [in Coq.Reals.RIneq]
r1:112 [in Coq.Reals.RIneq]
R1:112 [in Coq.Reals.Abstract.ConstructiveMinMax]
R1:112 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:114 [in Coq.Reals.RIneq]
r1:114 [in Coq.Reals.RiemannInt_SF]
r1:116 [in Coq.Reals.RIneq]
r1:117 [in Coq.Reals.Abstract.ConstructiveReals]
r1:117 [in Coq.Reals.RList]
r1:118 [in Coq.Reals.RIneq]
r1:118 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R1:118 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:12 [in Coq.Reals.Rbasic_fun]
r1:12 [in Coq.Numbers.NatInt.NZDiv]
r1:120 [in Coq.Reals.RIneq]
r1:121 [in Coq.Reals.Abstract.ConstructiveReals]
r1:122 [in Coq.Reals.RIneq]
R1:123 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:124 [in Coq.Reals.RIneq]
r1:126 [in Coq.Reals.RIneq]
r1:127 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r1:128 [in Coq.Reals.RIneq]
R1:129 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:13 [in Coq.Reals.RIneq]
r1:13 [in Coq.micromega.RMicromega]
r1:130 [in Coq.Reals.RIneq]
r1:132 [in Coq.Reals.RIneq]
r1:132 [in Coq.Reals.RiemannInt_SF]
r1:134 [in Coq.Reals.RIneq]
R1:135 [in Coq.setoid_ring.Ring_polynom]
r1:14 [in Coq.Reals.R_Ifp]
r1:14 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
r1:141 [in Coq.Reals.RIneq]
R1:142 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:144 [in Coq.Reals.RIneq]
R1:145 [in Coq.micromega.EnvRing]
R1:146 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:147 [in Coq.Reals.RIneq]
r1:147 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
R1:149 [in Coq.micromega.EnvRing]
r1:149 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r1:15 [in Coq.Reals.Rbasic_fun]
r1:15 [in Coq.Reals.RIneq]
r1:15 [in Coq.micromega.RMicromega]
R1:15 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
R1:150 [in Coq.setoid_ring.Ring_polynom]
R1:151 [in Coq.micromega.EnvRing]
r1:151 [in Coq.Reals.SeqProp]
r1:152 [in Coq.Reals.RIneq]
R1:153 [in Coq.micromega.EnvRing]
r1:153 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
R1:153 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
R1:154 [in Coq.setoid_ring.Ring_polynom]
R1:154 [in Coq.Classes.Morphisms]
r1:155 [in Coq.Reals.RIneq]
R1:156 [in Coq.setoid_ring.Ring_polynom]
R1:158 [in Coq.setoid_ring.Ring_polynom]
r1:158 [in Coq.Reals.RIneq]
R1:159 [in Coq.micromega.EnvRing]
r1:159 [in Coq.Reals.RIneq]
r1:16 [in Coq.Reals.R_Ifp]
r1:16 [in Coq.Reals.Raxioms]
r1:16 [in Coq.Numbers.NatInt.NZDiv]
r1:161 [in Coq.Reals.RIneq]
r1:164 [in Coq.Reals.Abstract.ConstructiveReals]
R1:165 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
R1:166 [in Coq.setoid_ring.Ring_polynom]
r1:166 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r1:168 [in Coq.Reals.Abstract.ConstructiveReals]
R1:168 [in Coq.Classes.Morphisms]
r1:168 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r1:17 [in Coq.Reals.RIneq]
r1:17 [in Coq.micromega.RMicromega]
r1:171 [in Coq.Reals.RIneq]
r1:171 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r1:172 [in Coq.Reals.Abstract.ConstructiveReals]
r1:173 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r1:174 [in Coq.Reals.RIneq]
R1:175 [in Coq.Classes.Morphisms]
r1:176 [in Coq.Reals.Abstract.ConstructiveReals]
r1:177 [in Coq.Reals.RIneq]
r1:179 [in Coq.Reals.Abstract.ConstructiveReals]
r1:18 [in Coq.Reals.R_Ifp]
r1:18 [in Coq.Reals.Raxioms]
r1:18 [in Coq.Reals.ClassicalConstructiveReals]
r1:180 [in Coq.Reals.RIneq]
r1:182 [in Coq.Reals.RIneq]
R1:183 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
R1:184 [in Coq.Classes.CMorphisms]
r1:184 [in Coq.Reals.RIneq]
r1:186 [in Coq.Reals.RIneq]
R1:187 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:188 [in Coq.Reals.Abstract.ConstructiveReals]
r1:188 [in Coq.Reals.RIneq]
r1:188 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R1:189 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:19 [in Coq.Reals.RIneq]
r1:19 [in Coq.micromega.RMicromega]
r1:190 [in Coq.Reals.RIneq]
r1:192 [in Coq.Reals.Abstract.ConstructiveReals]
r1:192 [in Coq.Reals.RIneq]
R1:193 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:194 [in Coq.Reals.RIneq]
r1:195 [in Coq.Reals.Abstract.ConstructiveReals]
r1:196 [in Coq.Reals.RIneq]
R1:197 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
R1:198 [in Coq.Classes.CMorphisms]
r1:198 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r1:20 [in Coq.Reals.R_Ifp]
r1:20 [in Coq.Numbers.NatInt.NZDiv]
r1:200 [in Coq.Reals.Abstract.ConstructiveReals]
r1:201 [in Coq.Reals.RIneq]
r1:201 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R1:201 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:204 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R1:205 [in Coq.Classes.CMorphisms]
r1:206 [in Coq.Reals.Abstract.ConstructiveReals]
r1:206 [in Coq.Reals.RIneq]
r1:207 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R1:207 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:208 [in Coq.Reals.RIneq]
r1:21 [in Coq.Reals.RIneq]
r1:210 [in Coq.Reals.Abstract.ConstructiveReals]
r1:210 [in Coq.Reals.RIneq]
r1:210 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r1:212 [in Coq.Reals.RIneq]
r1:214 [in Coq.Reals.Abstract.ConstructiveReals]
r1:214 [in Coq.Reals.RIneq]
r1:216 [in Coq.Reals.RIneq]
r1:217 [in Coq.Reals.Abstract.ConstructiveReals]
r1:219 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r1:22 [in Coq.Reals.R_Ifp]
r1:22 [in Coq.Reals.PSeries_reg]
r1:220 [in Coq.Reals.RIneq]
r1:222 [in Coq.Reals.RIneq]
r1:224 [in Coq.Reals.RIneq]
r1:227 [in Coq.Reals.RIneq]
r1:229 [in Coq.Reals.RIneq]
r1:23 [in Coq.Reals.Raxioms]
r1:23 [in Coq.Reals.RIneq]
R1:23 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:230 [in Coq.Reals.Abstract.ConstructiveReals]
r1:231 [in Coq.Reals.RIneq]
r1:233 [in Coq.Reals.Abstract.ConstructiveReals]
r1:233 [in Coq.Reals.RIneq]
r1:233 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r1:235 [in Coq.Reals.RIneq]
r1:236 [in Coq.Reals.Abstract.ConstructiveReals]
r1:236 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r1:237 [in Coq.Reals.RIneq]
r1:239 [in Coq.Reals.Abstract.ConstructiveReals]
r1:239 [in Coq.Reals.RIneq]
R1:239 [in Coq.Reals.Abstract.ConstructiveSum]
r1:24 [in Coq.Reals.R_Ifp]
r1:242 [in Coq.Reals.RIneq]
r1:245 [in Coq.setoid_ring.Field_theory]
R1:245 [in Coq.Reals.Abstract.ConstructiveSum]
r1:247 [in Coq.Reals.Abstract.ConstructiveReals]
r1:247 [in Coq.Reals.RIneq]
R1:249 [in Coq.Reals.Abstract.ConstructiveSum]
r1:25 [in Coq.Reals.Raxioms]
r1:25 [in Coq.Reals.RIneq]
R1:25 [in Coq.Relations.Relation_Definitions]
r1:250 [in Coq.Reals.RIneq]
r1:252 [in Coq.Reals.RIneq]
r1:253 [in Coq.Reals.Abstract.ConstructiveReals]
r1:254 [in Coq.Reals.RIneq]
r1:256 [in Coq.Reals.RIneq]
r1:257 [in Coq.Reals.Abstract.ConstructiveReals]
r1:26 [in Coq.Reals.R_Ifp]
r1:260 [in Coq.Reals.RIneq]
r1:263 [in Coq.Reals.RIneq]
r1:266 [in Coq.Reals.RIneq]
r1:267 [in Coq.Reals.Abstract.ConstructiveReals]
r1:269 [in Coq.Reals.RIneq]
r1:27 [in Coq.Reals.RIneq]
r1:270 [in Coq.Reals.Abstract.ConstructiveReals]
r1:272 [in Coq.Reals.RIneq]
r1:274 [in Coq.Reals.Abstract.ConstructiveReals]
r1:275 [in Coq.Reals.RIneq]
r1:278 [in Coq.Reals.Abstract.ConstructiveReals]
r1:278 [in Coq.Reals.RIneq]
r1:28 [in Coq.Reals.R_Ifp]
R1:28 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:280 [in Coq.Reals.RIneq]
r1:284 [in Coq.Reals.RIneq]
r1:285 [in Coq.Reals.Abstract.ConstructiveReals]
r1:288 [in Coq.Reals.RIneq]
r1:289 [in Coq.Reals.Abstract.ConstructiveReals]
r1:29 [in Coq.Reals.RIneq]
R1:29 [in Coq.Relations.Relation_Definitions]
r1:292 [in Coq.Reals.RIneq]
r1:293 [in Coq.Reals.Abstract.ConstructiveReals]
r1:295 [in Coq.ssr.ssrbool]
r1:296 [in Coq.Reals.RIneq]
r1:297 [in Coq.Reals.Abstract.ConstructiveReals]
r1:3 [in Coq.Reals.Rbasic_fun]
r1:3 [in Coq.Reals.ROrderedType]
r1:30 [in Coq.Reals.Raxioms]
r1:300 [in Coq.Reals.RIneq]
r1:301 [in Coq.Reals.Abstract.ConstructiveReals]
r1:303 [in Coq.ssr.ssrbool]
r1:304 [in Coq.Reals.RIneq]
r1:307 [in Coq.Reals.Abstract.ConstructiveReals]
r1:308 [in Coq.Reals.RIneq]
r1:31 [in Coq.Reals.RIneq]
R1:31 [in Coq.Relations.Relation_Definitions]
r1:310 [in Coq.Reals.Abstract.ConstructiveReals]
r1:312 [in Coq.Reals.RIneq]
r1:314 [in Coq.Reals.RIneq]
r1:315 [in Coq.ssr.ssrbool]
r1:316 [in Coq.Reals.RIneq]
r1:318 [in Coq.Reals.RIneq]
r1:32 [in Coq.Reals.PartSum]
r1:326 [in Coq.ssr.ssrbool]
r1:327 [in Coq.Reals.RIneq]
r1:328 [in Coq.MSets.MSetGenTree]
r1:329 [in Coq.ssr.ssrbool]
r1:33 [in Coq.Reals.Raxioms]
r1:33 [in Coq.Reals.RIneq]
r1:330 [in Coq.Reals.RIneq]
r1:333 [in Coq.Reals.RIneq]
r1:336 [in Coq.Reals.RIneq]
r1:339 [in Coq.Reals.RIneq]
r1:342 [in Coq.Reals.RIneq]
r1:343 [in Coq.Reals.Abstract.ConstructiveReals]
r1:344 [in Coq.Reals.RIneq]
r1:347 [in Coq.Reals.Abstract.ConstructiveReals]
r1:347 [in Coq.Reals.RIneq]
r1:35 [in Coq.Reals.Raxioms]
r1:35 [in Coq.Reals.RIneq]
R1:35 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:350 [in Coq.Reals.RIneq]
r1:353 [in Coq.Reals.RIneq]
r1:356 [in Coq.Reals.RIneq]
r1:358 [in Coq.Reals.RIneq]
r1:360 [in Coq.Reals.RIneq]
r1:362 [in Coq.Reals.RIneq]
r1:364 [in Coq.Reals.RIneq]
r1:366 [in Coq.Reals.RIneq]
r1:368 [in Coq.Reals.RIneq]
r1:37 [in Coq.Reals.RIneq]
r1:370 [in Coq.Reals.RIneq]
r1:371 [in Coq.Reals.Abstract.ConstructiveReals]
r1:375 [in Coq.Reals.Abstract.ConstructiveReals]
r1:378 [in Coq.Reals.RIneq]
r1:379 [in Coq.Reals.Abstract.ConstructiveReals]
r1:380 [in Coq.Reals.RIneq]
r1:382 [in Coq.Reals.RIneq]
r1:383 [in Coq.Reals.Abstract.ConstructiveReals]
r1:384 [in Coq.Reals.RIneq]
r1:387 [in Coq.Reals.RIneq]
r1:39 [in Coq.Reals.Raxioms]
r1:39 [in Coq.Reals.RIneq]
r1:390 [in Coq.Reals.RIneq]
r1:393 [in Coq.Reals.RIneq]
r1:396 [in Coq.Reals.RIneq]
r1:399 [in Coq.Reals.RIneq]
r1:4 [in Coq.QArith.Qreduction]
R1:40 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:402 [in Coq.Reals.RIneq]
r1:405 [in Coq.Reals.RIneq]
r1:407 [in Coq.Reals.RIneq]
r1:41 [in Coq.ZArith.Zdiv]
r1:41 [in Coq.Reals.RIneq]
r1:417 [in Coq.Reals.RIneq]
r1:42 [in Coq.Reals.Rdefinitions]
r1:42 [in Coq.Reals.Raxioms]
r1:421 [in Coq.Reals.RIneq]
r1:425 [in Coq.Reals.RIneq]
r1:429 [in Coq.Reals.RIneq]
r1:43 [in Coq.Reals.RIneq]
r1:431 [in Coq.Reals.RIneq]
r1:434 [in Coq.Reals.RIneq]
r1:437 [in Coq.Reals.RIneq]
r1:44 [in Coq.Reals.Rdefinitions]
r1:440 [in Coq.Reals.RIneq]
r1:443 [in Coq.Reals.RIneq]
r1:446 [in Coq.Reals.RIneq]
r1:449 [in Coq.Reals.RIneq]
r1:45 [in Coq.Reals.RIneq]
R1:45 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:452 [in Coq.Reals.RIneq]
r1:455 [in Coq.Reals.RIneq]
r1:457 [in Coq.Reals.RIneq]
r1:459 [in Coq.Reals.RIneq]
r1:46 [in Coq.Reals.Rdefinitions]
r1:46 [in Coq.ZArith.Zdiv]
r1:46 [in Coq.Reals.Rbasic_fun]
r1:463 [in Coq.Reals.RIneq]
r1:465 [in Coq.Reals.RIneq]
r1:467 [in Coq.Reals.RIneq]
r1:469 [in Coq.Reals.RIneq]
r1:47 [in Coq.Reals.RIneq]
r1:473 [in Coq.Reals.RIneq]
r1:475 [in Coq.Reals.RIneq]
r1:48 [in Coq.Reals.Rdefinitions]
R1:48 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:481 [in Coq.Reals.RIneq]
r1:483 [in Coq.Reals.RIneq]
r1:487 [in Coq.Reals.RIneq]
r1:489 [in Coq.Reals.RIneq]
r1:49 [in Coq.Reals.Rbasic_fun]
r1:49 [in Coq.Reals.RIneq]
r1:493 [in Coq.Reals.RIneq]
r1:5 [in Coq.Reals.RIneq]
r1:5 [in Coq.Reals.ROrderedType]
r1:51 [in Coq.Reals.RIneq]
R1:51 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:52 [in Coq.Reals.Rbasic_fun]
r1:53 [in Coq.Reals.RIneq]
r1:53 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r1:55 [in Coq.setoid_ring.Field_theory]
r1:55 [in Coq.Reals.RIneq]
r1:57 [in Coq.Reals.Rdefinitions]
r1:57 [in Coq.Reals.RIneq]
r1:573 [in Coq.Reals.RIneq]
r1:58 [in Coq.Reals.Abstract.ConstructiveReals]
r1:583 [in Coq.Reals.RIneq]
r1:584 [in Coq.Reals.RIneq]
r1:587 [in Coq.Reals.RIneq]
r1:59 [in Coq.Reals.RIneq]
r1:591 [in Coq.Reals.RIneq]
r1:6 [in Coq.Reals.Rbasic_fun]
r1:605 [in Coq.Reals.RIneq]
r1:61 [in Coq.Reals.RIneq]
R1:61 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:62 [in Coq.Reals.Abstract.ConstructiveReals]
r1:63 [in Coq.Reals.RIneq]
r1:65 [in Coq.Reals.RIneq]
R1:66 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:67 [in Coq.Reals.Rdefinitions]
r1:67 [in Coq.Reals.RIneq]
r1:69 [in Coq.Reals.RIneq]
r1:7 [in Coq.Reals.RIneq]
r1:70 [in Coq.FSets.FSetDecide]
r1:70 [in Coq.MSets.MSetDecide]
r1:71 [in Coq.Reals.RIneq]
r1:73 [in Coq.Reals.RIneq]
r1:74 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r1:75 [in Coq.Reals.RIneq]
R1:75 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:77 [in Coq.Reals.RIneq]
r1:77 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r1:79 [in Coq.Reals.RIneq]
r1:8 [in Coq.Numbers.Natural.Abstract.NDiv]
r1:8 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
R1:82 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:83 [in Coq.Reals.RIneq]
r1:87 [in Coq.Reals.RIneq]
R1:87 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:88 [in Coq.Reals.RiemannInt_SF]
r1:9 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
r1:9 [in Coq.Reals.Rbasic_fun]
r1:9 [in Coq.Reals.RIneq]
r1:90 [in Coq.Reals.RIneq]
R1:92 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:93 [in Coq.Reals.RIneq]
r1:96 [in Coq.Reals.RIneq]
R1:97 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r1:99 [in Coq.MSets.MSetAVL]
r1:99 [in Coq.Reals.RIneq]
r2nz:191 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r2nz:313 [in Coq.Reals.Abstract.ConstructiveReals]
r2':145 [in Coq.FSets.FMapAVL]
r2':71 [in Coq.MSets.MSetAVL]
r2':79 [in Coq.MSets.MSetAVL]
r2':86 [in Coq.MSets.MSetAVL]
r2:10 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
r2:10 [in Coq.Reals.Rbasic_fun]
r2:10 [in Coq.Reals.RIneq]
r2:100 [in Coq.MSets.MSetAVL]
r2:100 [in Coq.Reals.RIneq]
r2:103 [in Coq.Reals.RIneq]
R2:103 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:106 [in Coq.Reals.RIneq]
R2:108 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:109 [in Coq.Reals.RIneq]
R2:11 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:111 [in Coq.Reals.RIneq]
r2:113 [in Coq.Reals.RIneq]
R2:113 [in Coq.Reals.Abstract.ConstructiveMinMax]
R2:113 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:115 [in Coq.Reals.RIneq]
r2:117 [in Coq.Reals.RIneq]
r2:118 [in Coq.Reals.Abstract.ConstructiveReals]
r2:119 [in Coq.Reals.RIneq]
r2:119 [in Coq.Reals.RiemannInt_SF]
r2:119 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R2:119 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:12 [in Coq.Reals.RIneq]
r2:121 [in Coq.Reals.RIneq]
r2:122 [in Coq.Reals.Abstract.ConstructiveReals]
r2:123 [in Coq.Reals.RIneq]
R2:124 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:125 [in Coq.Reals.RIneq]
r2:1257 [in Coq.FSets.FMapAVL]
r2:127 [in Coq.Reals.RIneq]
r2:128 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r2:129 [in Coq.Reals.RIneq]
r2:13 [in Coq.Reals.Rbasic_fun]
r2:13 [in Coq.Numbers.NatInt.NZDiv]
R2:130 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:131 [in Coq.Reals.RIneq]
r2:133 [in Coq.Reals.RIneq]
r2:135 [in Coq.Reals.RIneq]
R2:137 [in Coq.setoid_ring.Ring_polynom]
r2:137 [in Coq.Reals.RiemannInt_SF]
r2:14 [in Coq.Reals.RIneq]
r2:14 [in Coq.micromega.RMicromega]
r2:142 [in Coq.Reals.RIneq]
R2:143 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:145 [in Coq.Reals.RIneq]
R2:147 [in Coq.micromega.EnvRing]
R2:147 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:148 [in Coq.Reals.RIneq]
r2:148 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r2:15 [in Coq.Reals.R_Ifp]
r2:15 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
r2:150 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
R2:152 [in Coq.setoid_ring.Ring_polynom]
r2:152 [in Coq.Reals.SeqProp]
r2:153 [in Coq.Reals.RIneq]
r2:154 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
R2:154 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:1540 [in Coq.FSets.FMapAVL]
r2:156 [in Coq.Reals.RIneq]
r2:16 [in Coq.Reals.Rbasic_fun]
r2:16 [in Coq.Reals.RIneq]
r2:16 [in Coq.micromega.RMicromega]
R2:16 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:160 [in Coq.Reals.RIneq]
r2:162 [in Coq.Reals.RIneq]
r2:165 [in Coq.Reals.Abstract.ConstructiveReals]
R2:166 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:167 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r2:169 [in Coq.Reals.Abstract.ConstructiveReals]
r2:169 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r2:17 [in Coq.Reals.R_Ifp]
r2:17 [in Coq.Reals.Raxioms]
r2:17 [in Coq.Numbers.NatInt.NZDiv]
R2:171 [in Coq.Classes.Morphisms]
r2:172 [in Coq.Reals.RIneq]
r2:172 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r2:173 [in Coq.Reals.Abstract.ConstructiveReals]
r2:174 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r2:175 [in Coq.Reals.RIneq]
r2:177 [in Coq.Reals.Abstract.ConstructiveReals]
R2:178 [in Coq.Classes.Morphisms]
r2:178 [in Coq.Reals.RIneq]
r2:18 [in Coq.Reals.RIneq]
r2:18 [in Coq.micromega.RMicromega]
r2:180 [in Coq.Reals.Abstract.ConstructiveReals]
r2:181 [in Coq.Reals.RIneq]
r2:183 [in Coq.Reals.RIneq]
R2:184 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:185 [in Coq.Reals.RIneq]
r2:187 [in Coq.Reals.RIneq]
R2:188 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:189 [in Coq.Reals.Abstract.ConstructiveReals]
r2:189 [in Coq.Reals.RIneq]
r2:189 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r2:19 [in Coq.Reals.R_Ifp]
r2:19 [in Coq.Reals.Raxioms]
r2:19 [in Coq.Reals.ClassicalConstructiveReals]
R2:190 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:191 [in Coq.Reals.RIneq]
r2:193 [in Coq.Reals.Abstract.ConstructiveReals]
r2:193 [in Coq.Reals.RIneq]
R2:194 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:195 [in Coq.Reals.RIneq]
r2:196 [in Coq.Reals.Abstract.ConstructiveReals]
r2:197 [in Coq.Reals.RIneq]
R2:198 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:199 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r2:2 [in Coq.Reals.ROrderedType]
R2:2 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:20 [in Coq.Reals.RIneq]
r2:201 [in Coq.Reals.Abstract.ConstructiveReals]
R2:201 [in Coq.Classes.CMorphisms]
r2:202 [in Coq.Reals.RIneq]
r2:202 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R2:202 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:205 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r2:207 [in Coq.Reals.Abstract.ConstructiveReals]
r2:207 [in Coq.Reals.RIneq]
R2:208 [in Coq.Classes.CMorphisms]
r2:208 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R2:208 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:209 [in Coq.Reals.RIneq]
r2:21 [in Coq.Reals.R_Ifp]
r2:21 [in Coq.Numbers.NatInt.NZDiv]
r2:211 [in Coq.Reals.Abstract.ConstructiveReals]
r2:211 [in Coq.Reals.RIneq]
r2:211 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r2:213 [in Coq.Reals.RIneq]
r2:215 [in Coq.Reals.Abstract.ConstructiveReals]
r2:215 [in Coq.Reals.RIneq]
r2:217 [in Coq.Reals.RIneq]
r2:218 [in Coq.Reals.Abstract.ConstructiveReals]
r2:22 [in Coq.Reals.RIneq]
r2:220 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r2:221 [in Coq.Reals.RIneq]
r2:223 [in Coq.Reals.RIneq]
r2:225 [in Coq.Reals.RIneq]
r2:228 [in Coq.Reals.RIneq]
r2:23 [in Coq.Reals.R_Ifp]
r2:23 [in Coq.Reals.PSeries_reg]
r2:230 [in Coq.Reals.RIneq]
r2:231 [in Coq.Reals.Abstract.ConstructiveReals]
r2:232 [in Coq.Reals.RIneq]
r2:234 [in Coq.Reals.Abstract.ConstructiveReals]
r2:234 [in Coq.Reals.RIneq]
r2:234 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r2:236 [in Coq.Reals.RIneq]
r2:237 [in Coq.Reals.Abstract.ConstructiveReals]
r2:237 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r2:238 [in Coq.Reals.RIneq]
r2:24 [in Coq.Reals.Raxioms]
r2:24 [in Coq.Reals.RIneq]
R2:24 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:240 [in Coq.Reals.Abstract.ConstructiveReals]
r2:240 [in Coq.Reals.RIneq]
R2:240 [in Coq.Reals.Abstract.ConstructiveSum]
r2:243 [in Coq.Reals.RIneq]
r2:246 [in Coq.setoid_ring.Field_theory]
R2:246 [in Coq.Reals.Abstract.ConstructiveSum]
r2:248 [in Coq.Reals.Abstract.ConstructiveReals]
r2:248 [in Coq.Reals.RIneq]
r2:25 [in Coq.Reals.R_Ifp]
R2:250 [in Coq.Reals.Abstract.ConstructiveSum]
r2:251 [in Coq.Reals.RIneq]
r2:253 [in Coq.Reals.RIneq]
r2:254 [in Coq.Reals.Abstract.ConstructiveReals]
r2:255 [in Coq.Reals.RIneq]
r2:257 [in Coq.Reals.RIneq]
r2:258 [in Coq.Reals.Abstract.ConstructiveReals]
r2:26 [in Coq.Reals.Raxioms]
r2:26 [in Coq.Reals.RIneq]
R2:26 [in Coq.Relations.Relation_Definitions]
r2:261 [in Coq.Reals.RIneq]
r2:264 [in Coq.Reals.RIneq]
r2:267 [in Coq.Reals.RIneq]
r2:268 [in Coq.Reals.Abstract.ConstructiveReals]
r2:27 [in Coq.Reals.R_Ifp]
r2:270 [in Coq.Reals.RIneq]
r2:271 [in Coq.Reals.Abstract.ConstructiveReals]
r2:273 [in Coq.Reals.RIneq]
r2:275 [in Coq.Reals.Abstract.ConstructiveReals]
r2:276 [in Coq.Reals.RIneq]
r2:279 [in Coq.Reals.Abstract.ConstructiveReals]
r2:279 [in Coq.Reals.RIneq]
r2:28 [in Coq.Reals.RIneq]
r2:281 [in Coq.Reals.RIneq]
r2:285 [in Coq.Reals.RIneq]
r2:286 [in Coq.Reals.Abstract.ConstructiveReals]
r2:289 [in Coq.Reals.RIneq]
r2:29 [in Coq.Reals.R_Ifp]
R2:29 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:290 [in Coq.Reals.Abstract.ConstructiveReals]
r2:293 [in Coq.Reals.RIneq]
r2:294 [in Coq.Reals.Abstract.ConstructiveReals]
r2:296 [in Coq.ssr.ssrbool]
r2:297 [in Coq.Reals.RIneq]
r2:298 [in Coq.Reals.Abstract.ConstructiveReals]
r2:30 [in Coq.Reals.RIneq]
R2:30 [in Coq.Relations.Relation_Definitions]
r2:301 [in Coq.Reals.RIneq]
r2:302 [in Coq.Reals.Abstract.ConstructiveReals]
r2:304 [in Coq.ssr.ssrbool]
r2:305 [in Coq.Reals.RIneq]
r2:308 [in Coq.Reals.Abstract.ConstructiveReals]
r2:309 [in Coq.Reals.RIneq]
r2:31 [in Coq.Reals.Raxioms]
r2:311 [in Coq.Reals.Abstract.ConstructiveReals]
r2:313 [in Coq.Reals.RIneq]
r2:315 [in Coq.Reals.RIneq]
r2:316 [in Coq.ssr.ssrbool]
r2:317 [in Coq.Reals.RIneq]
r2:319 [in Coq.Reals.RIneq]
r2:32 [in Coq.Reals.RIneq]
R2:32 [in Coq.Relations.Relation_Definitions]
r2:327 [in Coq.ssr.ssrbool]
r2:328 [in Coq.Reals.RIneq]
r2:33 [in Coq.Reals.PartSum]
r2:330 [in Coq.ssr.ssrbool]
r2:331 [in Coq.Reals.RIneq]
r2:334 [in Coq.Reals.RIneq]
r2:337 [in Coq.Reals.RIneq]
r2:34 [in Coq.Reals.Raxioms]
r2:34 [in Coq.Reals.RIneq]
r2:340 [in Coq.Reals.RIneq]
r2:343 [in Coq.Reals.RIneq]
r2:344 [in Coq.Reals.Abstract.ConstructiveReals]
r2:345 [in Coq.Reals.RIneq]
r2:348 [in Coq.Reals.Abstract.ConstructiveReals]
r2:348 [in Coq.Reals.RIneq]
r2:351 [in Coq.Reals.RIneq]
r2:354 [in Coq.Reals.RIneq]
r2:357 [in Coq.Reals.RIneq]
r2:359 [in Coq.Reals.RIneq]
r2:36 [in Coq.Reals.Raxioms]
r2:36 [in Coq.Reals.RIneq]
R2:36 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:360 [in Coq.MSets.MSetGenTree]
r2:361 [in Coq.Reals.RIneq]
r2:363 [in Coq.Reals.RIneq]
r2:365 [in Coq.Reals.RIneq]
r2:367 [in Coq.Reals.RIneq]
r2:369 [in Coq.Reals.RIneq]
r2:371 [in Coq.Reals.RIneq]
r2:372 [in Coq.Reals.Abstract.ConstructiveReals]
r2:376 [in Coq.Reals.Abstract.ConstructiveReals]
r2:379 [in Coq.Reals.RIneq]
r2:38 [in Coq.Reals.RIneq]
r2:380 [in Coq.Reals.Abstract.ConstructiveReals]
r2:381 [in Coq.Reals.RIneq]
r2:383 [in Coq.Reals.RIneq]
r2:384 [in Coq.Reals.Abstract.ConstructiveReals]
r2:385 [in Coq.Reals.RIneq]
r2:388 [in Coq.Reals.RIneq]
r2:391 [in Coq.Reals.RIneq]
r2:394 [in Coq.Reals.RIneq]
r2:397 [in Coq.Reals.RIneq]
r2:4 [in Coq.Reals.Rbasic_fun]
r2:4 [in Coq.Reals.ROrderedType]
r2:40 [in Coq.Reals.Raxioms]
r2:40 [in Coq.Reals.RIneq]
r2:400 [in Coq.Reals.RIneq]
r2:403 [in Coq.Reals.RIneq]
r2:406 [in Coq.Reals.RIneq]
r2:408 [in Coq.Reals.RIneq]
R2:41 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:418 [in Coq.Reals.RIneq]
r2:42 [in Coq.ZArith.Zdiv]
r2:42 [in Coq.Reals.RIneq]
r2:422 [in Coq.Reals.RIneq]
r2:426 [in Coq.Reals.RIneq]
r2:43 [in Coq.Reals.Rdefinitions]
r2:43 [in Coq.Reals.Raxioms]
r2:430 [in Coq.Reals.RIneq]
r2:432 [in Coq.Reals.RIneq]
r2:435 [in Coq.Reals.RIneq]
r2:438 [in Coq.Reals.RIneq]
r2:44 [in Coq.Reals.RIneq]
r2:441 [in Coq.Reals.RIneq]
r2:444 [in Coq.Reals.RIneq]
r2:447 [in Coq.Reals.RIneq]
r2:45 [in Coq.Reals.Rdefinitions]
r2:450 [in Coq.Reals.RIneq]
r2:453 [in Coq.Reals.RIneq]
r2:456 [in Coq.Reals.RIneq]
r2:458 [in Coq.Reals.RIneq]
r2:46 [in Coq.Reals.RIneq]
R2:46 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:460 [in Coq.Reals.RIneq]
r2:464 [in Coq.Reals.RIneq]
r2:466 [in Coq.Reals.RIneq]
r2:468 [in Coq.Reals.RIneq]
r2:47 [in Coq.Reals.Rdefinitions]
r2:47 [in Coq.ZArith.Zdiv]
r2:47 [in Coq.Reals.Rbasic_fun]
r2:470 [in Coq.Reals.RIneq]
r2:474 [in Coq.Reals.RIneq]
r2:476 [in Coq.Reals.RIneq]
r2:48 [in Coq.Reals.RIneq]
r2:482 [in Coq.Reals.RIneq]
r2:484 [in Coq.Reals.RIneq]
r2:488 [in Coq.Reals.RIneq]
r2:49 [in Coq.Reals.Rdefinitions]
R2:49 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:490 [in Coq.Reals.RIneq]
r2:494 [in Coq.Reals.RIneq]
r2:5 [in Coq.QArith.Qreduction]
r2:50 [in Coq.Reals.Rbasic_fun]
r2:50 [in Coq.Reals.RIneq]
r2:52 [in Coq.Reals.RIneq]
R2:52 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:53 [in Coq.Reals.Rbasic_fun]
r2:54 [in Coq.Reals.RIneq]
r2:54 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r2:56 [in Coq.setoid_ring.Field_theory]
r2:56 [in Coq.Reals.RIneq]
r2:574 [in Coq.Reals.RIneq]
r2:58 [in Coq.Reals.Rdefinitions]
r2:58 [in Coq.Reals.RIneq]
r2:588 [in Coq.Reals.RIneq]
r2:59 [in Coq.Reals.Abstract.ConstructiveReals]
r2:592 [in Coq.Reals.RIneq]
r2:6 [in Coq.Reals.RIneq]
r2:6 [in Coq.Reals.ROrderedType]
r2:60 [in Coq.Reals.RIneq]
r2:606 [in Coq.Reals.RIneq]
r2:62 [in Coq.Reals.RIneq]
R2:62 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:63 [in Coq.Reals.Abstract.ConstructiveReals]
r2:64 [in Coq.Reals.RIneq]
r2:66 [in Coq.Reals.RIneq]
R2:67 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:68 [in Coq.Reals.Rdefinitions]
r2:68 [in Coq.Reals.RIneq]
r2:7 [in Coq.Reals.Rbasic_fun]
r2:70 [in Coq.Reals.RIneq]
r2:71 [in Coq.FSets.FSetDecide]
r2:71 [in Coq.MSets.MSetDecide]
r2:72 [in Coq.Reals.RIneq]
r2:74 [in Coq.Reals.RIneq]
r2:75 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r2:76 [in Coq.Reals.RIneq]
R2:76 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:78 [in Coq.Reals.RIneq]
r2:78 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r2:8 [in Coq.Reals.RIneq]
r2:80 [in Coq.Reals.RIneq]
R2:83 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:84 [in Coq.Reals.RIneq]
r2:88 [in Coq.Reals.RIneq]
R2:88 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:89 [in Coq.Reals.RiemannInt_SF]
r2:9 [in Coq.Numbers.Natural.Abstract.NDiv]
r2:9 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
r2:91 [in Coq.Reals.RIneq]
R2:93 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r2:94 [in Coq.Reals.RIneq]
r2:97 [in Coq.Reals.RIneq]
R2:98 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r3:101 [in Coq.Reals.RIneq]
r3:104 [in Coq.Reals.RIneq]
r3:107 [in Coq.Reals.RIneq]
r3:115 [in Coq.Reals.RiemannInt_SF]
r3:119 [in Coq.Reals.Abstract.ConstructiveReals]
r3:123 [in Coq.Reals.Abstract.ConstructiveReals]
r3:133 [in Coq.Reals.RiemannInt_SF]
r3:136 [in Coq.Reals.RIneq]
r3:151 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r3:155 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r3:181 [in Coq.Reals.Abstract.ConstructiveReals]
R3:181 [in Coq.Classes.Morphisms]
r3:197 [in Coq.Reals.Abstract.ConstructiveReals]
r3:198 [in Coq.Reals.RIneq]
r3:20 [in Coq.Reals.Raxioms]
r3:202 [in Coq.Reals.Abstract.ConstructiveReals]
R3:211 [in Coq.Classes.CMorphisms]
r3:241 [in Coq.Reals.RIneq]
r3:244 [in Coq.Reals.RIneq]
r3:25 [in Coq.Reals.PSeries_reg]
r3:255 [in Coq.Reals.Abstract.ConstructiveReals]
r3:258 [in Coq.Reals.RIneq]
r3:259 [in Coq.Reals.Abstract.ConstructiveReals]
r3:27 [in Coq.Reals.Raxioms]
r3:282 [in Coq.Reals.RIneq]
r3:286 [in Coq.Reals.RIneq]
r3:290 [in Coq.Reals.RIneq]
r3:294 [in Coq.Reals.RIneq]
r3:298 [in Coq.Reals.RIneq]
R3:30 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r3:302 [in Coq.Reals.RIneq]
r3:306 [in Coq.Reals.RIneq]
r3:310 [in Coq.Reals.RIneq]
r3:32 [in Coq.Reals.Raxioms]
r3:346 [in Coq.Reals.RIneq]
r3:349 [in Coq.Reals.RIneq]
r3:352 [in Coq.Reals.RIneq]
r3:355 [in Coq.Reals.RIneq]
r3:37 [in Coq.Reals.Raxioms]
r3:409 [in Coq.Reals.RIneq]
r3:419 [in Coq.Reals.RIneq]
r3:423 [in Coq.Reals.RIneq]
r3:427 [in Coq.Reals.RIneq]
r3:55 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r3:589 [in Coq.Reals.RIneq]
r3:76 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r3:81 [in Coq.Reals.RIneq]
r3:85 [in Coq.Reals.RIneq]
r3:89 [in Coq.Reals.RIneq]
r3:90 [in Coq.Reals.RiemannInt_SF]
r3:92 [in Coq.Reals.RIneq]
r3:95 [in Coq.Reals.RIneq]
r3:98 [in Coq.Reals.RIneq]
r4:118 [in Coq.Reals.RiemannInt_SF]
r4:136 [in Coq.Reals.RiemannInt_SF]
r4:137 [in Coq.Reals.RIneq]
r4:152 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r4:156 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r4:182 [in Coq.Reals.Abstract.ConstructiveReals]
r4:198 [in Coq.Reals.Abstract.ConstructiveReals]
r4:203 [in Coq.Reals.Abstract.ConstructiveReals]
r4:283 [in Coq.Reals.RIneq]
r4:287 [in Coq.Reals.RIneq]
r4:291 [in Coq.Reals.RIneq]
r4:295 [in Coq.Reals.RIneq]
r4:299 [in Coq.Reals.RIneq]
r4:303 [in Coq.Reals.RIneq]
r4:307 [in Coq.Reals.RIneq]
r4:311 [in Coq.Reals.RIneq]
r4:410 [in Coq.Reals.RIneq]
r4:420 [in Coq.Reals.RIneq]
r4:424 [in Coq.Reals.RIneq]
r4:428 [in Coq.Reals.RIneq]
r4:590 [in Coq.Reals.RIneq]
r4:82 [in Coq.Reals.RIneq]
r4:86 [in Coq.Reals.RIneq]
R:1 [in Coq.setoid_ring.Ncring_initial]
r:1 [in Coq.Reals.R_Ifp]
R:1 [in Coq.nsatz.NsatzTactic]
R:1 [in Coq.Reals.Abstract.ConstructivePower]
R:1 [in Coq.setoid_ring.Ncring_tac]
R:1 [in Coq.setoid_ring.Integral_domain]
R:1 [in Coq.setoid_ring.Cring]
R:1 [in Coq.Reals.Abstract.ConstructiveAbs]
R:1 [in Coq.Reals.Abstract.ConstructiveLimits]
r:1 [in Coq.ZArith.ZArith_dec]
r:1 [in Coq.Reals.Rpow_def]
r:1 [in Coq.Reals.RIneq]
R:1 [in Coq.Reals.Abstract.ConstructiveSum]
R:1 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:10 [in Coq.Program.Wf]
R:10 [in Coq.Reals.Abstract.ConstructiveLUB]
R:10 [in Coq.Classes.RelationClasses]
R:10 [in Coq.Logic.ChoiceFacts]
r:10 [in Coq.Numbers.NatInt.NZLog]
R:10 [in Coq.Reals.Abstract.ConstructiveAbs]
R:10 [in Coq.Reals.Abstract.ConstructiveLimits]
R:10 [in Coq.Sets.Relations_2_facts]
R:10 [in Coq.Sets.Relations_3_facts]
r:10 [in Coq.Reals.ClassicalDedekindReals]
r:100 [in Coq.Reals.Abstract.ConstructiveLUB]
R:100 [in Coq.Classes.Morphisms]
R:100 [in Coq.Classes.CRelationClasses]
R:100 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:101 [in Coq.FSets.FSetDecide]
R:101 [in Coq.Classes.RelationClasses]
R:101 [in Coq.Logic.ChoiceFacts]
r:101 [in Coq.MSets.MSetDecide]
R:101 [in Coq.Classes.CMorphisms]
R:101 [in Coq.Reals.Abstract.ConstructiveSum]
r:102 [in Coq.Reals.Abstract.ConstructiveLUB]
R:102 [in Coq.Reals.Abstract.ConstructiveLimits]
R:102 [in Coq.Classes.CRelationClasses]
R:103 [in Coq.Classes.RelationClasses]
R:103 [in Coq.Classes.Morphisms]
r:1031 [in Coq.FSets.FMapAVL]
r:1035 [in Coq.FSets.FMapAVL]
r:104 [in Coq.Reals.Abstract.ConstructiveLUB]
R:104 [in Coq.Classes.CRelationClasses]
r:104 [in Coq.Reals.Rbasic_fun]
R:104 [in Coq.Reals.Abstract.ConstructiveSum]
R:104 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:1040 [in Coq.FSets.FMapAVL]
r:1044 [in Coq.FSets.FMapAVL]
r:1049 [in Coq.FSets.FMapAVL]
r:105 [in Coq.ZArith.BinIntDef]
R:105 [in Coq.Reals.Abstract.ConstructiveLUB]
R:105 [in Coq.Classes.CMorphisms]
r:1055 [in Coq.FSets.FMapAVL]
R:106 [in Coq.Classes.Morphisms]
R:106 [in Coq.Classes.CRelationClasses]
R:107 [in Coq.setoid_ring.Ncring_tac]
r:107 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
r:107 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:108 [in Coq.ZArith.BinIntDef]
R:108 [in Coq.Classes.Morphisms]
R:108 [in Coq.Logic.ChoiceFacts]
R:108 [in Coq.Reals.Abstract.ConstructiveLimits]
R:108 [in Coq.Classes.CRelationClasses]
R:108 [in Coq.Reals.Abstract.ConstructiveSum]
R:108 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:1085 [in Coq.FSets.FMapAVL]
R:109 [in Coq.Classes.CMorphisms]
r:109 [in Coq.Init.Datatypes]
r:1091 [in Coq.FSets.FMapAVL]
r:1098 [in Coq.FSets.FMapAVL]
r:11 [in Coq.Arith.Compare]
r:11 [in Coq.Reals.R_Ifp]
r:11 [in Coq.NArith.BinNat]
r:11 [in Coq.ZArith.Zdiv]
R:11 [in Coq.Classes.CMorphisms]
r:11 [in Coq.Reals.Rbasic_fun]
r:11 [in Coq.micromega.ZifyComparison]
r:11 [in Coq.Numbers.NatInt.NZSqrt]
r:11 [in Coq.micromega.RMicromega]
R:11 [in Coq.Logic.Diaconescu]
R:11 [in Coq.Reals.Abstract.ConstructiveSum]
R:11 [in Coq.Sets.Relations_1]
R:110 [in Coq.Reals.Abstract.ConstructiveReals]
r:110 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
r:110 [in Coq.ZArith.BinIntDef]
R:110 [in Coq.Classes.Morphisms]
R:110 [in Coq.Classes.CRelationClasses]
r:1103 [in Coq.FSets.FMapAVL]
r:1108 [in Coq.FSets.FMapAVL]
r:111 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:111 [in Coq.Lists.SetoidList]
r:112 [in Coq.Classes.RelationClasses]
R:112 [in Coq.Classes.CRelationClasses]
R:112 [in Coq.Reals.Abstract.ConstructiveSum]
R:113 [in Coq.Reals.Abstract.ConstructiveReals]
R:113 [in Coq.Reals.Abstract.ConstructiveLUB]
R:113 [in Coq.Classes.CMorphisms]
r:113 [in Coq.Reals.RList]
r:113 [in Coq.Reals.RiemannInt_SF]
R:114 [in Coq.Reals.Abstract.ConstructiveReals]
r:114 [in Coq.FSets.FSetDecide]
R:114 [in Coq.Logic.ChoiceFacts]
r:114 [in Coq.MSets.MSetDecide]
r:114 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
r:1141 [in Coq.FSets.FMapAVL]
r:1146 [in Coq.FSets.FMapAVL]
r:115 [in Coq.Init.Nat]
r:115 [in Coq.ZArith.Zdiv]
r:1150 [in Coq.FSets.FMapAVL]
R:116 [in Coq.Reals.Abstract.ConstructiveReals]
r:116 [in Coq.ZArith.BinInt]
R:116 [in Coq.Reals.Abstract.ConstructiveLimits]
r:116 [in Coq.Reals.RList]
r:116 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r:117 [in Coq.ZArith.BinIntDef]
R:117 [in Coq.Classes.Morphisms]
R:117 [in Coq.Classes.CMorphisms]
r:117 [in Coq.Numbers.Cyclic.Int31.Int31]
r:117 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R:118 [in Coq.Reals.Abstract.ConstructiveLUB]
R:118 [in Coq.setoid_ring.Ncring]
R:119 [in Coq.Logic.ChoiceFacts]
R:119 [in Coq.Classes.CRelationClasses]
r:119 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
r:119 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
R:12 [in Coq.Classes.Morphisms]
R:12 [in Coq.Reals.Abstract.ConstructivePower]
R:12 [in Coq.Logic.ClassicalChoice]
R:12 [in Coq.Reals.Abstract.ConstructiveAbs]
R:12 [in Coq.Logic.IndefiniteDescription]
r:12 [in Coq.micromega.QMicromega]
R:12 [in Coq.Sets.Relations_1_facts]
R:12 [in Coq.Sets.Relations_2_facts]
r:12 [in Coq.micromega.RMicromega]
r:12 [in Coq.Arith.Euclid]
R:12 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:120 [in Coq.Reals.Abstract.ConstructiveReals]
R:120 [in Coq.Classes.CMorphisms]
R:120 [in Coq.Reals.Abstract.ConstructiveLimits]
R:120 [in Coq.Reals.Abstract.ConstructiveSum]
R:122 [in Coq.Reals.Abstract.ConstructiveLUB]
R:122 [in Coq.setoid_ring.Ncring_tac]
r:122 [in Coq.Reals.Rbasic_fun]
r:122 [in Coq.Reals.PSeries_reg]
r:123 [in Coq.ZArith.BinIntDef]
R:123 [in Coq.Classes.Morphisms]
r:123 [in Coq.Init.Nat]
R:123 [in Coq.Classes.CMorphisms]
R:123 [in Coq.Classes.CRelationClasses]
r:123 [in Coq.MSets.MSetGenTree]
r:1233 [in Coq.FSets.FMapAVL]
R:124 [in Coq.Program.Wf]
R:124 [in Coq.Reals.Abstract.ConstructiveReals]
R:124 [in Coq.Logic.ChoiceFacts]
r:124 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
r:125 [in Coq.ZArith.BinIntDef]
R:125 [in Coq.Reals.Abstract.ConstructiveLimits]
R:125 [in Coq.Reals.Abstract.ConstructiveSum]
R:126 [in Coq.Classes.Morphisms]
r:126 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r:126 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r:127 [in Coq.ZArith.BinIntDef]
R:127 [in Coq.Classes.CRelationClasses]
r:127 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
R:128 [in Coq.Reals.Abstract.ConstructiveReals]
R:128 [in Coq.Classes.Morphisms]
r:129 [in Coq.ZArith.BinIntDef]
r:13 [in Coq.Reals.R_Ifp]
r:13 [in Coq.Numbers.Natural.Abstract.NDiv]
R:13 [in Coq.Classes.RelationClasses]
r:13 [in Coq.FSets.FMapFullAVL]
r:13 [in Coq.ZArith.Zdiv]
R:13 [in Coq.Logic.ClassicalUniqueChoice]
R:13 [in Coq.Classes.CRelationClasses]
r:13 [in Coq.Reals.PSeries_reg]
r:13 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
r:13 [in Coq.Reals.ClassicalConstructiveReals]
r:130 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
r:130 [in Coq.Floats.SpecFloat]
R:130 [in Coq.Reals.Abstract.ConstructiveLimits]
R:131 [in Coq.Classes.Morphisms]
r:131 [in Coq.Reals.RiemannInt_SF]
R:131 [in Coq.Reals.Abstract.ConstructiveSum]
R:132 [in Coq.Reals.Abstract.ConstructiveReals]
r:132 [in Coq.setoid_ring.Ring_polynom]
R:133 [in Coq.setoid_ring.Ring_polynom]
R:133 [in Coq.Classes.Morphisms]
R:133 [in Coq.Classes.CRelationClasses]
r:133 [in Coq.ZArith.Znumtheory]
r:134 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
R:134 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r:135 [in Coq.ZArith.BinInt]
R:135 [in Coq.Reals.Abstract.ConstructiveSum]
R:136 [in Coq.Reals.Abstract.ConstructiveReals]
R:136 [in Coq.micromega.ZifyClasses]
R:136 [in Coq.Classes.Morphisms]
R:137 [in Coq.Classes.RelationClasses]
R:138 [in Coq.Reals.Abstract.ConstructiveReals]
r:138 [in Coq.Reals.RIneq]
R:138 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
R:139 [in Coq.Classes.RelationClasses]
r:139 [in Coq.ZArith.BinInt]
R:139 [in Coq.Classes.CMorphisms]
R:139 [in Coq.Classes.CRelationClasses]
r:139 [in Coq.Reals.RIneq]
R:139 [in Coq.setoid_ring.Ncring]
R:14 [in Coq.Reals.Abstract.ConstructiveLUB]
r:14 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
R:14 [in Coq.Logic.SetoidChoice]
r:14 [in Coq.Reals.Rbasic_fun]
r:14 [in Coq.Logic.HLevels]
R:14 [in Coq.Sets.Relations_3_facts]
r:14 [in Coq.Reals.ClassicalDedekindReals]
r:14 [in Coq.Reals.ClassicalConstructiveReals]
R:140 [in Coq.micromega.EnvRing]
r:140 [in Coq.Reals.RIneq]
R:141 [in Coq.Reals.Abstract.ConstructiveReals]
r:141 [in Coq.PArith.BinPos]
R:141 [in Coq.Reals.Abstract.ConstructiveSum]
r:142 [in Coq.Reals.Rfunctions]
R:142 [in Coq.micromega.EnvRing]
r:142 [in Coq.setoid_ring.Ncring_polynom]
r:143 [in Coq.Reals.RIneq]
r:144 [in Coq.PArith.BinPos]
r:144 [in Coq.MSets.MSetPositive]
R:144 [in Coq.Classes.CRelationClasses]
R:145 [in Coq.Reals.Abstract.ConstructiveReals]
R:145 [in Coq.setoid_ring.Ring_polynom]
R:145 [in Coq.Arith.Wf_nat]
R:145 [in Coq.setoid_ring.Ncring_tac]
R:146 [in Coq.Reals.Abstract.ConstructiveReals]
R:146 [in Coq.Classes.RelationClasses]
r:146 [in Coq.Reals.RIneq]
r:146 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
R:146 [in Coq.Reals.Abstract.ConstructiveSum]
R:147 [in Coq.Reals.Abstract.ConstructiveReals]
r:147 [in Coq.PArith.BinPos]
R:147 [in Coq.setoid_ring.Ring_polynom]
R:148 [in Coq.Reals.Abstract.ConstructiveReals]
R:148 [in Coq.Classes.RelationClasses]
r:148 [in Coq.FSets.FMapPositive]
R:149 [in Coq.Reals.Abstract.ConstructiveReals]
R:15 [in Coq.Reals.Abstract.ConstructivePower]
R:15 [in Coq.Logic.ChoiceFacts]
R:15 [in Coq.Reals.Abstract.ConstructiveAbs]
R:15 [in Coq.Classes.CMorphisms]
R:15 [in Coq.Reals.Abstract.ConstructiveSum]
r:15 [in Coq.Arith.Euclid]
r:15 [in Coq.micromega.Refl]
R:15 [in Coq.Sets.Relations_1]
R:15 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:150 [in Coq.Reals.Abstract.ConstructiveReals]
R:151 [in Coq.Reals.Abstract.ConstructiveReals]
R:151 [in Coq.Classes.CMorphisms]
r:151 [in Coq.Reals.RIneq]
R:152 [in Coq.Reals.Abstract.ConstructiveReals]
r:152 [in Coq.MSets.MSetGenTree]
R:152 [in Coq.setoid_ring.Ncring]
R:153 [in Coq.Reals.Abstract.ConstructiveReals]
R:153 [in Coq.Lists.SetoidList]
r:154 [in Coq.PArith.BinPos]
r:154 [in Coq.Reals.RIneq]
R:154 [in Coq.Reals.Abstract.ConstructiveSum]
R:155 [in Coq.Reals.Abstract.ConstructiveReals]
R:155 [in Coq.Classes.CMorphisms]
r:156 [in Coq.Numbers.Cyclic.Int63.Int63]
r:156 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R:157 [in Coq.Reals.Abstract.ConstructiveReals]
r:157 [in Coq.ZArith.BinInt]
r:157 [in Coq.Numbers.Cyclic.Int31.Int31]
r:157 [in Coq.Reals.RIneq]
R:158 [in Coq.Classes.Morphisms]
R:158 [in Coq.Classes.CMorphisms]
r:158 [in Coq.FSets.FSetPositive]
R:159 [in Coq.Reals.Abstract.ConstructiveReals]
r:159 [in Coq.PArith.BinPos]
r:159 [in Coq.Reals.Rfunctions]
r:159 [in Coq.NArith.BinNat]
r:159 [in Coq.Numbers.Cyclic.Int31.Int31]
r:159 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
r:16 [in Coq.Logic.EqdepFacts]
r:16 [in Coq.ZArith.Zpow_facts]
r:16 [in Coq.Reals.Rseries]
R:16 [in Coq.Classes.Morphisms]
R:16 [in Coq.Reals.Abstract.ConstructiveLimits]
R:160 [in Coq.setoid_ring.Ncring_tac]
r:160 [in Coq.FSets.FMapAVL]
r:160 [in Coq.MSets.MSetGenTree]
R:161 [in Coq.Reals.Abstract.ConstructiveReals]
R:161 [in Coq.Classes.Morphisms]
R:161 [in Coq.Reals.Abstract.ConstructiveSum]
r:162 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
R:162 [in Coq.Reals.Abstract.ConstructiveReals]
r:162 [in Coq.PArith.BinPos]
R:162 [in Coq.Classes.RelationClasses]
R:162 [in Coq.Classes.CMorphisms]
r:163 [in Coq.Reals.Abstract.ConstructiveReals]
r:163 [in Coq.NArith.BinNat]
r:163 [in Coq.Reals.RIneq]
r:164 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
R:164 [in Coq.Classes.RelationClasses]
r:164 [in Coq.Reals.Rpower]
r:164 [in Coq.FSets.FMapAVL]
r:164 [in Coq.Reals.RIneq]
r:165 [in Coq.PArith.BinPos]
r:165 [in Coq.Reals.Rpower]
R:165 [in Coq.Classes.CMorphisms]
r:165 [in Coq.MSets.MSetGenTree]
R:165 [in Coq.setoid_ring.Ncring_polynom]
r:165 [in Coq.Reals.RIneq]
r:165 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r:165 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R:166 [in Coq.Reals.Abstract.ConstructiveReals]
r:166 [in Coq.Reals.RIneq]
r:167 [in Coq.Reals.Abstract.ConstructiveReals]
r:167 [in Coq.Reals.RIneq]
r:168 [in Coq.PArith.BinPos]
R:168 [in Coq.Classes.RelationClasses]
r:168 [in Coq.Reals.RIneq]
r:169 [in Coq.FSets.FMapAVL]
R:169 [in Coq.Classes.CMorphisms]
r:169 [in Coq.Reals.RIneq]
R:169 [in Coq.Reals.Abstract.ConstructiveSum]
r:17 [in Coq.Numbers.Natural.Abstract.NDiv]
R:17 [in Coq.setoid_ring.Integral_domain]
R:17 [in Coq.setoid_ring.Cring]
R:17 [in Coq.Classes.CEquivalence]
r:17 [in Coq.MSets.MSetRBT]
R:17 [in Coq.Classes.CRelationClasses]
R:17 [in Coq.Sets.Relations_2_facts]
r:17 [in Coq.Reals.Rbasic_fun]
r:17 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
R:17 [in Coq.Sets.Relations_3_facts]
R:17 [in Coq.Reals.Abstract.ConstructiveSum]
R:17 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:17 [in Coq.Reals.ClassicalConstructiveReals]
R:17 [in Coq.Classes.Equivalence]
R:170 [in Coq.Reals.Abstract.ConstructiveReals]
r:170 [in Coq.Reals.RIneq]
r:170 [in Coq.ZArith.Znumtheory]
r:171 [in Coq.Reals.Abstract.ConstructiveReals]
r:172 [in Coq.micromega.ZMicromega]
R:173 [in Coq.setoid_ring.Ncring_tac]
r:173 [in Coq.Reals.RIneq]
R:174 [in Coq.Reals.Abstract.ConstructiveReals]
R:174 [in Coq.Classes.RelationClasses]
r:174 [in Coq.Vectors.VectorDef]
r:175 [in Coq.Reals.Abstract.ConstructiveReals]
r:176 [in Coq.Reals.RIneq]
r:176 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r:177 [in Coq.NArith.BinNat]
r:177 [in Coq.FSets.FMapAVL]
R:177 [in Coq.Reals.Abstract.ConstructiveSum]
R:178 [in Coq.Reals.Abstract.ConstructiveReals]
R:178 [in Coq.setoid_ring.Ncring_polynom]
r:178 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
R:179 [in Coq.Classes.RelationClasses]
r:179 [in Coq.Reals.RIneq]
R:18 [in Coq.Classes.RelationClasses]
r:18 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
r:18 [in Coq.FSets.FMapFullAVL]
r:18 [in Coq.ZArith.Zdiv]
R:18 [in Coq.Reals.Abstract.ConstructiveAbs]
R:18 [in Coq.Sets.Relations_1_facts]
r:181 [in Coq.setoid_ring.Ring_theory]
r:181 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
R:181 [in Coq.Reals.Abstract.ConstructiveSum]
r:182 [in Coq.FSets.FMapAVL]
R:183 [in Coq.Reals.Abstract.ConstructiveReals]
r:183 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r:183 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R:185 [in Coq.Classes.Morphisms]
r:185 [in Coq.Arith.PeanoNat]
r:185 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
r:185 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R:186 [in Coq.Reals.Abstract.ConstructiveReals]
R:186 [in Coq.Reals.Abstract.ConstructiveSum]
r:187 [in Coq.Reals.Abstract.ConstructiveReals]
r:187 [in Coq.FSets.FMapAVL]
r:187 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
R:188 [in Coq.Classes.CMorphisms]
R:189 [in Coq.setoid_ring.Ncring]
R:19 [in Coq.Reals.Abstract.ConstructivePower]
r:19 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
R:19 [in Coq.Sets.Relations_2_facts]
r:19 [in Coq.Reals.PSeries_reg]
r:19 [in Coq.ZArith.Zcompare]
R:190 [in Coq.Reals.Abstract.ConstructiveReals]
R:190 [in Coq.Classes.Morphisms]
R:190 [in Coq.Classes.CMorphisms]
r:191 [in Coq.Reals.Abstract.ConstructiveReals]
r:191 [in Coq.ZArith.BinInt]
r:193 [in Coq.setoid_ring.Ring_theory]
R:194 [in Coq.Reals.Abstract.ConstructiveReals]
r:194 [in Coq.ZArith.BinInt]
r:194 [in Coq.Reals.RiemannInt_SF]
R:196 [in Coq.setoid_ring.Ncring_tac]
r:196 [in Coq.Reals.RiemannInt_SF]
r:197 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r:198 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
R:198 [in Coq.Reals.Abstract.ConstructiveSum]
R:199 [in Coq.Reals.Abstract.ConstructiveReals]
r:199 [in Coq.Reals.RIneq]
r:2 [in Coq.Reals.R_Ifp]
R:2 [in Coq.Classes.RelationClasses]
r:2 [in Coq.Reals.Abstract.ConstructivePower]
R:2 [in Coq.Classes.SetoidTactics]
R:2 [in Coq.ssr.ssrclasses]
R:2 [in Coq.Classes.CEquivalence]
R:2 [in Coq.Reals.Abstract.ConstructiveAbs]
R:2 [in Coq.Classes.CMorphisms]
R:2 [in Coq.Sets.Relations_1_facts]
R:2 [in Coq.Sets.Relations_2_facts]
R:2 [in Coq.ssr.ssrsetoid]
R:2 [in Coq.setoid_ring.Ncring_polynom]
r:2 [in Coq.Reals.PSeries_reg]
r:2 [in Coq.Reals.RIneq]
R:2 [in Coq.Sets.Relations_3_facts]
R:2 [in Coq.Classes.Equivalence]
r:20 [in Coq.FSets.FSetPositive]
r:20 [in Coq.MSets.MSetPositive]
R:20 [in Coq.Classes.CRelationClasses]
R:20 [in Coq.Reals.Abstract.ConstructiveSum]
r:20 [in Coq.Reals.Rlogic]
R:20 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:20 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
R:200 [in Coq.Classes.Morphisms]
r:200 [in Coq.Reals.RIneq]
r:200 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r:201 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
r:203 [in Coq.Reals.RIneq]
r:203 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R:204 [in Coq.Reals.Abstract.ConstructiveReals]
r:204 [in Coq.Reals.RIneq]
r:205 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
r:205 [in Coq.Reals.Abstract.ConstructiveReals]
r:205 [in Coq.FSets.FMapAVL]
r:205 [in Coq.Reals.RIneq]
R:206 [in Coq.Classes.Morphisms]
r:206 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r:207 [in Coq.Init.Specif]
R:208 [in Coq.Reals.Abstract.ConstructiveReals]
r:209 [in Coq.Reals.Abstract.ConstructiveReals]
r:209 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r:21 [in Coq.Lists.List]
R:21 [in Coq.Reals.Abstract.ConstructivePower]
R:21 [in Coq.Classes.RelationPairs]
r:21 [in Coq.Numbers.Cyclic.Int63.Int63]
R:21 [in Coq.setoid_ring.Ncring_tac]
R:21 [in Coq.Reals.Abstract.ConstructiveAbs]
R:21 [in Coq.funind.Recdef]
R:21 [in Coq.Classes.CMorphisms]
r:21 [in Coq.Reals.Raxioms]
r:21 [in Coq.MSets.MSetRBT]
R:21 [in Coq.Sets.Relations_1_facts]
R:21 [in Coq.Classes.CRelationClasses]
R:21 [in Coq.Sets.Relations_2_facts]
r:21 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
r:21 [in Coq.micromega.RMicromega]
r:21 [in Coq.Reals.ClassicalConstructiveReals]
R:210 [in Coq.setoid_ring.Ncring_tac]
R:212 [in Coq.Reals.Abstract.ConstructiveReals]
R:212 [in Coq.Classes.Morphisms]
r:213 [in Coq.Reals.Abstract.ConstructiveReals]
R:213 [in Coq.Reals.Abstract.ConstructiveSum]
r:214 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R:215 [in Coq.Classes.CMorphisms]
R:216 [in Coq.Reals.Abstract.ConstructiveReals]
r:216 [in Coq.Reals.RiemannInt_SF]
R:218 [in Coq.Classes.Morphisms]
r:218 [in Coq.Reals.RIneq]
r:218 [in Coq.Reals.RiemannInt_SF]
r:218 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R:219 [in Coq.Reals.Abstract.ConstructiveReals]
r:219 [in Coq.Reals.RIneq]
R:22 [in Coq.Classes.Morphisms]
r:22 [in Coq.FSets.FMapFullAVL]
r:22 [in Coq.Reals.Raxioms]
R:22 [in Coq.Logic.ClassicalDescription]
r:22 [in Coq.micromega.RMicromega]
r:22 [in Coq.Reals.Rlogic]
R:220 [in Coq.Reals.Abstract.ConstructiveReals]
R:220 [in Coq.Classes.CMorphisms]
R:221 [in Coq.Reals.Abstract.ConstructiveReals]
R:222 [in Coq.Reals.Abstract.ConstructiveReals]
R:222 [in Coq.Reals.Abstract.ConstructiveSum]
R:223 [in Coq.Reals.Abstract.ConstructiveReals]
R:224 [in Coq.Reals.Abstract.ConstructiveReals]
R:224 [in Coq.setoid_ring.Ncring_tac]
R:225 [in Coq.Reals.Abstract.ConstructiveReals]
r:225 [in Coq.PArith.BinPos]
R:225 [in Coq.Classes.CMorphisms]
R:226 [in Coq.Reals.Abstract.ConstructiveReals]
r:226 [in Coq.PArith.BinPos]
R:227 [in Coq.Reals.Abstract.ConstructiveReals]
r:227 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r:228 [in Coq.Reals.Abstract.ConstructiveReals]
R:229 [in Coq.Reals.Abstract.ConstructiveReals]
R:23 [in Coq.Classes.RelationClasses]
R:23 [in Coq.Logic.ChoiceFacts]
r:23 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
r:23 [in Coq.FSets.FMapAVL]
r:23 [in Coq.Reals.Abstract.ConstructiveLimits]
r:23 [in Coq.Numbers.HexadecimalQ]
r:23 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:23 [in Coq.Reals.ClassicalConstructiveReals]
r:231 [in Coq.MSets.MSetRBT]
R:231 [in Coq.Reals.Abstract.ConstructiveSum]
R:232 [in Coq.Reals.Abstract.ConstructiveReals]
r:232 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R:233 [in Coq.Classes.CMorphisms]
r:234 [in Coq.PArith.BinPos]
r:234 [in Coq.ZArith.Zdiv]
R:235 [in Coq.Reals.Abstract.ConstructiveReals]
R:235 [in Coq.setoid_ring.Ncring_tac]
r:235 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r:236 [in Coq.ZArith.Zdiv]
R:238 [in Coq.Reals.Abstract.ConstructiveReals]
r:239 [in Coq.PArith.BinPos]
r:24 [in Coq.Program.Wf]
r:24 [in Coq.Numbers.Cyclic.Int63.Int63]
r:24 [in Coq.MSets.MSetAVL]
R:24 [in Coq.Classes.CEquivalence]
R:24 [in Coq.Reals.Abstract.ConstructiveAbs]
R:24 [in Coq.Sets.Relations_1_facts]
R:24 [in Coq.Classes.CRelationClasses]
R:24 [in Coq.Sets.Relations_2_facts]
R:24 [in Coq.Reals.Abstract.ConstructiveSum]
r:24 [in Coq.Reals.Rlogic]
R:24 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:24 [in Coq.Classes.Equivalence]
r:240 [in Coq.MSets.MSetRBT]
R:241 [in Coq.Reals.Abstract.ConstructiveReals]
r:241 [in Coq.MSets.MSetRBT]
r:242 [in Coq.Reals.Abstract.ConstructiveReals]
r:242 [in Coq.ZArith.Zdiv]
r:243 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
R:243 [in Coq.Reals.Abstract.ConstructiveReals]
r:243 [in Coq.FSets.FSetInterface]
R:243 [in Coq.Classes.CMorphisms]
r:244 [in Coq.PArith.BinPos]
R:245 [in Coq.Reals.Abstract.ConstructiveReals]
r:245 [in Coq.ZArith.Zdiv]
r:245 [in Coq.Reals.RIneq]
r:246 [in Coq.Reals.Abstract.ConstructiveReals]
r:246 [in Coq.Reals.RIneq]
r:247 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
R:249 [in Coq.Reals.Abstract.ConstructiveReals]
r:249 [in Coq.FSets.FSetInterface]
R:249 [in Coq.Classes.CMorphisms]
r:249 [in Coq.MSets.MSetRBT]
r:249 [in Coq.Reals.RIneq]
R:25 [in Coq.Reals.Abstract.ConstructivePower]
r:25 [in Coq.Reals.Abstract.ConstructiveLimits]
r:25 [in Coq.MSets.MSetRBT]
r:25 [in Coq.Numbers.HexadecimalQ]
r:25 [in Coq.Numbers.NatInt.NZDiv]
r:25 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
r:25 [in Coq.micromega.RMicromega]
r:250 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
r:250 [in Coq.Reals.Abstract.ConstructiveReals]
R:250 [in Coq.setoid_ring.Ncring_tac]
r:250 [in Coq.MSets.MSetRBT]
R:252 [in Coq.Reals.Abstract.ConstructiveReals]
R:253 [in Coq.Logic.EqdepFacts]
R:254 [in Coq.Logic.ChoiceFacts]
r:255 [in Coq.ZArith.Zdiv]
R:255 [in Coq.Classes.CMorphisms]
R:256 [in Coq.Reals.Abstract.ConstructiveReals]
r:256 [in Coq.Numbers.Cyclic.Int63.Int63]
R:257 [in Coq.Logic.ClassicalFacts]
r:258 [in Coq.MSets.MSetRBT]
r:259 [in Coq.Reals.RIneq]
r:26 [in Coq.FSets.FMapFullAVL]
r:26 [in Coq.QArith.Qabs]
R:26 [in Coq.Reals.Abstract.ConstructiveAbs]
R:26 [in Coq.Reals.Abstract.ConstructiveLimits]
r:26 [in Coq.micromega.ZMicromega]
R:260 [in Coq.Reals.Abstract.ConstructiveReals]
R:261 [in Coq.Classes.CMorphisms]
R:262 [in Coq.Reals.Abstract.ConstructiveReals]
r:262 [in Coq.Reals.RIneq]
R:264 [in Coq.Reals.Abstract.ConstructiveReals]
r:265 [in Coq.Reals.Abstract.ConstructiveReals]
r:265 [in Coq.Reals.RIneq]
R:266 [in Coq.Reals.Abstract.ConstructiveReals]
r:266 [in Coq.MSets.MSetRBT]
r:267 [in Coq.MSets.MSetRBT]
R:268 [in Coq.Logic.EqdepFacts]
R:268 [in Coq.setoid_ring.Ncring_tac]
r:268 [in Coq.Reals.RIneq]
R:269 [in Coq.Reals.Abstract.ConstructiveReals]
r:27 [in Coq.QArith.Qcabs]
r:27 [in Coq.FSets.FMapAVL]
R:27 [in Coq.Sets.Relations_1_facts]
R:27 [in Coq.Sets.Relations_2_facts]
r:27 [in Coq.Numbers.HexadecimalQ]
R:27 [in Coq.Logic.Classical_Prop]
r:271 [in Coq.Reals.RIneq]
R:272 [in Coq.Reals.Abstract.ConstructiveReals]
r:273 [in Coq.Reals.Abstract.ConstructiveReals]
r:274 [in Coq.MSets.MSetRBT]
r:274 [in Coq.Reals.RIneq]
R:276 [in Coq.Reals.Abstract.ConstructiveReals]
r:277 [in Coq.Reals.Abstract.ConstructiveReals]
R:277 [in Coq.setoid_ring.Ring_polynom]
r:277 [in Coq.Reals.RIneq]
r:278 [in Coq.MSets.MSetRBT]
r:279 [in Coq.Reals.Ratan]
r:28 [in Coq.Program.Wf]
R:28 [in Coq.Reals.Abstract.ConstructiveAbs]
r:28 [in Coq.Reals.Raxioms]
r:28 [in Coq.Logic.Berardi]
R:28 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:280 [in Coq.Reals.Abstract.ConstructiveReals]
r:281 [in Coq.Reals.Abstract.ConstructiveReals]
R:282 [in Coq.setoid_ring.Ring_theory]
R:283 [in Coq.Reals.Abstract.ConstructiveReals]
r:284 [in Coq.Reals.Abstract.ConstructiveReals]
R:284 [in Coq.setoid_ring.Ring_polynom]
r:285 [in Coq.MSets.MSetRBT]
R:287 [in Coq.Reals.Abstract.ConstructiveReals]
R:287 [in Coq.setoid_ring.Ring_theory]
r:288 [in Coq.Reals.Abstract.ConstructiveReals]
r:289 [in Coq.MSets.MSetRBT]
R:29 [in Coq.Classes.RelationClasses]
R:29 [in Coq.Reals.Abstract.ConstructivePower]
r:29 [in Coq.setoid_ring.Integral_domain]
r:29 [in Coq.MSets.MSetAVL]
r:29 [in Coq.Reals.Raxioms]
r:29 [in Coq.MSets.MSetRBT]
R:29 [in Coq.Classes.CRelationClasses]
r:29 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
r:29 [in Coq.Numbers.HexadecimalQ]
r:29 [in Coq.Numbers.NatInt.NZDiv]
r:29 [in Coq.Arith.Between]
r:29 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
r:29 [in Coq.Reals.ClassicalConstructiveReals]
r:290 [in Coq.PArith.BinPos]
r:290 [in Coq.MSets.MSetGenTree]
R:291 [in Coq.Reals.Abstract.ConstructiveReals]
r:292 [in Coq.Reals.Abstract.ConstructiveReals]
r:293 [in Coq.PArith.BinPos]
R:295 [in Coq.Reals.Abstract.ConstructiveReals]
r:296 [in Coq.Reals.Abstract.ConstructiveReals]
r:296 [in Coq.MSets.MSetRBT]
r:296 [in Coq.MSets.MSetGenTree]
R:299 [in Coq.Reals.Abstract.ConstructiveReals]
r:299 [in Coq.Reals.Ratan]
r:3 [in Coq.Reals.R_Ifp]
R:3 [in Coq.FSets.FSetDecide]
R:3 [in Coq.Logic.SetoidChoice]
R:3 [in Coq.Classes.Morphisms]
R:3 [in Coq.Classes.RelationPairs]
R:3 [in Coq.MSets.MSetDecide]
R:3 [in Coq.Reals.Abstract.ConstructiveAbs]
R:3 [in Coq.Logic.RelationalChoice]
r:3 [in Coq.Reals.Ratan]
r:3 [in Coq.Reals.RIneq]
r:30 [in Coq.FSets.FMapFullAVL]
R:30 [in Coq.Reals.Abstract.ConstructiveAbs]
r:30 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
r:300 [in Coq.Reals.Abstract.ConstructiveReals]
R:300 [in Coq.micromega.EnvRing]
r:300 [in Coq.MSets.MSetRBT]
r:301 [in Coq.Reals.Ratan]
R:303 [in Coq.Reals.Abstract.ConstructiveReals]
R:305 [in Coq.Reals.Abstract.ConstructiveReals]
r:305 [in Coq.micromega.RingMicromega]
r:306 [in Coq.Reals.Abstract.ConstructiveReals]
r:308 [in Coq.ssr.ssrbool]
R:309 [in Coq.Reals.Abstract.ConstructiveReals]
R:31 [in Coq.Reals.Abstract.ConstructiveLimits]
r:31 [in Coq.Numbers.HexadecimalQ]
r:31 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
R:31 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:31 [in Coq.Reals.ClassicalConstructiveReals]
r:312 [in Coq.ssr.ssrbool]
R:315 [in Coq.Reals.Abstract.ConstructiveReals]
R:32 [in Coq.Classes.Morphisms]
R:32 [in Coq.Reals.Abstract.ConstructiveAbs]
R:32 [in Coq.Classes.CMorphisms]
r:32 [in Coq.Arith.Between]
r:32 [in Coq.micromega.RMicromega]
R:320 [in Coq.Reals.Abstract.ConstructiveReals]
r:320 [in Coq.ssr.ssrbool]
R:323 [in Coq.Reals.Abstract.ConstructiveReals]
r:323 [in Coq.MSets.MSetRBT]
r:324 [in Coq.Reals.Abstract.ConstructiveReals]
R:326 [in Coq.Reals.Abstract.ConstructiveReals]
r:326 [in Coq.Reals.RIneq]
R:327 [in Coq.Reals.Abstract.ConstructiveReals]
r:327 [in Coq.MSets.MSetRBT]
r:329 [in Coq.Reals.Abstract.ConstructiveReals]
r:329 [in Coq.Reals.RIneq]
r:33 [in Coq.Reals.Rtrigo1]
R:33 [in Coq.Classes.RelationClasses]
R:33 [in Coq.Reals.Abstract.ConstructivePower]
R:33 [in Coq.Logic.ChoiceFacts]
R:33 [in Coq.Sets.Relations_2_facts]
r:33 [in Coq.Numbers.HexadecimalQ]
r:33 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
R:330 [in Coq.Reals.Abstract.ConstructiveReals]
R:331 [in Coq.Reals.Abstract.ConstructiveReals]
r:332 [in Coq.Reals.RIneq]
R:333 [in Coq.Reals.Abstract.ConstructiveReals]
r:334 [in Coq.MSets.MSetRBT]
R:335 [in Coq.Reals.Abstract.ConstructiveReals]
r:335 [in Coq.Reals.RIneq]
R:338 [in Coq.Reals.Abstract.ConstructiveReals]
r:338 [in Coq.MSets.MSetRBT]
r:338 [in Coq.Reals.RIneq]
r:34 [in Coq.Reals.Rtrigo1]
r:34 [in Coq.FSets.FMapFullAVL]
r:34 [in Coq.MSets.MSetRBT]
R:34 [in Coq.Classes.CRelationClasses]
r:34 [in Coq.micromega.RMicromega]
R:34 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:341 [in Coq.Reals.Abstract.ConstructiveReals]
r:341 [in Coq.Reals.RIneq]
r:342 [in Coq.Reals.Abstract.ConstructiveReals]
R:344 [in Coq.FSets.FMapFacts]
r:345 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
R:345 [in Coq.Reals.Abstract.ConstructiveReals]
r:346 [in Coq.Reals.Abstract.ConstructiveReals]
r:348 [in Coq.MSets.MSetGenTree]
R:349 [in Coq.Reals.Abstract.ConstructiveReals]
R:35 [in Coq.Reals.Abstract.ConstructivePower]
R:35 [in Coq.setoid_ring.Ncring_tac]
r:35 [in Coq.setoid_ring.Integral_domain]
R:35 [in Coq.Reals.Abstract.ConstructiveLimits]
r:35 [in Coq.Arith.Between]
r:35 [in Coq.micromega.RMicromega]
R:352 [in Coq.Reals.Abstract.ConstructiveReals]
R:355 [in Coq.Reals.Abstract.ConstructiveReals]
R:359 [in Coq.Reals.Abstract.ConstructiveReals]
R:36 [in Coq.Logic.ClassicalDescription]
R:363 [in Coq.Reals.Abstract.ConstructiveReals]
r:364 [in Coq.MSets.MSetRBT]
R:366 [in Coq.Reals.Abstract.ConstructiveReals]
r:368 [in Coq.PArith.BinPos]
r:368 [in Coq.MSets.MSetRBT]
R:369 [in Coq.Reals.Abstract.ConstructiveReals]
R:37 [in Coq.Classes.RelationClasses]
r:37 [in Coq.Init.Wf]
r:37 [in Coq.ZArith.Zdiv]
R:37 [in Coq.Reals.Abstract.ConstructiveSum]
r:370 [in Coq.Reals.Abstract.ConstructiveReals]
r:371 [in Coq.PArith.BinPos]
r:372 [in Coq.Reals.RIneq]
R:373 [in Coq.Reals.Abstract.ConstructiveReals]
r:373 [in Coq.Reals.RIneq]
r:374 [in Coq.Reals.Abstract.ConstructiveReals]
r:374 [in Coq.Reals.RIneq]
r:375 [in Coq.Reals.RIneq]
r:376 [in Coq.PArith.BinPos]
r:376 [in Coq.Reals.RIneq]
R:377 [in Coq.Reals.Abstract.ConstructiveReals]
r:377 [in Coq.Reals.RIneq]
r:378 [in Coq.Reals.Abstract.ConstructiveReals]
r:379 [in Coq.PArith.BinPos]
r:38 [in Coq.Reals.Abstract.ConstructiveReals]
r:38 [in Coq.Reals.Raxioms]
r:38 [in Coq.ZArith.Zquot]
r:38 [in Coq.Arith.Between]
R:38 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:381 [in Coq.Reals.Abstract.ConstructiveReals]
r:382 [in Coq.Reals.Abstract.ConstructiveReals]
r:382 [in Coq.PArith.BinPos]
r:383 [in Coq.FSets.FMapWeakList]
R:385 [in Coq.Reals.Abstract.ConstructiveReals]
r:385 [in Coq.FSets.FMapWeakList]
r:386 [in Coq.PArith.BinPos]
r:386 [in Coq.Reals.RIneq]
R:386 [in Coq.Init.Logic]
r:387 [in Coq.MSets.MSetRBT]
r:389 [in Coq.PArith.BinPos]
r:389 [in Coq.Reals.RIneq]
r:39 [in Coq.Init.Decimal]
R:39 [in Coq.Reals.Abstract.ConstructiveLUB]
r:39 [in Coq.PArith.BinPos]
R:39 [in Coq.Classes.RelationClasses]
R:39 [in Coq.Logic.ClassicalEpsilon]
R:39 [in Coq.Reals.Abstract.ConstructivePower]
R:39 [in Coq.Logic.ChoiceFacts]
r:39 [in Coq.Init.Hexadecimal]
R:39 [in Coq.Reals.Abstract.ConstructiveAbs]
R:39 [in Coq.Reals.Abstract.ConstructiveLimits]
r:392 [in Coq.PArith.BinPos]
r:392 [in Coq.Reals.RIneq]
r:395 [in Coq.Reals.RIneq]
r:396 [in Coq.PArith.BinPos]
r:398 [in Coq.setoid_ring.Ring_polynom]
r:398 [in Coq.Reals.RIneq]
r:399 [in Coq.PArith.BinPos]
R:4 [in Coq.Logic.ChoiceFacts]
r:4 [in Coq.Relations.Relations]
r:4 [in Coq.ZArith.Zdiv]
R:4 [in Coq.Logic.ClassicalUniqueChoice]
R:4 [in Coq.Numbers.NatInt.NZDomain]
R:4 [in Coq.Sets.Relations_2_facts]
R:4 [in Coq.Numbers.Cyclic.Int63.Ring63]
r:4 [in Coq.Reals.RIneq]
R:4 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:4 [in Coq.Numbers.Cyclic.Int31.Ring31]
R:40 [in Coq.micromega.ZifyClasses]
R:40 [in Coq.Init.Peano]
r:40 [in Coq.ZArith.BinInt]
R:40 [in Coq.Classes.CRelationClasses]
r:401 [in Coq.Reals.RIneq]
r:402 [in Coq.PArith.BinPos]
r:404 [in Coq.Reals.RIneq]
r:405 [in Coq.PArith.BinPos]
r:408 [in Coq.PArith.BinPos]
r:41 [in Coq.Reals.Abstract.ConstructiveReals]
R:41 [in Coq.Reals.Abstract.ConstructivePower]
R:41 [in Coq.Reals.Abstract.ConstructiveLimits]
r:41 [in Coq.Reals.Raxioms]
r:41 [in Coq.ZArith.Zquot]
r:41 [in Coq.Arith.Between]
r:412 [in Coq.PArith.BinPos]
r:412 [in Coq.Numbers.Cyclic.Int63.Int63]
r:413 [in Coq.setoid_ring.Ring_polynom]
r:415 [in Coq.PArith.BinPos]
r:418 [in Coq.PArith.BinPos]
r:42 [in Coq.Init.Decimal]
r:42 [in Coq.FSets.FSetBridge]
r:42 [in Coq.Reals.ArithProp]
r:42 [in Coq.micromega.ZifyBool]
r:42 [in Coq.Init.Hexadecimal]
R:42 [in Coq.Reals.Abstract.ConstructiveAbs]
r:42 [in Coq.FSets.FMapAVL]
r:42 [in Coq.Reals.PSeries_reg]
R:42 [in Coq.Reals.Abstract.ConstructiveSum]
R:42 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:43 [in Coq.PArith.BinPos]
R:43 [in Coq.Classes.RelationClasses]
R:43 [in Coq.Reals.Abstract.ConstructivePower]
r:430 [in Coq.Numbers.Cyclic.Int63.Int63]
r:432 [in Coq.PArith.BinPos]
r:433 [in Coq.Reals.RIneq]
r:435 [in Coq.PArith.BinPos]
r:436 [in Coq.Reals.RIneq]
r:439 [in Coq.setoid_ring.Ring_polynom]
r:439 [in Coq.Init.Specif]
r:439 [in Coq.Reals.RIneq]
R:44 [in Coq.Reals.Abstract.ConstructiveLUB]
R:44 [in Coq.Classes.Morphisms]
R:44 [in Coq.Logic.ChoiceFacts]
r:44 [in Coq.FSets.FMapFullAVL]
R:44 [in Coq.Classes.CRelationClasses]
r:44 [in Coq.ZArith.Zquot]
r:44 [in Coq.Arith.Between]
r:44 [in Coq.micromega.RMicromega]
R:440 [in Coq.setoid_ring.Field_theory]
r:442 [in Coq.PArith.BinPos]
r:442 [in Coq.setoid_ring.Ring_polynom]
r:442 [in Coq.Reals.RIneq]
r:445 [in Coq.PArith.BinPos]
r:445 [in Coq.setoid_ring.Ring_polynom]
r:445 [in Coq.Reals.RIneq]
r:447 [in Coq.Reals.Ranalysis5]
r:448 [in Coq.PArith.BinPos]
r:448 [in Coq.Reals.RIneq]
r:45 [in Coq.micromega.ZifyBool]
R:45 [in Coq.Reals.Abstract.ConstructiveAbs]
R:45 [in Coq.Classes.CMorphisms]
r:450 [in Coq.setoid_ring.Ring_polynom]
r:451 [in Coq.PArith.BinPos]
r:451 [in Coq.Reals.RIneq]
r:454 [in Coq.PArith.BinPos]
r:454 [in Coq.Reals.RIneq]
r:457 [in Coq.PArith.BinPos]
r:46 [in Coq.Init.Decimal]
r:46 [in Coq.PArith.BinPos]
R:46 [in Coq.setoid_ring.Ncring_tac]
r:46 [in Coq.Init.Hexadecimal]
r:46 [in Coq.Reals.PSeries_reg]
R:46 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:462 [in Coq.PArith.BinPos]
r:465 [in Coq.PArith.BinPos]
r:465 [in Coq.setoid_ring.Ring_polynom]
r:468 [in Coq.PArith.BinPos]
R:469 [in Coq.Init.Specif]
r:47 [in Coq.Reals.Abstract.ConstructiveReals]
R:47 [in Coq.setoid_ring.Ncring_initial]
r:47 [in Coq.FSets.FSetBridge]
R:47 [in Coq.Reals.Abstract.ConstructiveLimits]
r:47 [in Coq.Arith.Between]
r:472 [in Coq.Init.Specif]
r:477 [in Coq.Reals.RIneq]
r:479 [in Coq.Reals.RIneq]
r:48 [in Coq.Init.Decimal]
R:48 [in Coq.Reals.Abstract.ConstructiveLUB]
R:48 [in Coq.Classes.RelationClasses]
R:48 [in Coq.Classes.Morphisms]
r:48 [in Coq.setoid_ring.Field_theory]
r:48 [in Coq.Init.Hexadecimal]
R:48 [in Coq.ssr.ssreflect]
r:48 [in Coq.MSets.MSetRBT]
R:48 [in Coq.Classes.CRelationClasses]
r:48 [in Coq.ZArith.Zquot]
r:48 [in Coq.Logic.HLevels]
r:480 [in Coq.Reals.RIneq]
R:482 [in Coq.Init.Specif]
r:485 [in Coq.Reals.RIneq]
r:486 [in Coq.Reals.RIneq]
r:49 [in Coq.PArith.BinPos]
r:49 [in Coq.Init.Wf]
r:49 [in Coq.setoid_ring.Field_theory]
r:49 [in Coq.FSets.FMapFullAVL]
r:49 [in Coq.ssr.ssreflect]
r:49 [in Coq.MSets.MSetRBT]
R:490 [in Coq.Init.Specif]
r:491 [in Coq.Reals.RIneq]
r:492 [in Coq.Reals.RIneq]
r:494 [in Coq.setoid_ring.Ring_polynom]
r:495 [in Coq.Init.Logic]
r:497 [in Coq.MSets.MSetAVL]
r:498 [in Coq.setoid_ring.Ring_polynom]
r:5 [in Coq.Reals.R_Ifp]
r:5 [in Coq.Reals.Rseries]
R:5 [in Coq.Classes.SetoidTactics]
R:5 [in Coq.Classes.CEquivalence]
R:5 [in Coq.Reals.Abstract.ConstructiveAbs]
R:5 [in Coq.Classes.Equivalence]
r:50 [in Coq.Reals.Abstract.ConstructiveReals]
R:50 [in Coq.Classes.RelationClasses]
R:50 [in Coq.Classes.CMorphisms]
R:50 [in Coq.Classes.CRelationClasses]
r:50 [in Coq.Arith.Between]
R:50 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:501 [in Coq.MSets.MSetAVL]
r:508 [in Coq.MSets.MSetAVL]
r:509 [in Coq.setoid_ring.Ring_polynom]
r:51 [in Coq.ZArith.Zdiv]
r:51 [in Coq.Reals.Raxioms]
r:512 [in Coq.MSets.MSetAVL]
r:513 [in Coq.Init.Specif]
R:519 [in Coq.Init.Specif]
r:52 [in Coq.PArith.BinPos]
R:52 [in Coq.Logic.ChoiceFacts]
r:52 [in Coq.ZArith.Zquot]
r:52 [in Coq.Reals.PSeries_reg]
R:52 [in Coq.Reals.Abstract.ConstructiveSum]
R:520 [in Coq.Init.Logic]
r:521 [in Coq.setoid_ring.Ring_polynom]
R:525 [in Coq.ssr.ssrbool]
r:529 [in Coq.MSets.MSetAVL]
R:53 [in Coq.Reals.Abstract.ConstructiveLimits]
r:53 [in Coq.Logic.HLevels]
r:53 [in Coq.Reals.Ratan]
r:533 [in Coq.MSets.MSetAVL]
R:54 [in Coq.Classes.RelationClasses]
R:54 [in Coq.Classes.CRelationClasses]
r:54 [in Coq.Reals.Rbasic_fun]
R:54 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:540 [in Coq.MSets.MSetAVL]
r:545 [in Coq.MSets.MSetAVL]
r:55 [in Coq.Reals.Abstract.ConstructiveLUB]
r:55 [in Coq.PArith.BinPos]
r:55 [in Coq.ZArith.Zdiv]
r:55 [in Coq.Logic.HLevels]
R:55 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r:550 [in Coq.MSets.MSetAVL]
r:551 [in Coq.PArith.BinPos]
r:56 [in Coq.Init.Nat]
r:56 [in Coq.ZArith.Zquot]
R:56 [in Coq.Reals.Abstract.ConstructiveSum]
r:564 [in Coq.Reals.RIneq]
r:566 [in Coq.PArith.BinPos]
r:567 [in Coq.Reals.RIneq]
r:569 [in Coq.PArith.BinPos]
r:57 [in Coq.Reals.Abstract.ConstructiveReals]
R:57 [in Coq.setoid_ring.Ncring_tac]
r:57 [in Coq.setoid_ring.Field_theory]
r:57 [in Coq.Arith.Between]
r:57 [in Coq.Numbers.Natural.Abstract.NGcd]
R:57 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:570 [in Coq.Reals.RIneq]
r:574 [in Coq.PArith.BinPos]
r:577 [in Coq.PArith.BinPos]
r:58 [in Coq.PArith.BinPos]
R:58 [in Coq.Classes.Morphisms]
R:58 [in Coq.Logic.ChoiceFacts]
r:58 [in Coq.setoid_ring.Field_theory]
R:58 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:58 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
r:583 [in Coq.MSets.MSetRBT]
r:587 [in Coq.MSets.MSetRBT]
r:59 [in Coq.FSets.FSetDecide]
R:59 [in Coq.Classes.RelationClasses]
r:59 [in Coq.Numbers.Cyclic.Int63.Int63]
r:59 [in Coq.MSets.MSetDecide]
r:59 [in Coq.setoid_ring.Field_theory]
r:59 [in Coq.ZArith.Zdiv]
R:59 [in Coq.Reals.Abstract.ConstructiveLimits]
R:59 [in Coq.Classes.CRelationClasses]
R:59 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:592 [in Coq.Init.Specif]
r:593 [in Coq.MSets.MSetRBT]
R:6 [in Coq.Reals.Abstract.ConstructiveLUB]
R:6 [in Coq.FSets.FSetDecide]
R:6 [in Coq.Classes.RelationClasses]
R:6 [in Coq.Reals.Abstract.ConstructivePower]
R:6 [in Coq.setoid_ring.Ncring_tac]
R:6 [in Coq.MSets.MSetDecide]
r:6 [in Coq.MSets.MSetAVL]
R:6 [in Coq.Classes.CMorphisms]
R:6 [in Coq.Reals.Abstract.ConstructiveLimits]
R:6 [in Coq.Sets.Relations_1_facts]
R:6 [in Coq.Sets.Relations_2_facts]
r:6 [in Coq.Reals.Rlimit]
R:6 [in Coq.Sets.Relations_3_facts]
R:6 [in Coq.Reals.Abstract.ConstructiveSum]
r:6 [in Coq.NArith.Ndiv_def]
r:6 [in Coq.Arith.Euclid]
r:60 [in Coq.FSets.FMapAVL]
r:60 [in Coq.Reals.PSeries_reg]
r:60 [in Coq.Reals.ClassicalDedekindReals]
r:61 [in Coq.Program.Wf]
r:61 [in Coq.Reals.Abstract.ConstructiveReals]
r:61 [in Coq.PArith.BinPos]
R:61 [in Coq.Classes.CMorphisms]
R:61 [in Coq.Reals.Abstract.ConstructiveSum]
r:62 [in Coq.Reals.Abstract.ConstructiveLUB]
R:62 [in Coq.Classes.Morphisms]
r:62 [in Coq.Numbers.Natural.Abstract.NDefOps]
R:62 [in Coq.Logic.ChoiceFacts]
r:62 [in Coq.FSets.FMapFullAVL]
r:62 [in Coq.NArith.BinNatDef]
r:621 [in Coq.PArith.BinPos]
R:622 [in Coq.Init.Specif]
r:623 [in Coq.MSets.MSetRBT]
r:625 [in Coq.Init.Specif]
r:627 [in Coq.MSets.MSetRBT]
r:63 [in Coq.ZArith.Zdiv]
R:63 [in Coq.Reals.Abstract.ConstructiveLimits]
R:63 [in Coq.Classes.CRelationClasses]
R:63 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:631 [in Coq.MSets.MSetRBT]
R:635 [in Coq.Init.Specif]
r:635 [in Coq.MSets.MSetRBT]
r:639 [in Coq.MSets.MSetRBT]
R:643 [in Coq.Init.Specif]
r:643 [in Coq.MSets.MSetRBT]
r:647 [in Coq.MSets.MSetRBT]
R:65 [in Coq.Classes.RelationClasses]
R:65 [in Coq.Classes.Morphisms]
R:65 [in Coq.Classes.CMorphisms]
r:65 [in Coq.NArith.BinNatDef]
R:65 [in Coq.Reals.Abstract.ConstructiveSum]
r:66 [in Coq.FSets.FMapFullAVL]
R:66 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:664 [in Coq.Init.Specif]
R:667 [in Coq.ssr.ssrbool]
r:667 [in Coq.MSets.MSetRBT]
R:67 [in Coq.Classes.RelationClasses]
r:67 [in Coq.PArith.BinPosDef]
R:670 [in Coq.Init.Specif]
R:68 [in Coq.setoid_ring.Ncring_tac]
r:68 [in Coq.ssr.ssrfun]
R:68 [in Coq.Reals.Abstract.ConstructiveLimits]
r:68 [in Coq.MSets.MSetRBT]
R:68 [in Coq.Classes.CRelationClasses]
r:69 [in Coq.Numbers.Natural.Abstract.NDiv]
R:69 [in Coq.Classes.RelationClasses]
R:69 [in Coq.Classes.Morphisms]
R:69 [in Coq.Classes.CMorphisms]
R:69 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:7 [in Coq.Reals.R_Ifp]
R:7 [in Coq.Classes.Morphisms]
r:7 [in Coq.FSets.FMapFullAVL]
R:7 [in Coq.Reals.Abstract.ConstructiveAbs]
R:7 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:70 [in Coq.Reals.Abstract.ConstructiveReals]
r:70 [in Coq.Reals.Abstract.ConstructiveLUB]
R:70 [in Coq.Reals.Abstract.ConstructiveSum]
r:70 [in Coq.Reals.ClassicalDedekindReals]
R:71 [in Coq.Classes.RelationClasses]
R:71 [in Coq.Reals.Abstract.ConstructiveLimits]
R:71 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:72 [in Coq.Logic.ChoiceFacts]
r:73 [in Coq.Reals.Abstract.ConstructiveReals]
r:73 [in Coq.Reals.Rbasic_fun]
r:73 [in Coq.Reals.PSeries_reg]
R:73 [in Coq.Init.Logic]
r:73 [in Coq.Reals.ClassicalDedekindReals]
R:74 [in Coq.Classes.CMorphisms]
R:74 [in Coq.Reals.Abstract.ConstructiveLimits]
R:74 [in Coq.Classes.CRelationClasses]
R:74 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:75 [in Coq.Reals.Abstract.ConstructiveLUB]
R:75 [in Coq.Reals.Abstract.ConstructiveSum]
R:76 [in Coq.Classes.RelationClasses]
r:76 [in Coq.Numbers.Integer.Abstract.ZGcd]
R:76 [in Coq.Classes.CRelationClasses]
r:76 [in Coq.micromega.ZifyInst]
R:77 [in Coq.Reals.Abstract.ConstructiveLUB]
r:77 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
R:77 [in Coq.Classes.Morphisms]
r:77 [in Coq.Logic.Hurkens]
r:77 [in Coq.Numbers.Cyclic.Int31.Int31]
r:77 [in Coq.ZArith.Znumtheory]
r:78 [in Coq.ssr.ssrfun]
r:78 [in Coq.ZArith.Zpower]
R:78 [in Coq.Classes.CRelationClasses]
R:78 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:79 [in Coq.btauto.Algebra]
R:79 [in Coq.Reals.Abstract.ConstructiveLimits]
R:79 [in Coq.Reals.Abstract.ConstructiveSum]
r:8 [in Coq.Reals.R_Ifp]
R:8 [in Coq.Classes.SetoidTactics]
r:8 [in Coq.ZArith.Zdiv]
R:8 [in Coq.Sets.Relations_1_facts]
R:8 [in Coq.Sets.Relations_2_facts]
R:8 [in Coq.Sets.Relations_3_facts]
R:8 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:8 [in Coq.Classes.Morphisms_Relations]
r:80 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
r:80 [in Coq.Reals.Abstract.ConstructiveLUB]
R:80 [in Coq.setoid_ring.Ncring_tac]
R:80 [in Coq.Classes.CMorphisms]
R:80 [in Coq.Classes.CRelationClasses]
R:81 [in Coq.MSets.MSetProperties]
r:81 [in Coq.Numbers.Cyclic.Int31.Int31]
r:81 [in Coq.micromega.ZifyInst]
R:81 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:81 [in Coq.FSets.FSetProperties]
R:82 [in Coq.Classes.RelationClasses]
R:82 [in Coq.Classes.Morphisms]
r:82 [in Coq.Logic.Hurkens]
r:83 [in Coq.Reals.Rfunctions]
r:83 [in Coq.Numbers.NatInt.NZDiv]
r:83 [in Coq.micromega.ZifyInst]
r:84 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
R:84 [in Coq.Reals.Abstract.ConstructiveLimits]
r:84 [in Coq.ZArith.Zpower]
R:84 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:85 [in Coq.Classes.CRelationClasses]
r:85 [in Coq.micromega.ZifyInst]
R:86 [in Coq.Logic.ChoiceFacts]
r:86 [in Coq.micromega.ZifyInst]
R:87 [in Coq.Reals.Abstract.ConstructiveLUB]
r:87 [in Coq.Reals.Rbasic_fun]
R:87 [in Coq.Reals.Abstract.ConstructiveSum]
r:88 [in Coq.Arith.PeanoNat]
r:88 [in Coq.MSets.MSetGenTree]
r:88 [in Coq.Reals.Rbasic_fun]
R:88 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:89 [in Coq.Classes.Morphisms]
r:89 [in Coq.Reals.Rbasic_fun]
r:89 [in Coq.micromega.ZifyInst]
r:9 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
r:9 [in Coq.Reals.R_Ifp]
R:9 [in Coq.Classes.Morphisms_Prop]
R:9 [in Coq.Classes.RelationClasses]
R:9 [in Coq.Reals.Abstract.ConstructivePower]
r:9 [in Coq.Floats.FloatOps]
R:9 [in Coq.setoid_ring.Ncring_tac]
r:9 [in Coq.MSets.MSetAVL]
r:9 [in Coq.ZArith.Zdiv]
R:9 [in Coq.Classes.EquivDec]
R:9 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:90 [in Coq.Reals.Abstract.ConstructiveLUB]
R:90 [in Coq.Reals.Abstract.ConstructiveLimits]
r:90 [in Coq.Reals.Rbasic_fun]
R:90 [in Coq.Reals.Abstract.ConstructiveSum]
R:91 [in Coq.Classes.RelationClasses]
R:91 [in Coq.Classes.Morphisms]
R:91 [in Coq.Classes.CRelationClasses]
r:91 [in Coq.Reals.Rbasic_fun]
r:92 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
r:92 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
R:92 [in Coq.setoid_ring.Ncring_tac]
r:92 [in Coq.MSets.MSetGenTree]
R:92 [in Coq.Reals.Abstract.ConstructiveMinMax]
R:93 [in Coq.Classes.RelationClasses]
r:93 [in Coq.Reals.PSeries_reg]
R:94 [in Coq.Classes.Morphisms]
R:94 [in Coq.Classes.CMorphisms]
r:94 [in Coq.micromega.ZifyInst]
r:940 [in Coq.FSets.FMapAVL]
r:948 [in Coq.FSets.FMapAVL]
r:95 [in Coq.ZArith.BinIntDef]
R:95 [in Coq.Classes.RelationClasses]
R:95 [in Coq.Reals.Abstract.ConstructiveSum]
r:954 [in Coq.FSets.FMapAVL]
R:96 [in Coq.Reals.Abstract.ConstructiveLimits]
r:96 [in Coq.MSets.MSetGenTree]
R:96 [in Coq.Reals.Abstract.ConstructiveMinMax]
r:960 [in Coq.FSets.FMapAVL]
r:966 [in Coq.FSets.FMapAVL]
R:97 [in Coq.Classes.RelationClasses]
R:97 [in Coq.Classes.Morphisms]
r:97 [in Coq.Arith.PeanoNat]
R:97 [in Coq.Classes.CMorphisms]
r:972 [in Coq.FSets.FMapAVL]
r:978 [in Coq.FSets.FMapAVL]
r:98 [in Coq.ZArith.BinIntDef]
r:98 [in Coq.Reals.Abstract.ConstructiveLUB]
r:98 [in Coq.PArith.BinPosDef]
R:99 [in Coq.Classes.RelationClasses]
r:99 [in Coq.Reals.Abstract.ConstructiveMinMax]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (68863 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (985 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (44709 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (761 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1497 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (570 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11380 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (976 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (603 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (298 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (460 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (476 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (811 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1157 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4018 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (162 entries) |