| 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 | (72745 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 | (47313 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 | (784 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 | (1547 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 | (583 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 | (11764 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 | (627 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 | (492 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 | (903 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 | (1448 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 | (4360 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) |
Y (binder)
yn:12 [in Coq.Reals.Abstract.ConstructiveLimits]yn:3 [in Coq.Reals.Abstract.ConstructiveLimits]
yp:19 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
yp:23 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
yq:20 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
yq:24 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
ys:270 [in Coq.MSets.MSetList]
y'':186 [in Coq.Logic.EqdepFacts]
y'':188 [in Coq.Logic.EqdepFacts]
y':101 [in Coq.Relations.Relation_Operators]
y':111 [in Coq.Relations.Relation_Operators]
y':114 [in Coq.Relations.Relation_Operators]
y':127 [in Coq.Relations.Relation_Operators]
y':185 [in Coq.Logic.EqdepFacts]
y':187 [in Coq.Logic.EqdepFacts]
y':259 [in Coq.Logic.ChoiceFacts]
y':262 [in Coq.Logic.ChoiceFacts]
y':35 [in Coq.Logic.Eqdep_dec]
y':36 [in Coq.Relations.Relation_Definitions]
y':37 [in Coq.Relations.Relation_Definitions]
y':377 [in Coq.Logic.ChoiceFacts]
y':383 [in Coq.Logic.ChoiceFacts]
y':386 [in Coq.Logic.ChoiceFacts]
y':389 [in Coq.Logic.ChoiceFacts]
y':4 [in Coq.Logic.Eqdep_dec]
y':48 [in Coq.Logic.Decidable]
y':58 [in Coq.Logic.Eqdep_dec]
y':58 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y':60 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y':61 [in Coq.Init.Wf]
y':68 [in Coq.Init.Wf]
y':7 [in Coq.Wellfounded.Union]
y':74 [in Coq.Init.Wf]
y':78 [in Coq.Logic.ChoiceFacts]
y':8 [in Coq.Wellfounded.Union]
y':9 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y':98 [in Coq.Relations.Relation_Operators]
y0:12 [in Coq.Reals.Rgeom]
y0:2 [in Coq.Reals.Rgeom]
y0:22 [in Coq.Reals.Rgeom]
y0:26 [in Coq.Wellfounded.Lexicographic_Product]
y0:27 [in Coq.Wellfounded.Lexicographic_Product]
y0:309 [in Coq.Reals.Rtopology]
y0:312 [in Coq.Reals.Rtopology]
y0:338 [in Coq.Reals.Rtopology]
y0:339 [in Coq.Reals.Rtopology]
y0:341 [in Coq.Reals.Rtopology]
y0:342 [in Coq.Reals.Rtopology]
y0:6 [in Coq.Reals.Rgeom]
y0:654 [in Coq.Lists.List]
y0:8 [in Coq.Reals.Rgeom]
y1:10 [in Coq.Reals.Rgeom]
y1:1120 [in Coq.FSets.FMapAVL]
y1:1174 [in Coq.FSets.FMapAVL]
y1:1179 [in Coq.FSets.FMapAVL]
y1:14 [in Coq.Reals.Rgeom]
y1:15 [in Coq.micromega.OrderedRing]
y1:179 [in Coq.Init.Logic]
y1:199 [in Coq.Init.Logic]
y1:20 [in Coq.micromega.OrderedRing]
y1:208 [in Coq.Init.Logic]
y1:220 [in Coq.Init.Logic]
y1:220 [in Coq.setoid_ring.Ncring]
y1:235 [in Coq.Init.Logic]
y1:24 [in Coq.Reals.Rgeom]
y1:28 [in Coq.micromega.OrderedRing]
y1:295 [in Coq.Init.Logic]
y1:327 [in Coq.Init.Logic]
y1:33 [in Coq.micromega.OrderedRing]
y1:34 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y1:35 [in Coq.Reals.Rgeom]
y1:389 [in Coq.Lists.List]
y1:4 [in Coq.Reals.Rgeom]
y1:50 [in Coq.Reals.Rgeom]
y1:54 [in Coq.Lists.List]
y1:55 [in Coq.Reals.Rgeom]
y1:56 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y1:560 [in Coq.MSets.MSetAVL]
y1:577 [in Coq.MSets.MSetAVL]
y1:58 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y1:60 [in Coq.Reals.Rgeom]
y1:67 [in Coq.Reals.Rgeom]
y1:95 [in Coq.Init.Datatypes]
y2:1121 [in Coq.FSets.FMapAVL]
y2:1175 [in Coq.FSets.FMapAVL]
y2:1180 [in Coq.FSets.FMapAVL]
y2:16 [in Coq.micromega.OrderedRing]
y2:16 [in Coq.Reals.Rgeom]
y2:180 [in Coq.Init.Logic]
y2:201 [in Coq.Init.Logic]
y2:21 [in Coq.micromega.OrderedRing]
y2:210 [in Coq.Init.Logic]
y2:221 [in Coq.setoid_ring.Ncring]
y2:222 [in Coq.Init.Logic]
y2:237 [in Coq.Init.Logic]
y2:26 [in Coq.Reals.Rgeom]
y2:29 [in Coq.micromega.OrderedRing]
y2:296 [in Coq.Init.Logic]
y2:328 [in Coq.Init.Logic]
y2:34 [in Coq.micromega.OrderedRing]
y2:36 [in Coq.Reals.Rgeom]
y2:390 [in Coq.Lists.List]
y2:52 [in Coq.Reals.Rgeom]
y2:55 [in Coq.Lists.List]
y2:561 [in Coq.MSets.MSetAVL]
y2:57 [in Coq.Reals.Rgeom]
y2:578 [in Coq.MSets.MSetAVL]
y2:62 [in Coq.Reals.Rgeom]
y2:69 [in Coq.Reals.Rgeom]
y2:96 [in Coq.Init.Datatypes]
y3:212 [in Coq.Init.Logic]
y3:224 [in Coq.Init.Logic]
y3:239 [in Coq.Init.Logic]
y3:297 [in Coq.Init.Logic]
y4:226 [in Coq.Init.Logic]
y4:241 [in Coq.Init.Logic]
y5:243 [in Coq.Init.Logic]
y:1 [in Coq.Init.Tauto]
y:1 [in Coq.Arith.Cantor]
y:10 [in Coq.Structures.DecidableTypeEx]
Y:10 [in Coq.Sets.Finite_sets_facts]
y:10 [in Coq.PArith.BinPos]
y:10 [in Coq.ZArith.BinInt]
y:10 [in Coq.funind.Recdef]
y:10 [in Coq.Sets.Partial_Order]
y:10 [in Coq.Sets.Relations_1_facts]
y:10 [in Coq.ZArith.Zbool]
y:10 [in Coq.micromega.ZifyComparison]
y:10 [in Coq.Structures.GenericMinMax]
y:10 [in Coq.Reals.PSeries_reg]
y:10 [in Coq.Reals.Ranalysis5]
y:10 [in Coq.omega.PreOmega]
y:10 [in Coq.Sets.Relations_1]
y:10 [in Coq.Relations.Relation_Definitions]
y:10 [in Coq.Reals.ROrderedType]
y:10 [in Coq.Floats.FloatAxioms]
y:10 [in Coq.Sorting.Heap]
y:10 [in Coq.QArith.QArith_base]
y:10 [in Coq.Structures.OrdersFacts]
y:100 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:100 [in Coq.QArith.Qcanon]
y:100 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:100 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:100 [in Coq.Structures.EqualitiesFacts]
y:100 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:100 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:100 [in Coq.Relations.Relation_Operators]
y:101 [in Coq.Program.Wf]
y:101 [in Coq.Logic.Eqdep_dec]
y:101 [in Coq.Structures.OrderedTypeEx]
y:101 [in Coq.Reals.Rbasic_fun]
y:101 [in Coq.setoid_ring.Ring_theory]
y:101 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:101 [in Coq.Structures.OrdersFacts]
y:102 [in Coq.Program.Wf]
y:102 [in Coq.FSets.FSetBridge]
y:102 [in Coq.Reals.Ranalysis4]
y:102 [in Coq.Init.Nat]
y:102 [in Coq.Sorting.Permutation]
y:102 [in Coq.Structures.OrderedType]
y:102 [in Coq.Reals.Ranalysis5]
y:102 [in Coq.Structures.EqualitiesFacts]
y:102 [in Coq.setoid_ring.Ncring]
y:102 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:102 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:103 [in Coq.QArith.Qcanon]
y:103 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
y:103 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:103 [in Coq.Logic.ChoiceFacts]
y:103 [in Coq.Reals.Rpower]
y:103 [in Coq.Reals.Rtopology]
y:103 [in Coq.Reals.Rbasic_fun]
y:103 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:103 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:103 [in Coq.Structures.OrdersFacts]
y:103 [in Coq.Reals.Cos_plus]
y:1036 [in Coq.FSets.FMapAVL]
y:104 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:104 [in Coq.FSets.FMapFacts]
y:104 [in Coq.Reals.Rpower]
y:104 [in Coq.Arith.PeanoNat]
y:104 [in Coq.setoid_ring.Ring_theory]
y:104 [in Coq.micromega.ZifyInst]
y:104 [in Coq.Reals.ClassicalDedekindReals]
y:104 [in Coq.Logic.FinFun]
y:1045 [in Coq.FSets.FMapAVL]
y:105 [in Coq.Program.Wf]
y:105 [in Coq.QArith.Qcanon]
y:105 [in Coq.Init.Nat]
y:105 [in Coq.Reals.PSeries_reg]
y:105 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:1050 [in Coq.FSets.FMapAVL]
y:1056 [in Coq.FSets.FMapAVL]
y:1059 [in Coq.FSets.FMapAVL]
y:106 [in Coq.Program.Wf]
y:106 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:106 [in Coq.Logic.ChoiceFacts]
y:106 [in Coq.Reals.Ranalysis5]
y:106 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:106 [in Coq.setoid_ring.Ncring]
y:106 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:106 [in Coq.Structures.OrdersFacts]
y:1060 [in Coq.Lists.List]
y:1062 [in Coq.Init.Specif]
y:1066 [in Coq.FSets.FMapAVL]
y:107 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:107 [in Coq.Program.Wf]
y:107 [in Coq.Reals.Abstract.ConstructiveReals]
y:107 [in Coq.QArith.Qcanon]
y:107 [in Coq.Lists.List]
y:107 [in Coq.Structures.OrderedType]
y:107 [in Coq.Reals.PSeries_reg]
y:107 [in Coq.Init.Logic]
y:107 [in Coq.micromega.ZifyInst]
y:1070 [in Coq.FSets.FMapAVL]
y:1071 [in Coq.Lists.List]
y:1075 [in Coq.FSets.FMapAVL]
y:1077 [in Coq.Lists.List]
y:108 [in Coq.Program.Wf]
y:108 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:1080 [in Coq.FSets.FMapAVL]
y:1082 [in Coq.Init.Specif]
y:1084 [in Coq.Lists.List]
y:1087 [in Coq.FSets.FMapAVL]
y:1088 [in Coq.Init.Specif]
y:109 [in Coq.Program.Wf]
y:109 [in Coq.QArith.Qcanon]
y:109 [in Coq.Reals.Rfunctions]
y:109 [in Coq.Reals.Rtopology]
y:109 [in Coq.Reals.PSeries_reg]
y:109 [in Coq.Lists.SetoidList]
y:109 [in Coq.Structures.OrdersFacts]
y:1093 [in Coq.FSets.FMapAVL]
y:11 [in Coq.Structures.Orders]
y:11 [in Coq.Relations.Operators_Properties]
y:11 [in Coq.Structures.OrdersLists]
y:11 [in Coq.Sets.Relations_3]
y:11 [in Coq.FSets.FSetDecide]
y:11 [in Coq.Arith.Bool_nat]
y:11 [in Coq.Reals.Exp_prop]
y:11 [in Coq.MSets.MSetDecide]
y:11 [in Coq.Relations.Relations]
y:11 [in Coq.QArith.Qreals]
y:11 [in Coq.Lists.SetoidPermutation]
y:11 [in Coq.Structures.OrderedTypeEx]
y:11 [in Coq.Reals.Raxioms]
y:11 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
y:11 [in Coq.Bool.BoolEq]
y:11 [in Coq.Classes.SetoidDec]
y:11 [in Coq.Strings.Byte]
y:11 [in Coq.Logic.HLevels]
y:11 [in Coq.Sets.Relations_2]
Y:11 [in Coq.Sets.Classical_sets]
y:11 [in Coq.Structures.OrdersTac]
y:11 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:110 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:110 [in Coq.Program.Wf]
y:110 [in Coq.Logic.Eqdep_dec]
y:110 [in Coq.Logic.ChoiceFacts]
y:110 [in Coq.setoid_ring.Field_theory]
y:110 [in Coq.Structures.OrderedType]
y:110 [in Coq.Reals.Ranalysis5]
y:110 [in Coq.setoid_ring.Ring_theory]
y:110 [in Coq.setoid_ring.Ncring]
y:110 [in Coq.Relations.Relation_Operators]
y:1101 [in Coq.Init.Specif]
y:111 [in Coq.Program.Wf]
y:111 [in Coq.QArith.Qcanon]
y:111 [in Coq.FSets.FMapFacts]
y:111 [in Coq.Lists.ListSet]
y:111 [in Coq.Reals.PSeries_reg]
y:111 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:111 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:1110 [in Coq.FSets.FMapAVL]
y:1112 [in Coq.Lists.List]
y:1113 [in Coq.FSets.FMapAVL]
y:1116 [in Coq.Lists.List]
y:1116 [in Coq.FSets.FMapAVL]
y:112 [in Coq.Program.Wf]
y:112 [in Coq.Logic.Eqdep_dec]
y:112 [in Coq.FSets.FSetDecide]
y:112 [in Coq.MSets.MSetDecide]
y:112 [in Coq.Reals.PSeries_reg]
y:112 [in Coq.Structures.OrdersFacts]
y:1124 [in Coq.FSets.FMapAVL]
y:1127 [in Coq.Lists.List]
y:1129 [in Coq.FSets.FMapAVL]
y:113 [in Coq.Program.Wf]
y:113 [in Coq.QArith.Qcanon]
y:113 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:113 [in Coq.Reals.Rtrigo1]
y:113 [in Coq.Structures.GenericMinMax]
y:113 [in Coq.Reals.Ratan]
y:113 [in Coq.setoid_ring.Ring_theory]
y:113 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:113 [in Coq.Relations.Relation_Operators]
y:1132 [in Coq.FSets.FMapAVL]
y:1136 [in Coq.FSets.FMapAVL]
y:1138 [in Coq.Lists.List]
y:114 [in Coq.Program.Wf]
y:114 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
y:114 [in Coq.Lists.List]
y:114 [in Coq.MSets.MSetGenTree]
y:114 [in Coq.Lists.ListSet]
y:114 [in Coq.Reals.PSeries_reg]
y:114 [in Coq.setoid_ring.Ncring]
y:114 [in Coq.Lists.SetoidList]
y:1142 [in Coq.Lists.List]
y:1142 [in Coq.FSets.FMapAVL]
y:1149 [in Coq.Lists.List]
y:115 [in Coq.Program.Wf]
y:115 [in Coq.QArith.Qcanon]
y:115 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:115 [in Coq.Reals.Rtrigo1]
y:115 [in Coq.Reals.Rtopology]
y:115 [in Coq.Structures.OrdersFacts]
y:1151 [in Coq.FSets.FMapAVL]
y:1152 [in Coq.Lists.List]
y:1154 [in Coq.FSets.FMapAVL]
y:1155 [in Coq.Lists.List]
y:1157 [in Coq.FSets.FMapAVL]
y:116 [in Coq.Program.Wf]
y:116 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
y:116 [in Coq.Logic.ChoiceFacts]
y:116 [in Coq.Reals.Rtopology]
y:116 [in Coq.Structures.OrderedType]
y:116 [in Coq.Reals.PSeries_reg]
y:116 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:116 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:1161 [in Coq.Lists.List]
y:1164 [in Coq.Lists.List]
y:1168 [in Coq.FSets.FMapAVL]
y:117 [in Coq.Program.Wf]
y:117 [in Coq.Reals.Rtrigo1]
y:117 [in Coq.Logic.EqdepFacts]
y:117 [in Coq.Logic.Hurkens]
y:117 [in Coq.Reals.Rtopology]
y:117 [in Coq.MSets.MSetGenTree]
y:117 [in Coq.Lists.ListSet]
y:117 [in Coq.setoid_ring.Ring_theory]
y:117 [in Coq.Structures.OrdersFacts]
y:1171 [in Coq.FSets.FMapAVL]
y:1178 [in Coq.FSets.FMapAVL]
y:118 [in Coq.Program.Wf]
y:118 [in Coq.setoid_ring.InitialRing]
y:118 [in Coq.Reals.Rtopology]
y:118 [in Coq.Reals.Ratan]
y:118 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:119 [in Coq.Program.Wf]
y:119 [in Coq.Reals.Rtrigo1]
y:119 [in Coq.Floats.SpecFloat]
y:119 [in Coq.Reals.RiemannInt]
y:119 [in Coq.Logic.Hurkens]
y:119 [in Coq.ssr.ssrfun]
y:119 [in Coq.Structures.OrderedTypeEx]
y:119 [in Coq.Reals.Rtopology]
y:119 [in Coq.Structures.OrderedType]
y:119 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:1194 [in Coq.FSets.FMapAVL]
y:12 [in Coq.Program.Wf]
y:12 [in Coq.Structures.DecidableTypeEx]
y:12 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:12 [in Coq.Wellfounded.Inverse_Image]
y:12 [in Coq.Logic.Eqdep_dec]
y:12 [in Coq.Structures.OrdersEx]
y:12 [in Coq.Reals.ArithProp]
y:12 [in Coq.Logic.JMeq]
y:12 [in Coq.Structures.OrdersAlt]
y:12 [in Coq.Logic.ChoiceFacts]
y:12 [in Coq.Reals.Machin]
y:12 [in Coq.ZArith.Zwf]
y:12 [in Coq.Sets.Cpo]
y:12 [in Coq.funind.Recdef]
y:12 [in Coq.Structures.OrderedTypeAlt]
y:12 [in Coq.micromega.ZifySint63]
y:12 [in Coq.ZArith.Zbool]
y:12 [in Coq.micromega.ZifyUint63]
y:12 [in Coq.Sets.Permut]
y:12 [in Coq.Reals.Ranalysis5]
y:12 [in Coq.Sets.Relations_2]
y:12 [in Coq.omega.PreOmega]
y:12 [in Coq.Reals.Rlogic]
y:12 [in Coq.Reals.ROrderedType]
y:12 [in Coq.Reals.Cos_rel]
Y:12 [in Coq.Sets.Infinite_sets]
y:12 [in Coq.Reals.ClassicalConstructiveReals]
y:12 [in Coq.Relations.Relation_Operators]
y:12 [in Coq.Bool.DecBool]
y:12 [in Coq.Structures.OrdersFacts]
y:12 [in Coq.Sets.Powerset]
y:120 [in Coq.Program.Wf]
y:120 [in Coq.MSets.MSetList]
y:120 [in Coq.Reals.Rtopology]
y:120 [in Coq.Lists.ListSet]
y:120 [in Coq.Reals.Ratan]
y:120 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:120 [in Coq.Structures.OrdersFacts]
y:121 [in Coq.Program.Wf]
y:121 [in Coq.Reals.Abstract.ConstructiveReals]
y:121 [in Coq.Reals.Rtrigo1]
y:121 [in Coq.Reals.Ranalysis5]
y:121 [in Coq.setoid_ring.Ring_theory]
y:121 [in Coq.Init.Logic]
y:122 [in Coq.Program.Wf]
y:122 [in Coq.Logic.EqdepFacts]
y:122 [in Coq.PArith.BinPos]
y:122 [in Coq.Reals.MVT]
y:122 [in Coq.FSets.FMapFacts]
y:122 [in Coq.Reals.RiemannInt]
y:122 [in Coq.Logic.ChoiceFacts]
y:122 [in Coq.Structures.OrderedTypeEx]
y:122 [in Coq.Classes.CRelationClasses]
y:122 [in Coq.Structures.OrderedType]
y:122 [in Coq.Reals.Ratan]
y:122 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:122 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:122 [in Coq.Structures.OrdersFacts]
y:123 [in Coq.QArith.Qcanon]
y:123 [in Coq.Logic.Eqdep_dec]
y:123 [in Coq.Reals.Rtrigo1]
y:123 [in Coq.Logic.ChoiceFacts]
y:124 [in Coq.Reals.PSeries_reg]
y:124 [in Coq.Reals.Ratan]
y:124 [in Coq.Structures.OrdersFacts]
y:125 [in Coq.Reals.Abstract.ConstructiveReals]
y:125 [in Coq.Reals.Abstract.ConstructiveLUB]
y:125 [in Coq.Reals.Rtrigo1]
y:125 [in Coq.Reals.MVT]
y:125 [in Coq.FSets.FMapFacts]
y:125 [in Coq.Reals.RiemannInt]
y:125 [in Coq.Reals.PSeries_reg]
y:125 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:125 [in Coq.Relations.Relation_Operators]
y:126 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:126 [in Coq.Logic.EqdepFacts]
y:126 [in Coq.Classes.CRelationClasses]
y:126 [in Coq.Relations.Relation_Operators]
y:126 [in Coq.Structures.OrdersFacts]
y:127 [in Coq.QArith.Qcanon]
y:127 [in Coq.Reals.Rtrigo1]
y:127 [in Coq.Logic.ChoiceFacts]
y:127 [in Coq.Reals.Rbasic_fun]
y:128 [in Coq.Program.Wf]
y:128 [in Coq.Lists.ListSet]
y:128 [in Coq.Structures.OrdersFacts]
y:129 [in Coq.Program.Wf]
y:129 [in Coq.Reals.Abstract.ConstructiveReals]
y:129 [in Coq.Reals.Abstract.ConstructiveLUB]
y:129 [in Coq.Reals.Rtrigo1]
y:129 [in Coq.setoid_ring.InitialRing]
y:129 [in Coq.ssr.ssrfun]
y:129 [in Coq.Reals.Rbasic_fun]
y:1292 [in Coq.FSets.FMapAVL]
y:13 [in Coq.Program.Wf]
y:13 [in Coq.Relations.Operators_Properties]
y:13 [in Coq.ZArith.BinIntDef]
y:13 [in Coq.FSets.FSetDecide]
y:13 [in Coq.Logic.EqdepFacts]
y:13 [in Coq.Arith.Bool_nat]
y:13 [in Coq.Reals.MVT]
y:13 [in Coq.ZArith.Zpow_facts]
y:13 [in Coq.Arith.Wf_nat]
y:13 [in Coq.MSets.MSetDecide]
y:13 [in Coq.Program.Subset]
y:13 [in Coq.Init.Wf]
y:13 [in Coq.setoid_ring.Cring]
y:13 [in Coq.QArith.Qreals]
y:13 [in Coq.QArith.Qfield]
y:13 [in Coq.QArith.Qabs]
y:13 [in Coq.Lists.ListDec]
y:13 [in Coq.Classes.EquivDec]
y:13 [in Coq.Reals.Raxioms]
y:13 [in Coq.Structures.Equalities]
y:13 [in Coq.Bool.BoolEq]
y:13 [in Coq.Structures.GenericMinMax]
y:13 [in Coq.Logic.ProofIrrelevanceFacts]
y:13 [in Coq.Numbers.Cyclic.Int63.Ring63]
y:13 [in Coq.Structures.OrdersTac]
y:13 [in Coq.Reals.R_sqr]
y:13 [in Coq.QArith.Qround]
y:13 [in Coq.Relations.Relation_Operators]
y:13 [in Coq.Sorting.Heap]
y:13 [in Coq.Lists.SetoidList]
y:13 [in Coq.Numbers.Cyclic.Int31.Ring31]
y:130 [in Coq.QArith.Qcanon]
y:130 [in Coq.Logic.Eqdep_dec]
y:130 [in Coq.FSets.FMapFacts]
y:130 [in Coq.Reals.RiemannInt]
y:130 [in Coq.Logic.Hurkens]
y:130 [in Coq.Classes.CRelationClasses]
y:130 [in Coq.Reals.Rtopology]
y:130 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:130 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:130 [in Coq.Structures.OrdersFacts]
y:131 [in Coq.Reals.Rtrigo1]
y:131 [in Coq.FSets.FSetDecide]
y:131 [in Coq.MSets.MSetEqProperties]
y:131 [in Coq.Reals.RiemannInt]
y:131 [in Coq.MSets.MSetDecide]
y:131 [in Coq.MSets.MSetList]
y:131 [in Coq.ssr.ssreflect]
y:131 [in Coq.FSets.FSetEqProperties]
y:131 [in Coq.Lists.ListSet]
y:132 [in Coq.Program.Wf]
y:132 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:132 [in Coq.Reals.MVT]
y:132 [in Coq.Reals.RiemannInt]
y:132 [in Coq.Logic.Hurkens]
y:132 [in Coq.ssr.ssreflect]
y:132 [in Coq.Reals.Rpower]
y:132 [in Coq.Reals.Rtopology]
y:133 [in Coq.Program.Wf]
y:133 [in Coq.QArith.Qcanon]
y:133 [in Coq.Reals.Rtrigo1]
y:133 [in Coq.Arith.Wf_nat]
y:133 [in Coq.Reals.RiemannInt]
y:133 [in Coq.ssr.ssreflect]
y:133 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:1337 [in Coq.FSets.FMapAVL]
y:134 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:134 [in Coq.FSets.FMapFacts]
y:134 [in Coq.FSets.FSetInterface]
y:134 [in Coq.ssr.ssreflect]
y:134 [in Coq.Lists.ListSet]
y:134 [in Coq.Relations.Relation_Operators]
y:1342 [in Coq.FSets.FMapAVL]
y:135 [in Coq.Reals.Abstract.ConstructiveReals]
y:135 [in Coq.Reals.Rtrigo1]
y:135 [in Coq.Reals.Rsqrt_def]
y:135 [in Coq.MSets.MSetList]
y:135 [in Coq.Reals.Rtopology]
y:135 [in Coq.FSets.FSetCompat]
y:135 [in Coq.Structures.OrdersFacts]
y:1351 [in Coq.FSets.FMapAVL]
y:1354 [in Coq.FSets.FMapAVL]
y:136 [in Coq.Sorting.PermutSetoid]
y:136 [in Coq.Reals.Rbasic_fun]
y:136 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:136 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:137 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:137 [in Coq.Reals.Rtrigo1]
y:137 [in Coq.Reals.Rsqrt_def]
y:137 [in Coq.Reals.Rtopology]
y:137 [in Coq.FSets.FMapWeakList]
y:137 [in Coq.Reals.Ratan]
y:137 [in Coq.Relations.Relation_Operators]
y:137 [in Coq.Structures.OrdersFacts]
y:138 [in Coq.Reals.Abstract.ConstructiveReals]
y:138 [in Coq.Logic.EqdepFacts]
y:138 [in Coq.Arith.Wf_nat]
y:138 [in Coq.FSets.FMapFacts]
y:138 [in Coq.Reals.Ratan]
y:138 [in Coq.Init.Logic]
y:139 [in Coq.Logic.Eqdep_dec]
y:139 [in Coq.Reals.Rtrigo1]
y:139 [in Coq.Reals.MVT]
y:139 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:139 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:139 [in Coq.Structures.OrdersFacts]
y:1396 [in Coq.FSets.FMapAVL]
y:14 [in Coq.Structures.Orders]
y:14 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:14 [in Coq.nsatz.NsatzTactic]
y:14 [in Coq.Logic.Eqdep_dec]
y:14 [in Coq.FSets.FSetBridge]
y:14 [in Coq.Reals.Rfunctions]
y:14 [in Coq.Reals.MVT]
y:14 [in Coq.Strings.String]
y:14 [in Coq.Reals.Exp_prop]
y:14 [in Coq.Structures.OrdersAlt]
y:14 [in Coq.Numbers.Natural.Abstract.NDefOps]
y:14 [in Coq.setoid_ring.Integral_domain]
y:14 [in Coq.Logic.ClassicalChoice]
y:14 [in Coq.Reals.Abstract.ConstructiveAbs]
y:14 [in Coq.Logic.IndefiniteDescription]
y:14 [in Coq.omega.OmegaLemmas]
y:14 [in Coq.Structures.OrderedTypeEx]
y:14 [in Coq.Sets.Relations_1_facts]
y:14 [in Coq.Structures.OrderedTypeAlt]
y:14 [in Coq.Sets.Relations_2_facts]
y:14 [in Coq.micromega.ZifySint63]
y:14 [in Coq.Structures.OrderedType]
y:14 [in Coq.Classes.SetoidClass]
y:14 [in Coq.micromega.ZifyUint63]
y:14 [in Coq.Reals.Ranalysis5]
y:14 [in Coq.Setoids.Setoid]
y:14 [in Coq.omega.PreOmega]
y:14 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:14 [in Coq.Sets.Classical_sets]
y:14 [in Coq.Reals.Rlogic]
y:14 [in Coq.Sets.Relations_1]
y:14 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:14 [in Coq.micromega.ZCoeff]
y:14 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:140 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:140 [in Coq.ssr.ssrfun]
y:140 [in Coq.Init.Datatypes]
y:1406 [in Coq.FSets.FMapAVL]
y:141 [in Coq.Logic.Eqdep_dec]
y:141 [in Coq.Sorting.PermutSetoid]
y:141 [in Coq.Reals.Rtrigo1]
y:141 [in Coq.Reals.Rsqrt_def]
y:141 [in Coq.Reals.RiemannInt]
y:141 [in Coq.ssr.ssrfun]
y:141 [in Coq.Reals.Rtopology]
y:141 [in Coq.FSets.FMapWeakList]
y:141 [in Coq.FSets.FSetCompat]
y:141 [in Coq.Structures.OrdersFacts]
y:1410 [in Coq.FSets.FMapAVL]
y:1415 [in Coq.FSets.FMapAVL]
y:142 [in Coq.FSets.FMapFacts]
y:142 [in Coq.Reals.Rtopology]
y:142 [in Coq.Init.Logic]
y:142 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:142 [in Coq.QArith.QArith_base]
y:1420 [in Coq.FSets.FMapAVL]
y:1423 [in Coq.FSets.FMapAVL]
y:1427 [in Coq.FSets.FMapAVL]
y:143 [in Coq.Reals.Rtrigo1]
y:143 [in Coq.Logic.EqdepFacts]
y:143 [in Coq.FSets.FSetPositive]
y:143 [in Coq.Reals.Rtopology]
y:143 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:143 [in Coq.Structures.OrdersFacts]
y:144 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:144 [in Coq.QArith.Qcanon]
y:145 [in Coq.Reals.Rtrigo1]
y:145 [in Coq.FSets.FMapFullAVL]
y:145 [in Coq.Structures.OrderedTypeEx]
y:145 [in Coq.Init.Datatypes]
y:145 [in Coq.setoid_ring.Ring_theory]
y:145 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:145 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:145 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:145 [in Coq.Structures.OrdersFacts]
y:1452 [in Coq.FSets.FMapAVL]
y:146 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:146 [in Coq.QArith.Qcanon]
y:146 [in Coq.FSets.FMapFacts]
y:146 [in Coq.Reals.Rtopology]
y:146 [in Coq.FSets.FMapWeakList]
y:146 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:146 [in Coq.Init.Logic]
y:147 [in Coq.Reals.Rtrigo1]
y:147 [in Coq.Logic.EqdepFacts]
y:147 [in Coq.Reals.Rtopology]
y:147 [in Coq.QArith.QArith_base]
y:147 [in Coq.FSets.FSetCompat]
y:147 [in Coq.Structures.OrdersFacts]
y:148 [in Coq.QArith.Qcanon]
y:148 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:148 [in Coq.MSets.MSetGenTree]
y:148 [in Coq.Reals.Ratan]
y:148 [in Coq.setoid_ring.Ring_theory]
y:148 [in Coq.FSets.FMapList]
y:148 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:148 [in Coq.Relations.Relation_Operators]
y:1487 [in Coq.FSets.FMapAVL]
y:149 [in Coq.Reals.Rtrigo1]
y:149 [in Coq.Reals.Ratan]
y:149 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:149 [in Coq.Reals.SeqProp]
y:149 [in Coq.Structures.OrdersFacts]
y:15 [in Coq.Relations.Operators_Properties]
y:15 [in Coq.Wellfounded.Well_Ordering]
y:15 [in Coq.Structures.OrdersEx]
y:15 [in Coq.QArith.Qcabs]
y:15 [in Coq.Arith.Bool_nat]
y:15 [in Coq.Numbers.Natural.Abstract.NDefOps]
y:15 [in Coq.Program.Subset]
y:15 [in Coq.QArith.Qreals]
y:15 [in Coq.Logic.ClassicalUniqueChoice]
y:15 [in Coq.Reals.Raxioms]
y:15 [in Coq.ZArith.Zbool]
y:15 [in Coq.Bool.BoolEq]
y:15 [in Coq.Reals.PSeries_reg]
y:15 [in Coq.Sets.Powerset_facts]
y:15 [in Coq.Numbers.Cyclic.Int63.Ring63]
y:15 [in Coq.Structures.OrdersTac]
y:15 [in Coq.Reals.R_sqr]
y:15 [in Coq.micromega.ZifyInst]
y:15 [in Coq.QArith.Qround]
y:15 [in Coq.Numbers.Cyclic.Int31.Ring31]
y:15 [in Coq.Structures.OrdersFacts]
y:150 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:150 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:150 [in Coq.Sorting.PermutSetoid]
y:150 [in Coq.FSets.FMapFacts]
y:150 [in Coq.Reals.Rtopology]
y:150 [in Coq.Init.Datatypes]
y:150 [in Coq.Init.Logic]
y:150 [in Coq.setoid_ring.Ncring]
y:150 [in Coq.Lists.SetoidList]
y:151 [in Coq.Reals.Rtrigo1]
y:151 [in Coq.FSets.FMapWeakList]
y:151 [in Coq.Reals.Ratan]
y:151 [in Coq.setoid_ring.Ring_theory]
y:151 [in Coq.Relations.Relation_Operators]
y:151 [in Coq.QArith.QArith_base]
y:152 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:152 [in Coq.setoid_ring.InitialRing]
y:152 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:152 [in Coq.FSets.FMapList]
y:152 [in Coq.Structures.OrdersFacts]
y:153 [in Coq.Reals.Rtrigo1]
y:153 [in Coq.MSets.MSetGenTree]
y:153 [in Coq.Reals.Ratan]
y:154 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:154 [in Coq.FSets.FMapFacts]
y:154 [in Coq.QArith.QArith_base]
y:155 [in Coq.Reals.Rtrigo1]
y:155 [in Coq.FSets.FMapFullAVL]
y:155 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:155 [in Coq.Structures.OrdersFacts]
y:156 [in Coq.Logic.Eqdep_dec]
y:156 [in Coq.Logic.EqdepFacts]
y:156 [in Coq.Lists.ListSet]
y:156 [in Coq.Relations.Relation_Operators]
y:156 [in Coq.Lists.SetoidList]
y:157 [in Coq.Reals.Rtrigo1]
y:157 [in Coq.FSets.FMapFacts]
y:157 [in Coq.Reals.Ratan]
y:157 [in Coq.setoid_ring.Ring_theory]
y:157 [in Coq.FSets.FMapList]
y:157 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:157 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:157 [in Coq.Structures.OrdersFacts]
y:158 [in Coq.Logic.EqdepFacts]
y:158 [in Coq.MSets.MSetGenTree]
y:158 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:159 [in Coq.Logic.Eqdep_dec]
y:159 [in Coq.FSets.FMapFullAVL]
y:159 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:159 [in Coq.Structures.OrdersFacts]
y:16 [in Coq.Structures.Orders]
y:16 [in Coq.Program.Wf]
y:16 [in Coq.Reals.Abstract.ConstructiveReals]
y:16 [in Coq.QArith.Qcanon]
y:16 [in Coq.nsatz.NsatzTactic]
y:16 [in Coq.Logic.Eqdep_dec]
y:16 [in Coq.Reals.Abstract.ConstructiveLUB]
y:16 [in Coq.Classes.RelationClasses]
y:16 [in Coq.Reals.Binomial]
y:16 [in Coq.Structures.OrdersAlt]
y:16 [in Coq.Program.Subset]
y:16 [in Coq.Reals.Rpower]
y:16 [in Coq.omega.OmegaLemmas]
y:16 [in Coq.ZArith.Int]
y:16 [in Coq.Strings.Ascii]
y:16 [in Coq.Sets.Permut]
y:16 [in Coq.omega.PreOmega]
y:16 [in Coq.Reals.RiemannInt_SF]
y:16 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:16 [in Coq.micromega.ZCoeff]
y:16 [in Coq.QArith.Qreduction]
y:16 [in Coq.Floats.FloatAxioms]
Y:16 [in Coq.Sets.Infinite_sets]
y:16 [in Coq.Reals.ClassicalConstructiveReals]
y:16 [in Coq.Sorting.Heap]
y:16 [in Coq.Logic.FinFun]
y:160 [in Coq.FSets.FSetBridge]
y:160 [in Coq.Logic.EqdepFacts]
y:160 [in Coq.FSets.FMapFacts]
y:160 [in Coq.setoid_ring.Ring_theory]
y:161 [in Coq.omega.OmegaLemmas]
y:161 [in Coq.MSets.MSetRBT]
y:161 [in Coq.Structures.OrdersFacts]
y:162 [in Coq.FSets.FMapAVL]
y:163 [in Coq.Logic.Eqdep_dec]
y:163 [in Coq.Logic.EqdepFacts]
y:163 [in Coq.FSets.FMapFacts]
y:163 [in Coq.MSets.MSetGenTree]
y:163 [in Coq.setoid_ring.Ring_theory]
y:164 [in Coq.Reals.Rfunctions]
y:164 [in Coq.Reals.MVT]
y:164 [in Coq.FSets.FMapFullAVL]
y:164 [in Coq.Reals.Ratan]
y:164 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:164 [in Coq.QArith.QArith_base]
y:165 [in Coq.Reals.MVT]
y:165 [in Coq.FSets.FSetInterface]
y:165 [in Coq.omega.OmegaLemmas]
y:165 [in Coq.Reals.Ratan]
y:166 [in Coq.Reals.MVT]
y:166 [in Coq.FSets.FMapFacts]
y:166 [in Coq.Reals.Rpower]
y:166 [in Coq.FSets.FMapAVL]
y:166 [in Coq.Reals.PSeries_reg]
y:166 [in Coq.QArith.QArith_base]
y:167 [in Coq.FSets.FSetBridge]
y:167 [in Coq.Reals.Rfunctions]
y:167 [in Coq.Reals.MVT]
y:167 [in Coq.ssr.ssrfun]
y:167 [in Coq.Reals.Ratan]
y:167 [in Coq.Reals.Ranalysis5]
y:167 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:168 [in Coq.Reals.MVT]
y:168 [in Coq.Reals.PSeries_reg]
y:168 [in Coq.setoid_ring.Ring_theory]
y:169 [in Coq.Reals.MVT]
y:169 [in Coq.FSets.FMapFacts]
y:169 [in Coq.FSets.FMapFullAVL]
y:169 [in Coq.omega.OmegaLemmas]
y:169 [in Coq.Reals.PSeries_reg]
y:169 [in Coq.Reals.Ratan]
y:169 [in Coq.QArith.QArith_base]
y:17 [in Coq.Program.Wf]
y:17 [in Coq.Relations.Operators_Properties]
y:17 [in Coq.Structures.OrdersLists]
y:17 [in Coq.Sets.Relations_3]
y:17 [in Coq.QArith.Qcabs]
y:17 [in Coq.Arith.Bool_nat]
y:17 [in Coq.ZArith.BinInt]
y:17 [in Coq.Reals.Abstract.ConstructivePower]
y:17 [in Coq.Logic.JMeq]
y:17 [in Coq.Numbers.Natural.Abstract.NDefOps]
y:17 [in Coq.Logic.ChoiceFacts]
y:17 [in Coq.Init.Wf]
y:17 [in Coq.QArith.Qreals]
y:17 [in Coq.Sets.Cpo]
y:17 [in Coq.Structures.OrderedTypeEx]
y:17 [in Coq.Structures.OrderedTypeAlt]
y:17 [in Coq.ZArith.Zbool]
y:17 [in Coq.Structures.Equalities]
y:17 [in Coq.Structures.OrderedType]
y:17 [in Coq.Sets.Powerset_facts]
y:17 [in Coq.Numbers.Cyclic.Int63.Ring63]
y:17 [in Coq.Sets.Relations_2]
y:17 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:17 [in Coq.Logic.Diaconescu]
y:17 [in Coq.Sets.Classical_sets]
y:17 [in Coq.Reals.RiemannInt_SF]
y:17 [in Coq.micromega.ZifyInst]
y:17 [in Coq.Reals.Cos_rel]
Y:17 [in Coq.Sets.Infinite_sets]
y:17 [in Coq.Numbers.Cyclic.Int31.Ring31]
y:17 [in Coq.Structures.OrdersFacts]
y:170 [in Coq.Reals.MVT]
y:170 [in Coq.MSets.MSetGenTree]
y:170 [in Coq.Reals.PSeries_reg]
y:170 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:170 [in Coq.ZArith.Znumtheory]
y:171 [in Coq.Reals.MVT]
y:171 [in Coq.FSets.FMapAVL]
y:172 [in Coq.FSets.FMapFullAVL]
y:172 [in Coq.QArith.QArith_base]
y:173 [in Coq.setoid_ring.Field_theory]
y:174 [in Coq.FSets.FSetBridge]
y:174 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:174 [in Coq.QArith.QArith_base]
y:175 [in Coq.MSets.MSetGenTree]
y:175 [in Coq.Reals.PSeries_reg]
y:176 [in Coq.FSets.FMapFullAVL]
y:176 [in Coq.ssr.ssrfun]
y:176 [in Coq.setoid_ring.Ncring]
y:176 [in Coq.QArith.QArith_base]
y:177 [in Coq.FSets.FSetBridge]
y:177 [in Coq.ssr.ssrfun]
y:177 [in Coq.Reals.Rpower]
y:177 [in Coq.Reals.PSeries_reg]
y:177 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:178 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:178 [in Coq.QArith.QArith_base]
y:179 [in Coq.Vectors.VectorSpec]
y:179 [in Coq.FSets.FMapAVL]
y:179 [in Coq.Vectors.Fin]
y:179 [in Coq.setoid_ring.Ncring]
y:18 [in Coq.Structures.Orders]
y:18 [in Coq.QArith.Qcanon]
y:18 [in Coq.nsatz.NsatzTactic]
y:18 [in Coq.FSets.FSetBridge]
y:18 [in Coq.Logic.EqdepFacts]
y:18 [in Coq.Strings.String]
y:18 [in Coq.Reals.R_sqrt]
y:18 [in Coq.Structures.OrdersAlt]
y:18 [in Coq.QArith.Qabs]
y:18 [in Coq.Reals.Rdefinitions]
y:18 [in Coq.Reals.Rpower]
y:18 [in Coq.omega.OmegaLemmas]
y:18 [in Coq.Sets.Partial_Order]
y:18 [in Coq.Structures.GenericMinMax]
y:18 [in Coq.Sets.Relations_2]
y:18 [in Coq.ssr.ssrunder]
y:18 [in Coq.Classes.DecidableClass]
y:18 [in Coq.ZArith.Znumtheory]
Y:18 [in Coq.Sets.Infinite_sets]
y:18 [in Coq.Relations.Relation_Operators]
y:18 [in Coq.Bool.DecBool]
y:18 [in Coq.Lists.SetoidList]
y:180 [in Coq.Reals.Abstract.ConstructiveReals]
y:180 [in Coq.FSets.FSetBridge]
y:180 [in Coq.FSets.FSetInterface]
y:180 [in Coq.Structures.OrderedType]
y:181 [in Coq.Sorting.Permutation]
y:182 [in Coq.setoid_ring.Ncring]
y:184 [in Coq.Logic.EqdepFacts]
y:184 [in Coq.micromega.RingMicromega]
y:184 [in Coq.FSets.FMapAVL]
y:184 [in Coq.Structures.OrderedType]
y:185 [in Coq.FSets.FMapFacts]
y:185 [in Coq.FSets.FSetInterface]
y:185 [in Coq.Init.Logic]
y:186 [in Coq.FSets.FSetBridge]
y:186 [in Coq.micromega.RingMicromega]
y:186 [in Coq.omega.OmegaLemmas]
y:186 [in Coq.Structures.GenericMinMax]
y:186 [in Coq.Reals.Ranalysis5]
y:186 [in Coq.setoid_ring.Ring_theory]
y:186 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:187 [in Coq.Reals.Rtopology]
y:187 [in Coq.setoid_ring.Ncring]
y:188 [in Coq.micromega.RingMicromega]
y:189 [in Coq.FSets.FSetBridge]
y:189 [in Coq.FSets.FMapAVL]
y:189 [in Coq.Reals.Rtopology]
y:189 [in Coq.Structures.GenericMinMax]
y:189 [in Coq.Reals.PSeries_reg]
y:189 [in Coq.QArith.QArith_base]
y:19 [in Coq.Relations.Operators_Properties]
y:19 [in Coq.Reals.Abstract.ConstructiveReals]
y:19 [in Coq.Logic.Eqdep_dec]
y:19 [in Coq.Sets.Constructive_sets]
y:19 [in Coq.QArith.Qcabs]
y:19 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
y:19 [in Coq.FSets.FMapFacts]
y:19 [in Coq.Wellfounded.Lexicographic_Product]
y:19 [in Coq.ZArith.Int]
y:19 [in Coq.micromega.QMicromega]
y:19 [in Coq.Structures.OrderedTypeAlt]
y:19 [in Coq.Classes.CRelationClasses]
y:19 [in Coq.micromega.ZifySint63]
y:19 [in Coq.Reals.Rbasic_fun]
y:19 [in Coq.Classes.SetoidClass]
y:19 [in Coq.Bool.BoolEq]
y:19 [in Coq.Logic.ProofIrrelevanceFacts]
y:19 [in Coq.Reals.RList]
y:19 [in Coq.Logic.Diaconescu]
Y:19 [in Coq.Sets.Classical_sets]
y:19 [in Coq.Program.Basics]
y:19 [in Coq.micromega.ZifyInst]
y:19 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:19 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:19 [in Coq.micromega.ZMicromega]
y:19 [in Coq.Floats.FloatAxioms]
y:19 [in Coq.Relations.Relation_Operators]
y:19 [in Coq.Numbers.Cyclic.Int31.Ring31]
y:19 [in Coq.Structures.OrdersFacts]
y:190 [in Coq.micromega.RingMicromega]
y:190 [in Coq.omega.OmegaLemmas]
y:191 [in Coq.Reals.Rpower]
y:191 [in Coq.Reals.Rtopology]
y:191 [in Coq.Reals.Ranalysis5]
y:191 [in Coq.Init.Logic]
y:191 [in Coq.QArith.QArith_base]
y:191 [in Coq.Lists.SetoidList]
y:191 [in Coq.FSets.FSetCompat]
y:192 [in Coq.FSets.FSetBridge]
y:192 [in Coq.Reals.PSeries_reg]
y:193 [in Coq.ssr.ssrfun]
y:193 [in Coq.Reals.Rtopology]
y:194 [in Coq.Reals.Rpower]
y:194 [in Coq.Bool.Bool]
y:194 [in Coq.omega.OmegaLemmas]
y:194 [in Coq.Structures.GenericMinMax]
y:194 [in Coq.Reals.Ranalysis5]
y:196 [in Coq.FSets.FSetBridge]
y:196 [in Coq.FSets.FMapAVL]
y:197 [in Coq.MSets.MSetList]
y:197 [in Coq.Reals.Rpower]
y:197 [in Coq.Reals.Ranalysis5]
y:197 [in Coq.FSets.FSetCompat]
y:198 [in Coq.FSets.FSetBridge]
y:198 [in Coq.FSets.FMapPositive]
y:199 [in Coq.FSets.FMapAVL]
y:199 [in Coq.omega.OmegaLemmas]
y:199 [in Coq.Structures.GenericMinMax]
y:199 [in Coq.Reals.Ranalysis5]
y:199 [in Coq.QArith.QArith_base]
y:2 [in Coq.Reals.Rderiv]
y:2 [in Coq.micromega.Ztac]
y:2 [in Coq.Structures.DecidableTypeEx]
y:2 [in Coq.Reals.Rminmax]
y:2 [in Coq.Structures.OrdersEx]
y:2 [in Coq.PArith.BinPos]
y:2 [in Coq.ZArith.BinInt]
y:2 [in Coq.ZArith.Zmax]
y:2 [in Coq.Numbers.NatInt.NZBase]
y:2 [in Coq.ZArith.Zmin]
y:2 [in Coq.FSets.FMapFacts]
y:2 [in Coq.Reals.Rsqrt_def]
y:2 [in Coq.MSets.MSetFacts]
y:2 [in Coq.QArith.Qfield]
y:2 [in Coq.NArith.BinNat]
y:2 [in Coq.Reals.Raxioms]
y:2 [in Coq.micromega.ZifyNat]
y:2 [in Coq.ZArith.Zbool]
y:2 [in Coq.Reals.Rbasic_fun]
y:2 [in Coq.NArith.NArith]
y:2 [in Coq.micromega.Fourier_util]
y:2 [in Coq.Numbers.Cyclic.Int63.Ring63]
y:2 [in Coq.Unicode.Utf8_core]
y:2 [in Coq.omega.PreOmega]
y:2 [in Coq.Numbers.Integer.Binary.ZBinary]
y:2 [in Coq.micromega.ZifyN]
y:2 [in Coq.FSets.FSetFacts]
y:2 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:2 [in Coq.Numbers.Cyclic.Int31.Ring31]
y:2 [in Coq.Structures.OrdersFacts]
y:2 [in Coq.Reals.Cos_plus]
y:20 [in Coq.Structures.Orders]
y:20 [in Coq.Program.Wf]
y:20 [in Coq.QArith.Qcanon]
y:20 [in Coq.Structures.OrdersLists]
y:20 [in Coq.Structures.OrdersEx]
y:20 [in Coq.Reals.R_sqrt]
y:20 [in Coq.Reals.Exp_prop]
y:20 [in Coq.Structures.OrdersAlt]
y:20 [in Coq.Reals.Rsqrt_def]
y:20 [in Coq.QArith.Qreals]
y:20 [in Coq.Reals.Abstract.ConstructiveAbs]
y:20 [in Coq.omega.OmegaLemmas]
y:20 [in Coq.Structures.OrderedTypeEx]
y:20 [in Coq.Structures.Equalities]
y:20 [in Coq.Strings.Ascii]
y:20 [in Coq.micromega.ZifyUint63]
y:20 [in Coq.Lists.ListSet]
y:20 [in Coq.Sets.Permut]
y:20 [in Coq.Sets.Powerset_facts]
y:20 [in Coq.Sets.Powerset_Classical_facts]
y:20 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:20 [in Coq.Sets.Multiset]
y:20 [in Coq.Classes.DecidableClass]
y:20 [in Coq.Sets.Image]
y:20 [in Coq.Sorting.Heap]
y:20 [in Coq.FSets.FSetCompat]
y:200 [in Coq.ssr.ssrfun]
y:200 [in Coq.Reals.Rpower]
y:201 [in Coq.FSets.FMapFullAVL]
y:201 [in Coq.Bool.Bool]
y:201 [in Coq.Reals.Ranalysis5]
y:201 [in Coq.Lists.SetoidList]
y:202 [in Coq.QArith.QArith_base]
y:203 [in Coq.Reals.Rfunctions]
y:203 [in Coq.Reals.Rtopology]
y:203 [in Coq.Reals.PSeries_reg]
y:203 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:203 [in Coq.FSets.FSetCompat]
y:204 [in Coq.Logic.EqdepFacts]
y:204 [in Coq.MSets.MSetList]
y:204 [in Coq.Reals.Ranalysis5]
y:204 [in Coq.micromega.ZMicromega]
y:204 [in Coq.Lists.SetoidList]
y:205 [in Coq.Reals.Rfunctions]
y:205 [in Coq.FSets.FMapWeakList]
y:205 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:206 [in Coq.Logic.ChoiceFacts]
y:206 [in Coq.omega.OmegaLemmas]
y:206 [in Coq.Structures.GenericMinMax]
y:206 [in Coq.Reals.PSeries_reg]
y:207 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:207 [in Coq.Reals.Rfunctions]
y:207 [in Coq.ssr.ssrfun]
y:207 [in Coq.MSets.MSetPositive]
y:207 [in Coq.Reals.Ranalysis5]
y:207 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:207 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:208 [in Coq.Logic.ChoiceFacts]
y:208 [in Coq.Reals.Rpower]
y:208 [in Coq.MSets.MSetRBT]
y:208 [in Coq.Reals.Rtopology]
y:208 [in Coq.Reals.PSeries_reg]
y:208 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:209 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:209 [in Coq.Reals.Rfunctions]
y:209 [in Coq.FSets.FMapWeakList]
y:209 [in Coq.Reals.Ranalysis5]
y:209 [in Coq.setoid_ring.Ring_theory]
y:209 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:209 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:21 [in Coq.Program.Wf]
y:21 [in Coq.Relations.Operators_Properties]
y:21 [in Coq.Logic.Eqdep_dec]
y:21 [in Coq.Sets.Constructive_sets]
y:21 [in Coq.Classes.RelationClasses]
y:21 [in Coq.Arith.Wf_nat]
y:21 [in Coq.Logic.JMeq]
y:21 [in Coq.Numbers.Natural.Abstract.NDefOps]
y:21 [in Coq.QArith.Qabs]
y:21 [in Coq.Reals.Rdefinitions]
y:21 [in Coq.micromega.QMicromega]
y:21 [in Coq.Sets.Partial_Order]
y:21 [in Coq.Structures.OrderedTypeAlt]
y:21 [in Coq.micromega.ZifySint63]
y:21 [in Coq.Structures.OrderedType]
y:21 [in Coq.Reals.Rbasic_fun]
y:21 [in Coq.Classes.SetoidDec]
y:21 [in Coq.Strings.Byte]
y:21 [in Coq.Lists.ListSet]
y:21 [in Coq.Reals.RList]
y:21 [in Coq.Logic.Diaconescu]
Y:21 [in Coq.Sets.Classical_sets]
y:21 [in Coq.Structures.OrdersTac]
y:21 [in Coq.micromega.ZifyInst]
y:21 [in Coq.micromega.ZMicromega]
y:21 [in Coq.micromega.ZCoeff]
y:21 [in Coq.Structures.OrdersFacts]
y:210 [in Coq.Reals.Rpower]
y:210 [in Coq.MSets.MSetPositive]
y:210 [in Coq.Reals.Rtopology]
y:210 [in Coq.Reals.PSeries_reg]
y:211 [in Coq.Structures.GenericMinMax]
y:211 [in Coq.Reals.PSeries_reg]
y:211 [in Coq.Reals.Ranalysis5]
y:211 [in Coq.setoid_ring.Ring_theory]
y:211 [in Coq.FSets.FMapList]
y:211 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:211 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:212 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:212 [in Coq.Reals.Rfunctions]
y:212 [in Coq.MSets.MSetPositive]
y:212 [in Coq.Reals.Rtopology]
y:212 [in Coq.setoid_ring.Ncring]
y:213 [in Coq.ssr.ssrfun]
y:213 [in Coq.MSets.MSetRBT]
y:213 [in Coq.Reals.PSeries_reg]
y:213 [in Coq.Reals.Ranalysis5]
y:213 [in Coq.setoid_ring.Ring_theory]
y:213 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:214 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:214 [in Coq.Reals.Ranalysis1]
y:214 [in Coq.Logic.ChoiceFacts]
y:214 [in Coq.Reals.Rtopology]
y:214 [in Coq.FSets.FMapWeakList]
y:214 [in Coq.setoid_ring.Ncring]
y:215 [in Coq.Reals.Ranalysis1]
y:215 [in Coq.ssr.ssrfun]
y:215 [in Coq.Reals.Rtopology]
y:215 [in Coq.Reals.Ranalysis5]
y:215 [in Coq.setoid_ring.Ring_theory]
y:215 [in Coq.FSets.FMapList]
y:215 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:215 [in Coq.Lists.SetoidList]
y:216 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:216 [in Coq.Reals.Ranalysis1]
y:216 [in Coq.Logic.ChoiceFacts]
y:216 [in Coq.Reals.Rtopology]
y:216 [in Coq.Structures.GenericMinMax]
y:216 [in Coq.setoid_ring.Ncring]
y:217 [in Coq.Reals.Ranalysis1]
y:217 [in Coq.ssr.ssrfun]
y:217 [in Coq.Reals.Ranalysis5]
y:217 [in Coq.setoid_ring.Ring_theory]
y:218 [in Coq.Reals.Ranalysis1]
y:218 [in Coq.Logic.ChoiceFacts]
y:218 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:218 [in Coq.Lists.SetoidList]
y:219 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:219 [in Coq.Reals.Ranalysis1]
y:219 [in Coq.ssr.ssrfun]
y:219 [in Coq.FSets.FMapWeakList]
y:219 [in Coq.Structures.GenericMinMax]
y:219 [in Coq.Reals.Ranalysis5]
y:22 [in Coq.Structures.Orders]
y:22 [in Coq.Reals.Abstract.ConstructiveReals]
y:22 [in Coq.QArith.Qcanon]
y:22 [in Coq.QArith.Qcabs]
y:22 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
y:22 [in Coq.FSets.FMapFacts]
y:22 [in Coq.Structures.OrdersAlt]
y:22 [in Coq.Logic.Hurkens]
y:22 [in Coq.Arith.Cantor]
y:22 [in Coq.Sets.Cpo]
y:22 [in Coq.Structures.OrderedTypeEx]
y:22 [in Coq.ZArith.Int]
y:22 [in Coq.Structures.Equalities]
y:22 [in Coq.Structures.GenericMinMax]
y:22 [in Coq.Reals.Rlimit]
y:22 [in Coq.micromega.ZifyUint63]
y:22 [in Coq.Sets.Powerset_facts]
Y:22 [in Coq.Sets.Powerset_Classical_facts]
y:22 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:22 [in Coq.Classes.DecidableClass]
y:22 [in Coq.Reals.R_sqr]
y:22 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:22 [in Coq.Floats.FloatAxioms]
y:22 [in Coq.Reals.Cos_rel]
Y:22 [in Coq.Sets.Infinite_sets]
y:220 [in Coq.setoid_ring.Ring_theory]
y:220 [in Coq.FSets.FMapList]
y:221 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:221 [in Coq.Reals.Ranalysis1]
y:221 [in Coq.Logic.ChoiceFacts]
y:221 [in Coq.Reals.Ranalysis5]
y:221 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:222 [in Coq.Structures.GenericMinMax]
y:223 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:223 [in Coq.Reals.Ranalysis1]
y:223 [in Coq.Reals.Ranalysis5]
y:224 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:224 [in Coq.setoid_ring.Ncring]
y:224 [in Coq.Lists.SetoidList]
y:225 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:225 [in Coq.Reals.Ranalysis1]
y:225 [in Coq.ssr.ssrfun]
y:225 [in Coq.Structures.GenericMinMax]
y:226 [in Coq.Logic.ChoiceFacts]
y:226 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:227 [in Coq.Reals.Ranalysis1]
y:227 [in Coq.ssr.ssrfun]
y:227 [in Coq.Reals.Ranalysis5]
y:227 [in Coq.setoid_ring.Ncring]
y:227 [in Coq.Lists.SetoidList]
y:228 [in Coq.Reals.Ranalysis1]
y:228 [in Coq.Logic.ChoiceFacts]
y:228 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:229 [in Coq.Reals.Ranalysis1]
y:229 [in Coq.ssr.ssrfun]
y:23 [in Coq.Relations.Operators_Properties]
y:23 [in Coq.Logic.Eqdep_dec]
y:23 [in Coq.Structures.OrdersLists]
y:23 [in Coq.ZArith.BinIntDef]
y:23 [in Coq.Reals.Rtrigo_reg]
Y:23 [in Coq.Sets.Finite_sets_facts]
y:23 [in Coq.Logic.EqdepFacts]
y:23 [in Coq.Reals.R_sqrt]
y:23 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:23 [in Coq.Reals.Abstract.ConstructivePower]
y:23 [in Coq.Wellfounded.Lexicographic_Product]
y:23 [in Coq.Init.Wf]
y:23 [in Coq.QArith.Qreals]
y:23 [in Coq.QArith.Qabs]
y:23 [in Coq.Reals.Abstract.ConstructiveAbs]
y:23 [in Coq.omega.OmegaLemmas]
y:23 [in Coq.Classes.CMorphisms]
y:23 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y:23 [in Coq.micromega.QMicromega]
y:23 [in Coq.Structures.OrderedTypeAlt]
y:23 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
y:23 [in Coq.Reals.Rbasic_fun]
y:23 [in Coq.Bool.BoolEq]
y:23 [in Coq.Lists.ListSet]
y:23 [in Coq.Sets.Multiset]
y:23 [in Coq.Logic.Diaconescu]
y:23 [in Coq.micromega.ZifyInst]
y:23 [in Coq.QArith.Qpower]
y:23 [in Coq.micromega.ZCoeff]
y:23 [in Coq.Structures.OrdersFacts]
y:230 [in Coq.Reals.Ranalysis1]
y:230 [in Coq.Logic.ChoiceFacts]
y:230 [in Coq.Lists.SetoidList]
y:231 [in Coq.Reals.Ranalysis1]
y:231 [in Coq.ssr.ssrfun]
y:231 [in Coq.Reals.Ranalysis5]
y:231 [in Coq.micromega.ZMicromega]
y:232 [in Coq.Logic.ChoiceFacts]
y:233 [in Coq.ssr.ssrfun]
y:234 [in Coq.MSets.MSetProperties]
y:234 [in Coq.ssr.ssrfun]
y:234 [in Coq.Reals.Ranalysis5]
y:234 [in Coq.FSets.FSetProperties]
y:235 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:235 [in Coq.Logic.EqdepFacts]
y:235 [in Coq.FSets.FSetPositive]
y:235 [in Coq.setoid_ring.Ring_theory]
y:236 [in Coq.MSets.MSetProperties]
y:236 [in Coq.Lists.List]
y:236 [in Coq.Logic.ChoiceFacts]
y:236 [in Coq.FSets.FMapFullAVL]
y:236 [in Coq.MSets.MSetRBT]
y:236 [in Coq.FSets.FSetProperties]
y:237 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:237 [in Coq.Logic.EqdepFacts]
y:237 [in Coq.Reals.Ranalysis5]
y:237 [in Coq.setoid_ring.Ring_theory]
y:237 [in Coq.QArith.QArith_base]
y:237 [in Coq.Lists.SetoidList]
y:238 [in Coq.Logic.ChoiceFacts]
y:239 [in Coq.FSets.FSetPositive]
y:239 [in Coq.QArith.QArith_base]
y:24 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:24 [in Coq.QArith.Qcabs]
y:24 [in Coq.Structures.OrdersAlt]
y:24 [in Coq.Reals.Rsqrt_def]
y:24 [in Coq.Arith.Cantor]
y:24 [in Coq.Structures.OrderedTypeEx]
y:24 [in Coq.Classes.EquivDec]
y:24 [in Coq.Structures.Equalities]
y:24 [in Coq.Structures.GenericMinMax]
y:24 [in Coq.micromega.ZifyUint63]
y:24 [in Coq.Sets.Permut]
y:24 [in Coq.Logic.ClassicalDescription]
y:24 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:24 [in Coq.Reals.RList]
y:24 [in Coq.Classes.DecidableClass]
y:24 [in Coq.Sets.Image]
y:24 [in Coq.Structures.OrdersTac]
y:24 [in Coq.Reals.R_sqr]
y:24 [in Coq.micromega.ZMicromega]
y:240 [in Coq.Logic.ChoiceFacts]
y:240 [in Coq.Reals.Ranalysis5]
y:240 [in Coq.ZArith.Znat]
y:240 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:241 [in Coq.ssr.ssrfun]
y:242 [in Coq.MSets.MSetProperties]
y:242 [in Coq.Logic.ChoiceFacts]
y:242 [in Coq.FSets.FSetPositive]
y:242 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:242 [in Coq.FSets.FSetProperties]
y:243 [in Coq.ssr.ssrfun]
y:243 [in Coq.Structures.GenericMinMax]
y:243 [in Coq.QArith.QArith_base]
y:244 [in Coq.MSets.MSetProperties]
y:244 [in Coq.Logic.ChoiceFacts]
y:244 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:244 [in Coq.FSets.FSetProperties]
y:245 [in Coq.Logic.ChoiceFacts]
y:245 [in Coq.ssr.ssrfun]
y:245 [in Coq.FSets.FSetPositive]
y:245 [in Coq.MSets.MSetRBT]
y:245 [in Coq.MSets.MSetGenTree]
y:245 [in Coq.Structures.GenericMinMax]
y:245 [in Coq.QArith.QArith_base]
y:246 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:247 [in Coq.Logic.ChoiceFacts]
y:247 [in Coq.ssr.ssrfun]
y:247 [in Coq.FSets.FSetPositive]
y:247 [in Coq.QArith.QArith_base]
y:248 [in Coq.Logic.ChoiceFacts]
y:248 [in Coq.Reals.Rtopology]
y:249 [in Coq.Logic.EqdepFacts]
y:249 [in Coq.ssr.ssrfun]
y:249 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:249 [in Coq.QArith.QArith_base]
y:25 [in Coq.Program.Wf]
y:25 [in Coq.Relations.Operators_Properties]
y:25 [in Coq.Reals.Rtrigo_reg]
y:25 [in Coq.Reals.MVT]
y:25 [in Coq.Reals.R_sqrt]
y:25 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:25 [in Coq.Arith.Wf_nat]
y:25 [in Coq.Logic.JMeq]
y:25 [in Coq.Numbers.Natural.Abstract.NDefOps]
y:25 [in Coq.Logic.ChoiceFacts]
y:25 [in Coq.Wellfounded.Lexicographic_Product]
y:25 [in Coq.QArith.Qabs]
y:25 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y:25 [in Coq.micromega.QMicromega]
y:25 [in Coq.Structures.OrderedTypeAlt]
y:25 [in Coq.micromega.ZifySint63]
y:25 [in Coq.Structures.OrderedType]
y:25 [in Coq.Reals.Rbasic_fun]
y:25 [in Coq.Reals.Rlimit]
y:25 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:25 [in Coq.micromega.ZCoeff]
y:25 [in Coq.QArith.Qreduction]
y:25 [in Coq.Reals.Cos_rel]
y:25 [in Coq.Structures.OrdersFacts]
y:250 [in Coq.Logic.ChoiceFacts]
y:250 [in Coq.ssr.ssrfun]
y:250 [in Coq.Reals.Ranalysis5]
y:251 [in Coq.FSets.FSetPositive]
y:251 [in Coq.Reals.Rtopology]
y:252 [in Coq.Logic.ChoiceFacts]
y:252 [in Coq.MSets.MSetGenTree]
y:253 [in Coq.Lists.List]
y:253 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:253 [in Coq.QArith.QArith_base]
y:253 [in Coq.Lists.SetoidList]
y:254 [in Coq.MSets.MSetProperties]
y:254 [in Coq.FSets.FSetInterface]
y:254 [in Coq.FSets.FSetPositive]
y:254 [in Coq.MSets.MSetRBT]
y:254 [in Coq.setoid_ring.Ring_theory]
y:254 [in Coq.FSets.FSetProperties]
y:254 [in Coq.Lists.SetoidList]
y:255 [in Coq.Reals.RIneq]
y:255 [in Coq.Init.Logic]
y:255 [in Coq.Lists.SetoidList]
y:256 [in Coq.Lists.List]
y:256 [in Coq.Logic.ChoiceFacts]
y:256 [in Coq.Reals.Rtopology]
y:256 [in Coq.Lists.SetoidList]
y:257 [in Coq.Logic.EqdepFacts]
y:257 [in Coq.MSets.MSetProperties]
y:257 [in Coq.Sorting.Permutation]
y:257 [in Coq.FSets.FSetPositive]
y:257 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:257 [in Coq.FSets.FSetProperties]
y:258 [in Coq.Logic.ChoiceFacts]
y:258 [in Coq.FSets.FSetInterface]
y:258 [in Coq.Reals.Ratan]
y:258 [in Coq.setoid_ring.Ring_theory]
y:259 [in Coq.Lists.List]
y:259 [in Coq.FSets.FMapFacts]
y:259 [in Coq.FSets.FSetPositive]
y:259 [in Coq.Reals.Rtopology]
y:259 [in Coq.Init.Logic]
y:259 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:26 [in Coq.Structures.Orders]
y:26 [in Coq.Program.Wf]
y:26 [in Coq.Reals.Abstract.ConstructiveReals]
y:26 [in Coq.setoid_ring.Ncring_initial]
y:26 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:26 [in Coq.Structures.OrdersEx]
y:26 [in Coq.QArith.Qcabs]
y:26 [in Coq.Classes.RelationClasses]
y:26 [in Coq.Reals.MVT]
y:26 [in Coq.Arith.Cantor]
y:26 [in Coq.Reals.Rdefinitions]
y:26 [in Coq.Sets.Cpo]
y:26 [in Coq.Arith.PeanoNat]
y:26 [in Coq.omega.OmegaLemmas]
y:26 [in Coq.Structures.OrderedTypeEx]
y:26 [in Coq.Structures.Equalities]
y:26 [in Coq.Bool.BoolEq]
y:26 [in Coq.Classes.SetoidDec]
y:26 [in Coq.Structures.GenericMinMax]
y:26 [in Coq.micromega.ZifyUint63]
y:26 [in Coq.Reals.PSeries_reg]
y:26 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:26 [in Coq.Classes.DecidableClass]
y:26 [in Coq.Reals.R_sqr]
y:26 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:26 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:26 [in Coq.Relations.Relation_Operators]
y:260 [in Coq.Logic.ClassicalFacts]
y:261 [in Coq.Logic.ChoiceFacts]
y:261 [in Coq.FSets.FSetPositive]
y:261 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:262 [in Coq.MSets.MSetRBT]
y:263 [in Coq.Init.Logic]
y:263 [in Coq.QArith.QArith_base]
y:264 [in Coq.MSets.MSetList]
y:264 [in Coq.Reals.Rtopology]
y:264 [in Coq.setoid_ring.Ring_theory]
y:264 [in Coq.Lists.SetoidList]
y:265 [in Coq.Logic.EqdepFacts]
y:265 [in Coq.setoid_ring.Ncring_tac]
y:265 [in Coq.ssr.ssrfun]
y:266 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:266 [in Coq.QArith.QArith_base]
y:267 [in Coq.MSets.MSetList]
y:267 [in Coq.Reals.Rtopology]
y:267 [in Coq.setoid_ring.Ring_theory]
y:267 [in Coq.Init.Logic]
y:268 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:268 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:269 [in Coq.QArith.QArith_base]
y:27 [in Coq.Relations.Operators_Properties]
y:27 [in Coq.Sets.Constructive_sets]
y:27 [in Coq.Reals.R_sqrt]
y:27 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:27 [in Coq.Structures.OrdersAlt]
y:27 [in Coq.ZArith.Wf_Z]
y:27 [in Coq.setoid_ring.InitialRing]
y:27 [in Coq.QArith.Qabs]
y:27 [in Coq.Structures.OrderedTypeAlt]
y:27 [in Coq.Classes.CRelationClasses]
y:27 [in Coq.micromega.ZifySint63]
y:27 [in Coq.Reals.Rbasic_fun]
y:27 [in Coq.Logic.HLevels]
y:27 [in Coq.Lists.ListSet]
y:27 [in Coq.Sets.Permut]
y:27 [in Coq.Reals.RList]
y:27 [in Coq.Sets.Image]
y:27 [in Coq.Structures.OrdersTac]
y:27 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:27 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:27 [in Coq.micromega.ZCoeff]
y:27 [in Coq.Floats.FloatAxioms]
y:27 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:27 [in Coq.Structures.OrdersFacts]
y:270 [in Coq.setoid_ring.Field_theory]
y:270 [in Coq.ssr.ssrfun]
y:270 [in Coq.MSets.MSetRBT]
y:270 [in Coq.setoid_ring.Ring_theory]
y:270 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:271 [in Coq.Logic.ChoiceFacts]
y:271 [in Coq.Sorting.Permutation]
y:271 [in Coq.Init.Logic]
y:272 [in Coq.Logic.EqdepFacts]
y:272 [in Coq.QArith.QArith_base]
y:273 [in Coq.Logic.ChoiceFacts]
y:273 [in Coq.setoid_ring.Field_theory]
y:273 [in Coq.ssr.ssrfun]
y:273 [in Coq.MSets.MSetGenTree]
y:273 [in Coq.setoid_ring.Ring_theory]
y:274 [in Coq.QArith.QArith_base]
y:274 [in Coq.Lists.SetoidList]
y:275 [in Coq.MSets.MSetRBT]
y:275 [in Coq.Init.Logic]
y:276 [in Coq.setoid_ring.Field_theory]
y:276 [in Coq.setoid_ring.Ring_theory]
y:276 [in Coq.micromega.ZMicromega]
y:276 [in Coq.QArith.QArith_base]
y:278 [in Coq.ssr.ssrfun]
y:278 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:278 [in Coq.QArith.QArith_base]
y:279 [in Coq.MSets.MSetPositive]
y:279 [in Coq.setoid_ring.Ring_theory]
y:28 [in Coq.setoid_ring.Ncring_initial]
y:28 [in Coq.ZArith.BinIntDef]
y:28 [in Coq.Reals.Rfunctions]
y:28 [in Coq.Lists.List]
y:28 [in Coq.Reals.Rsqrt_def]
y:28 [in Coq.Wellfounded.Lexicographic_Product]
y:28 [in Coq.Arith.PeanoNat]
y:28 [in Coq.Structures.Equalities]
y:28 [in Coq.Reals.Rtopology]
y:28 [in Coq.Structures.OrderedType]
y:28 [in Coq.Bool.BoolEq]
y:28 [in Coq.Structures.GenericMinMax]
y:28 [in Coq.Reals.Rlimit]
y:28 [in Coq.micromega.ZifyUint63]
y:28 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:28 [in Coq.Classes.DecidableClass]
y:28 [in Coq.Reals.R_sqr]
y:28 [in Coq.ZArith.Znumtheory]
y:28 [in Coq.Relations.Relation_Definitions]
y:28 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Y:28 [in Coq.Sets.Infinite_sets]
y:280 [in Coq.Lists.List]
y:280 [in Coq.Strings.Byte]
y:280 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:280 [in Coq.QArith.QArith_base]
y:281 [in Coq.Logic.ChoiceFacts]
y:281 [in Coq.ssr.ssrfun]
y:282 [in Coq.Reals.Ranalysis1]
y:282 [in Coq.setoid_ring.Field_theory]
y:282 [in Coq.Reals.Ratan]
y:282 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:282 [in Coq.QArith.QArith_base]
y:283 [in Coq.Reals.Ranalysis1]
y:283 [in Coq.Lists.List]
y:283 [in Coq.Logic.ChoiceFacts]
y:284 [in Coq.Reals.Ranalysis1]
y:284 [in Coq.QArith.QArith_base]
y:285 [in Coq.Reals.Ranalysis1]
y:285 [in Coq.MSets.MSetPositive]
y:286 [in Coq.Reals.Ranalysis1]
y:286 [in Coq.MSets.MSetRBT]
y:286 [in Coq.Reals.Ranalysis5]
y:286 [in Coq.setoid_ring.Ring_theory]
y:286 [in Coq.micromega.ZMicromega]
y:287 [in Coq.Reals.Ranalysis1]
y:288 [in Coq.Reals.Ranalysis1]
y:288 [in Coq.Reals.Rtopology]
y:288 [in Coq.Reals.Ranalysis5]
y:288 [in Coq.Init.Logic]
y:289 [in Coq.Reals.Ranalysis1]
y:289 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:29 [in Coq.Structures.Orders]
y:29 [in Coq.Relations.Operators_Properties]
y:29 [in Coq.Reals.Abstract.ConstructiveReals]
y:29 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:29 [in Coq.Reals.Ranalysis4]
y:29 [in Coq.micromega.RingMicromega]
y:29 [in Coq.Reals.Rfunctions]
y:29 [in Coq.Sets.Ensembles]
y:29 [in Coq.Reals.R_sqrt]
y:29 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:29 [in Coq.Arith.Wf_nat]
y:29 [in Coq.Logic.JMeq]
y:29 [in Coq.Wellfounded.Lexicographic_Product]
y:29 [in Coq.Init.Wf]
y:29 [in Coq.setoid_ring.InitialRing]
y:29 [in Coq.Reals.Rdefinitions]
y:29 [in Coq.Reals.Rpower]
y:29 [in Coq.Program.Equality]
y:29 [in Coq.omega.OmegaLemmas]
y:29 [in Coq.Structures.OrderedTypeEx]
y:29 [in Coq.micromega.QMicromega]
y:29 [in Coq.Sets.Relations_2_facts]
y:29 [in Coq.ZArith.ZArith_dec]
y:29 [in Coq.Logic.ClassicalDescription]
y:29 [in Coq.Sets.Image]
y:29 [in Coq.Reals.Rgeom]
y:29 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:29 [in Coq.Structures.OrdersFacts]
y:290 [in Coq.Reals.Ranalysis1]
y:290 [in Coq.Lists.List]
y:290 [in Coq.Strings.Byte]
y:290 [in Coq.Reals.Ranalysis5]
y:291 [in Coq.Reals.Ranalysis1]
y:291 [in Coq.Logic.ChoiceFacts]
y:291 [in Coq.MSets.MSetPositive]
y:291 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:293 [in Coq.MSets.MSetInterface]
y:293 [in Coq.Logic.ChoiceFacts]
y:293 [in Coq.Reals.Ranalysis5]
y:293 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:294 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:294 [in Coq.Lists.List]
y:294 [in Coq.Reals.Rtopology]
y:295 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:296 [in Coq.MSets.MSetInterface]
y:296 [in Coq.MSets.MSetPositive]
y:296 [in Coq.Reals.Ranalysis5]
y:296 [in Coq.QArith.QArith_base]
y:297 [in Coq.MSets.MSetRBT]
y:297 [in Coq.FSets.FMapPositive]
y:298 [in Coq.Reals.Rtopology]
y:298 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:299 [in Coq.Reals.Ranalysis5]
y:3 [in Coq.Sorting.PermutEq]
y:3 [in Coq.Logic.Eqdep_dec]
y:3 [in Coq.Structures.OrdersLists]
y:3 [in Coq.Arith.Bool_nat]
y:3 [in Coq.QArith.Qreals]
y:3 [in Coq.ZArith.Zwf]
y:3 [in Coq.Lists.ListDec]
y:3 [in Coq.Reals.Rpower]
y:3 [in Coq.Structures.GenericMinMax]
y:3 [in Coq.Lists.ListSet]
y:3 [in Coq.Reals.PSeries_reg]
y:3 [in Coq.micromega.RMicromega]
y:3 [in Coq.Reals.R_sqr]
y:3 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:3 [in Coq.Program.Utils]
y:30 [in Coq.Logic.EqdepFacts]
y:30 [in Coq.Reals.Rfunctions]
y:30 [in Coq.Structures.OrdersAlt]
y:30 [in Coq.QArith.Qabs]
y:30 [in Coq.Arith.PeanoNat]
y:30 [in Coq.Classes.CMorphisms]
y:30 [in Coq.Classes.EquivDec]
y:30 [in Coq.Sets.Uniset]
y:30 [in Coq.Structures.OrderedTypeAlt]
y:30 [in Coq.Reals.Rbasic_fun]
y:30 [in Coq.Structures.GenericMinMax]
y:30 [in Coq.micromega.ZifyUint63]
y:30 [in Coq.Sets.Multiset]
y:30 [in Coq.Classes.DecidableClass]
y:30 [in Coq.Structures.OrdersTac]
y:30 [in Coq.Reals.R_sqr]
y:30 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:30 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:30 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:30 [in Coq.Floats.FloatAxioms]
y:300 [in Coq.MSets.MSetInterface]
y:300 [in Coq.QArith.QArith_base]
y:302 [in Coq.Reals.Ranalysis1]
y:302 [in Coq.MSets.MSetInterface]
y:302 [in Coq.Lists.List]
y:302 [in Coq.Reals.Ranalysis5]
y:302 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:303 [in Coq.Reals.Ranalysis1]
y:304 [in Coq.Reals.Ranalysis1]
y:304 [in Coq.FSets.FSetBridge]
y:304 [in Coq.Reals.Rtopology]
y:304 [in Coq.QArith.QArith_base]
y:305 [in Coq.Reals.Ranalysis5]
y:305 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:307 [in Coq.MSets.MSetRBT]
y:307 [in Coq.MSets.MSetPositive]
y:307 [in Coq.QArith.QArith_base]
y:308 [in Coq.MSets.MSetInterface]
y:308 [in Coq.Logic.ChoiceFacts]
y:308 [in Coq.Init.Logic]
y:309 [in Coq.Reals.Ranalysis1]
y:31 [in Coq.Program.Wf]
y:31 [in Coq.Relations.Operators_Properties]
y:31 [in Coq.setoid_ring.Ncring_initial]
y:31 [in Coq.Reals.Ranalysis4]
y:31 [in Coq.Reals.Rfunctions]
y:31 [in Coq.Reals.R_sqrt]
y:31 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:31 [in Coq.ZArith.Wf_Z]
y:31 [in Coq.Reals.Rdefinitions]
y:31 [in Coq.Sets.Cpo]
y:31 [in Coq.Structures.OrderedTypeEx]
y:31 [in Coq.micromega.QMicromega]
y:31 [in Coq.Structures.Equalities]
y:31 [in Coq.Structures.OrderedType]
y:31 [in Coq.ZArith.ZArith_dec]
y:31 [in Coq.Classes.SetoidDec]
y:31 [in Coq.Reals.Rlimit]
y:31 [in Coq.Numbers.NatInt.NZOrder]
y:31 [in Coq.Logic.HLevels]
y:31 [in Coq.Sets.Permut]
y:31 [in Coq.Logic.ClassicalDescription]
y:31 [in Coq.Sets.Image]
y:310 [in Coq.Reals.Ranalysis1]
y:310 [in Coq.Logic.ChoiceFacts]
y:310 [in Coq.QArith.QArith_base]
y:311 [in Coq.Reals.Ranalysis1]
y:311 [in Coq.Arith.PeanoNat]
y:311 [in Coq.Reals.Ratan]
y:312 [in Coq.Reals.Abstract.ConstructiveReals]
y:313 [in Coq.MSets.MSetRBT]
y:313 [in Coq.MSets.MSetPositive]
y:313 [in Coq.QArith.QArith_base]
y:314 [in Coq.MSets.MSetInterface]
y:316 [in Coq.MSets.MSetRBT]
y:316 [in Coq.QArith.QArith_base]
y:317 [in Coq.Reals.Abstract.ConstructiveReals]
y:319 [in Coq.MSets.MSetPositive]
y:319 [in Coq.Init.Logic]
y:32 [in Coq.Structures.Orders]
y:32 [in Coq.Program.Wf]
y:32 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:32 [in Coq.Sets.Constructive_sets]
y:32 [in Coq.micromega.RingMicromega]
y:32 [in Coq.Reals.Rfunctions]
y:32 [in Coq.Structures.OrdersAlt]
y:32 [in Coq.Reals.Rsqrt_def]
y:32 [in Coq.Classes.CEquivalence]
y:32 [in Coq.Program.Equality]
y:32 [in Coq.Arith.PeanoNat]
y:32 [in Coq.omega.OmegaLemmas]
y:32 [in Coq.Classes.CRelationClasses]
y:32 [in Coq.Structures.GenericMinMax]
y:32 [in Coq.Sets.Multiset]
y:32 [in Coq.Classes.DecidableClass]
y:32 [in Coq.NArith.BinNatDef]
y:32 [in Coq.Reals.Rgeom]
y:32 [in Coq.PArith.BinPosDef]
y:32 [in Coq.Reals.R_sqr]
y:32 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:32 [in Coq.Numbers.Cyclic.Int63.Uint63]
Y:32 [in Coq.Sets.Infinite_sets]
y:32 [in Coq.Relations.Relation_Operators]
y:32 [in Coq.QArith.QArith_base]
y:32 [in Coq.Structures.OrdersFacts]
y:32 [in Coq.Classes.Equivalence]
y:320 [in Coq.QArith.QArith_base]
y:322 [in Coq.Reals.Rtopology]
y:322 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:323 [in Coq.QArith.QArith_base]
y:324 [in Coq.MSets.MSetRBT]
y:325 [in Coq.Logic.ChoiceFacts]
y:326 [in Coq.ssr.ssrbool]
y:326 [in Coq.QArith.QArith_base]
y:327 [in Coq.Logic.ChoiceFacts]
y:329 [in Coq.QArith.QArith_base]
y:33 [in Coq.Relations.Operators_Properties]
y:33 [in Coq.setoid_ring.Ncring_initial]
y:33 [in Coq.Reals.Ranalysis1]
y:33 [in Coq.ZArith.BinIntDef]
y:33 [in Coq.Reals.Ranalysis4]
y:33 [in Coq.Reals.Rfunctions]
y:33 [in Coq.Sets.Ensembles]
y:33 [in Coq.Reals.R_sqrt]
y:33 [in Coq.Arith.Wf_nat]
y:33 [in Coq.Classes.Morphisms]
y:33 [in Coq.Logic.JMeq]
y:33 [in Coq.setoid_ring.InitialRing]
y:33 [in Coq.Reals.Rpower]
y:33 [in Coq.Sets.Cpo]
y:33 [in Coq.Structures.OrderedTypeEx]
y:33 [in Coq.micromega.QMicromega]
y:33 [in Coq.Sets.Uniset]
y:33 [in Coq.Structures.Equalities]
y:33 [in Coq.Reals.Rbasic_fun]
y:33 [in Coq.Logic.Berardi]
y:33 [in Coq.setoid_ring.Ncring_polynom]
y:33 [in Coq.Reals.Ranalysis5]
y:33 [in Coq.Sets.Image]
y:33 [in Coq.Structures.OrdersTac]
y:33 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:33 [in Coq.micromega.ZMicromega]
y:33 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:33 [in Coq.Relations.Relation_Operators]
y:330 [in Coq.Reals.Rtopology]
y:330 [in Coq.Reals.RIneq]
y:331 [in Coq.ssr.ssrfun]
y:332 [in Coq.Reals.Rtopology]
y:332 [in Coq.QArith.QArith_base]
y:334 [in Coq.ssr.ssrbool]
y:334 [in Coq.Reals.Rtopology]
y:335 [in Coq.MSets.MSetRBT]
y:335 [in Coq.QArith.QArith_base]
y:336 [in Coq.Reals.Rtopology]
y:336 [in Coq.Init.Logic]
y:337 [in Coq.Reals.Rtopology]
y:338 [in Coq.ssr.ssrbool]
y:338 [in Coq.QArith.QArith_base]
y:339 [in Coq.MSets.MSetInterface]
y:339 [in Coq.Lists.List]
y:34 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:34 [in Coq.Logic.Eqdep_dec]
y:34 [in Coq.Logic.EqdepFacts]
y:34 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:34 [in Coq.Structures.OrdersAlt]
y:34 [in Coq.Init.Wf]
y:34 [in Coq.Reals.Rdefinitions]
y:34 [in Coq.Reals.Abstract.ConstructiveAbs]
y:34 [in Coq.Structures.OrderedType]
y:34 [in Coq.Classes.SetoidDec]
y:34 [in Coq.Numbers.NatInt.NZOrder]
y:34 [in Coq.Lists.ListSet]
y:34 [in Coq.Sets.Permut]
y:34 [in Coq.NArith.BinNatDef]
y:34 [in Coq.PArith.BinPosDef]
y:34 [in Coq.Reals.R_sqr]
y:34 [in Coq.Relations.Relation_Definitions]
y:34 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Y:34 [in Coq.Sets.Infinite_sets]
y:34 [in Coq.QArith.QArith_base]
y:34 [in Coq.Structures.OrdersFacts]
y:340 [in Coq.ssr.ssrfun]
y:340 [in Coq.Reals.Rtopology]
y:342 [in Coq.Lists.List]
y:342 [in Coq.Reals.Ranalysis5]
y:343 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:343 [in Coq.MSets.MSetInterface]
y:343 [in Coq.Reals.Rtopology]
y:343 [in Coq.micromega.ZMicromega]
y:344 [in Coq.Reals.Rtopology]
y:345 [in Coq.ssr.ssrfun]
y:346 [in Coq.Reals.Abstract.ConstructiveReals]
y:349 [in Coq.Reals.Abstract.ConstructiveReals]
y:349 [in Coq.ssr.ssrfun]
y:349 [in Coq.QArith.QArith_base]
y:35 [in Coq.Program.Wf]
y:35 [in Coq.Sorting.PermutEq]
y:35 [in Coq.Structures.OrdersEx]
Y:35 [in Coq.Sets.Finite_sets_facts]
y:35 [in Coq.FSets.FSetDecide]
y:35 [in Coq.Reals.Ranalysis4]
y:35 [in Coq.Reals.R_sqrt]
y:35 [in Coq.ZArith.Wf_Z]
y:35 [in Coq.Reals.Rsqrt_def]
y:35 [in Coq.Logic.ChoiceFacts]
y:35 [in Coq.MSets.MSetDecide]
y:35 [in Coq.setoid_ring.InitialRing]
y:35 [in Coq.Structures.DecidableType]
y:35 [in Coq.Reals.Rpower]
y:35 [in Coq.Structures.OrderedTypeEx]
y:35 [in Coq.Reals.Rbasic_fun]
y:35 [in Coq.Logic.Berardi]
y:35 [in Coq.Logic.HLevels]
y:35 [in Coq.Sets.Powerset_Classical_facts]
y:35 [in Coq.Reals.Ranalysis5]
y:35 [in Coq.ssr.ssrunder]
y:35 [in Coq.Sets.Multiset]
y:35 [in Coq.Sets.Image]
y:35 [in Coq.Floats.FloatAxioms]
y:35 [in Coq.Reals.ClassicalConstructiveReals]
y:350 [in Coq.ssr.ssrbool]
y:352 [in Coq.Reals.Abstract.ConstructiveReals]
y:352 [in Coq.ssr.ssrbool]
y:352 [in Coq.ssr.ssrfun]
y:352 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:353 [in Coq.MSets.MSetInterface]
y:353 [in Coq.QArith.QArith_base]
y:355 [in Coq.MSets.MSetGenTree]
y:355 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:356 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:356 [in Coq.Reals.Abstract.ConstructiveReals]
y:356 [in Coq.Init.Logic]
y:357 [in Coq.FSets.FMapWeakList]
y:357 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:357 [in Coq.QArith.QArith_base]
y:358 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:358 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:359 [in Coq.Lists.List]
y:359 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:36 [in Coq.Structures.Orders]
y:36 [in Coq.Program.Wf]
y:36 [in Coq.Relations.Operators_Properties]
y:36 [in Coq.QArith.Qcanon]
y:36 [in Coq.Reals.Ranalysis1]
y:36 [in Coq.Reals.Rtrigo1]
y:36 [in Coq.Reals.Ranalysis4]
y:36 [in Coq.micromega.RingMicromega]
y:36 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:36 [in Coq.Structures.OrdersAlt]
y:36 [in Coq.ZArith.Zeven]
y:36 [in Coq.Reals.Rdefinitions]
y:36 [in Coq.Reals.Abstract.ConstructiveAbs]
y:36 [in Coq.omega.OmegaLemmas]
y:36 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y:36 [in Coq.Classes.EquivDec]
y:36 [in Coq.Reals.NewtonInt]
y:36 [in Coq.ZArith.Zbool]
y:36 [in Coq.setoid_ring.Ncring_polynom]
y:36 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:36 [in Coq.Logic.Diaconescu]
y:36 [in Coq.Sets.Image]
y:36 [in Coq.Structures.OrdersTac]
y:36 [in Coq.Reals.R_sqr]
y:36 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:36 [in Coq.Numbers.Cyclic.Int63.Sint63]
Y:36 [in Coq.Sets.Infinite_sets]
y:360 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:360 [in Coq.Reals.Rtopology]
y:360 [in Coq.Reals.Ranalysis5]
y:361 [in Coq.ssr.ssrfun]
y:361 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:363 [in Coq.Reals.Rtopology]
y:364 [in Coq.Init.Logic]
y:364 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:366 [in Coq.ssr.ssrfun]
y:366 [in Coq.Reals.Rtopology]
y:366 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:367 [in Coq.FSets.FSetPositive]
y:368 [in Coq.Reals.Rtopology]
y:368 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:369 [in Coq.Init.Specif]
y:369 [in Coq.Init.Logic]
y:37 [in Coq.Reals.R_sqrt]
y:37 [in Coq.Logic.JMeq]
y:37 [in Coq.setoid_ring.InitialRing]
y:37 [in Coq.ZArith.Zeven]
y:37 [in Coq.Structures.OrderedTypeEx]
y:37 [in Coq.Reals.NewtonInt]
y:37 [in Coq.Classes.CRelationClasses]
y:37 [in Coq.Reals.Rtopology]
y:37 [in Coq.Structures.OrderedType]
y:37 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
y:37 [in Coq.Reals.Rbasic_fun]
y:37 [in Coq.Logic.Berardi]
y:37 [in Coq.Numbers.NatInt.NZOrder]
y:37 [in Coq.Sets.Permut]
y:37 [in Coq.Reals.Ranalysis5]
y:37 [in Coq.Sets.Image]
y:37 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:37 [in Coq.micromega.ZMicromega]
y:37 [in Coq.QArith.QArith_base]
y:37 [in Coq.Structures.OrdersFacts]
y:370 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:372 [in Coq.FSets.FMapList]
y:373 [in Coq.MSets.MSetRBT]
y:375 [in Coq.FSets.FSetPositive]
y:375 [in Coq.Reals.Rtopology]
y:376 [in Coq.Logic.ChoiceFacts]
y:376 [in Coq.Init.Logic]
y:377 [in Coq.Reals.Rtopology]
y:378 [in Coq.Reals.Rtopology]
y:378 [in Coq.Reals.Ranalysis5]
y:379 [in Coq.ssr.ssrfun]
y:38 [in Coq.Structures.Orders]
y:38 [in Coq.QArith.Qcanon]
y:38 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:38 [in Coq.Logic.Eqdep_dec]
Y:38 [in Coq.Sets.Finite_sets_facts]
Y:38 [in Coq.Sets.Constructive_sets]
y:38 [in Coq.Reals.Ranalysis4]
y:38 [in Coq.micromega.RingMicromega]
y:38 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:38 [in Coq.Structures.OrdersAlt]
y:38 [in Coq.Reals.Rsqrt_def]
y:38 [in Coq.Init.Wf]
y:38 [in Coq.Reals.Rdefinitions]
y:38 [in Coq.Reals.Abstract.ConstructiveAbs]
y:38 [in Coq.Program.Equality]
y:38 [in Coq.omega.OmegaLemmas]
y:38 [in Coq.Classes.EquivDec]
y:38 [in Coq.Reals.NewtonInt]
y:38 [in Coq.Logic.ClassicalDescription]
y:38 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:38 [in Coq.Sets.Multiset]
y:38 [in Coq.Sets.Image]
y:38 [in Coq.Reals.R_sqr]
y:38 [in Coq.Floats.FloatAxioms]
y:38 [in Coq.Reals.ClassicalConstructiveReals]
y:38 [in Coq.Relations.Relation_Operators]
y:380 [in Coq.MSets.MSetRBT]
y:380 [in Coq.Reals.Rtopology]
y:381 [in Coq.FSets.FSetPositive]
y:382 [in Coq.Logic.ChoiceFacts]
y:384 [in Coq.ssr.ssrfun]
y:384 [in Coq.Init.Logic]
y:385 [in Coq.Logic.ChoiceFacts]
y:386 [in Coq.FSets.FSetPositive]
y:386 [in Coq.MSets.MSetRBT]
y:386 [in Coq.Reals.Rtopology]
y:387 [in Coq.Reals.Ranalysis5]
y:388 [in Coq.Logic.ChoiceFacts]
y:389 [in Coq.ssr.ssrfun]
y:389 [in Coq.Reals.Rtopology]
y:39 [in Coq.Reals.Ranalysis1]
y:39 [in Coq.ZArith.BinIntDef]
y:39 [in Coq.Reals.R_sqrt]
y:39 [in Coq.ZArith.Wf_Z]
y:39 [in Coq.setoid_ring.InitialRing]
y:39 [in Coq.Structures.DecidableType]
y:39 [in Coq.Reals.Rpower]
y:39 [in Coq.Structures.OrderedTypeEx]
y:39 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y:39 [in Coq.Reals.NewtonInt]
y:39 [in Coq.Reals.Rbasic_fun]
y:39 [in Coq.Logic.Berardi]
y:39 [in Coq.Logic.HLevels]
y:39 [in Coq.Sets.Image]
y:39 [in Coq.Structures.OrdersTac]
y:39 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:39 [in Coq.QArith.QArith_base]
y:39 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:390 [in Coq.ssr.ssrbool]
y:391 [in Coq.Reals.Rtopology]
y:392 [in Coq.ssr.ssrbool]
y:392 [in Coq.Reals.Rtopology]
y:392 [in Coq.Init.Logic]
y:394 [in Coq.ssr.ssrbool]
y:395 [in Coq.Reals.Rtopology]
y:396 [in Coq.Reals.Rtopology]
y:396 [in Coq.Reals.Ranalysis5]
y:397 [in Coq.ZArith.BinInt]
y:397 [in Coq.ssr.ssrbool]
y:397 [in Coq.FSets.FSetPositive]
y:397 [in Coq.Reals.Rtopology]
y:398 [in Coq.ssr.ssrbool]
y:398 [in Coq.Reals.Rtopology]
y:399 [in Coq.Reals.Ranalysis1]
y:399 [in Coq.ZArith.BinInt]
y:399 [in Coq.Logic.ChoiceFacts]
y:399 [in Coq.Reals.Rtopology]
y:4 [in Coq.Structures.Orders]
y:4 [in Coq.Relations.Operators_Properties]
y:4 [in Coq.micromega.Ztac]
y:4 [in Coq.Reals.Abstract.ConstructiveReals]
y:4 [in Coq.Reals.Rminmax]
y:4 [in Coq.Structures.OrdersEx]
y:4 [in Coq.Sets.Relations_3]
y:4 [in Coq.PArith.BinPos]
y:4 [in Coq.ZArith.BinInt]
y:4 [in Coq.Structures.OrdersAlt]
y:4 [in Coq.NArith.BinNat]
y:4 [in Coq.Structures.OrderedTypeEx]
y:4 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y:4 [in Coq.Sets.Uniset]
y:4 [in Coq.Sets.Relations_1_facts]
y:4 [in Coq.Structures.OrderedTypeAlt]
y:4 [in Coq.ZArith.Zbool]
y:4 [in Coq.Strings.Byte]
y:4 [in Coq.Unicode.Utf8_core]
y:4 [in Coq.omega.PreOmega]
y:4 [in Coq.Sets.Relations_3_facts]
y:4 [in Coq.Vectors.VectorEq]
y:4 [in Coq.micromega.ZMicromega]
y:4 [in Coq.Structures.OrdersFacts]
y:40 [in Coq.Structures.Orders]
y:40 [in Coq.QArith.Qcanon]
y:40 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:40 [in Coq.Logic.EqdepFacts]
y:40 [in Coq.Reals.Ranalysis4]
y:40 [in Coq.micromega.RingMicromega]
y:40 [in Coq.Lists.List]
y:40 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:40 [in Coq.Classes.Morphisms]
y:40 [in Coq.Structures.OrdersAlt]
y:40 [in Coq.Reals.NewtonInt]
y:40 [in Coq.Sets.Uniset]
y:40 [in Coq.Structures.OrderedType]
y:40 [in Coq.Classes.SetoidDec]
y:40 [in Coq.Numbers.NatInt.NZOrder]
y:40 [in Coq.Lists.ListSet]
y:40 [in Coq.Sets.Permut]
y:40 [in Coq.Reals.Ranalysis5]
y:40 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:40 [in Coq.Reals.Rgeom]
y:40 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:40 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:400 [in Coq.ssr.ssrbool]
y:400 [in Coq.Init.Logic]
y:402 [in Coq.Reals.Ranalysis1]
y:402 [in Coq.Logic.ChoiceFacts]
y:402 [in Coq.Init.Logic]
y:403 [in Coq.Reals.Ranalysis1]
y:403 [in Coq.ssr.ssrbool]
y:403 [in Coq.FSets.FSetPositive]
y:403 [in Coq.FSets.FMapList]
y:404 [in Coq.Reals.Ranalysis1]
y:404 [in Coq.ssr.ssrbool]
y:405 [in Coq.Reals.Ranalysis1]
y:405 [in Coq.ZArith.BinInt]
y:406 [in Coq.Reals.Ranalysis1]
y:406 [in Coq.Logic.ChoiceFacts]
y:407 [in Coq.Reals.Ranalysis1]
y:407 [in Coq.ZArith.BinInt]
y:407 [in Coq.Lists.List]
y:407 [in Coq.Reals.Ranalysis5]
y:408 [in Coq.Reals.Ranalysis1]
y:409 [in Coq.Reals.Ranalysis1]
y:409 [in Coq.Logic.ChoiceFacts]
y:409 [in Coq.FSets.FSetPositive]
y:41 [in Coq.setoid_ring.Ncring_initial]
y:41 [in Coq.Logic.Eqdep_dec]
y:41 [in Coq.ZArith.BinIntDef]
y:41 [in Coq.Reals.Ranalysis4]
y:41 [in Coq.Logic.ClassicalEpsilon]
y:41 [in Coq.Reals.R_sqrt]
y:41 [in Coq.Logic.JMeq]
y:41 [in Coq.Logic.ChoiceFacts]
y:41 [in Coq.setoid_ring.InitialRing]
y:41 [in Coq.Reals.Rdefinitions]
y:41 [in Coq.Reals.Abstract.ConstructiveAbs]
y:41 [in Coq.Structures.OrderedTypeEx]
y:41 [in Coq.Reals.NewtonInt]
y:41 [in Coq.Reals.Rtopology]
y:41 [in Coq.ssr.ssrunder]
y:41 [in Coq.Sets.Multiset]
y:41 [in Coq.Reals.RList]
y:41 [in Coq.micromega.ZifyInst]
y:41 [in Coq.Floats.FloatAxioms]
y:41 [in Coq.Structures.OrdersFacts]
y:410 [in Coq.Reals.Ranalysis1]
y:410 [in Coq.ZArith.BinInt]
y:411 [in Coq.Reals.Ranalysis1]
y:412 [in Coq.Reals.Ranalysis1]
y:412 [in Coq.ZArith.BinInt]
y:412 [in Coq.Reals.Rtopology]
y:413 [in Coq.Reals.Ranalysis1]
y:414 [in Coq.Reals.Ranalysis1]
y:415 [in Coq.Lists.List]
y:416 [in Coq.ZArith.BinInt]
y:417 [in Coq.Reals.Ranalysis1]
y:418 [in Coq.ZArith.BinInt]
y:418 [in Coq.Reals.Rtopology]
y:42 [in Coq.Structures.Orders]
y:42 [in Coq.Relations.Operators_Properties]
y:42 [in Coq.Reals.Ranalysis1]
y:42 [in Coq.Logic.ConstructiveEpsilon]
y:42 [in Coq.Reals.Abstract.ConstructiveLUB]
y:42 [in Coq.Reals.Ranalysis4]
y:42 [in Coq.micromega.RingMicromega]
y:42 [in Coq.Reals.Rsqrt_def]
y:42 [in Coq.Init.Wf]
y:42 [in Coq.Reals.Rpower]
y:42 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y:42 [in Coq.Reals.NewtonInt]
y:42 [in Coq.Sets.Uniset]
y:42 [in Coq.Reals.Rbasic_fun]
y:42 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:42 [in Coq.Structures.OrdersTac]
y:42 [in Coq.PArith.BinPosDef]
y:42 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:42 [in Coq.QArith.QArith_base]
y:42 [in Coq.Lists.SetoidList]
y:420 [in Coq.Reals.Ranalysis1]
y:420 [in Coq.ZArith.BinInt]
y:422 [in Coq.Reals.Ranalysis1]
y:422 [in Coq.ZArith.BinInt]
y:423 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:424 [in Coq.ZArith.BinInt]
y:424 [in Coq.Reals.Rtopology]
y:424 [in Coq.Reals.Ranalysis5]
y:425 [in Coq.Reals.Ranalysis1]
y:425 [in Coq.Logic.ChoiceFacts]
y:426 [in Coq.ZArith.BinInt]
y:426 [in Coq.Reals.Rtopology]
y:427 [in Coq.Logic.ChoiceFacts]
y:429 [in Coq.ZArith.BinInt]
y:43 [in Coq.Program.Wf]
y:43 [in Coq.QArith.Qcanon]
y:43 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:43 [in Coq.ZArith.BinIntDef]
y:43 [in Coq.Reals.Abstract.ConstructiveLUB]
Y:43 [in Coq.Sets.Finite_sets_facts]
y:43 [in Coq.Reals.Ranalysis4]
y:43 [in Coq.Reals.R_sqrt]
y:43 [in Coq.Structures.OrdersAlt]
y:43 [in Coq.setoid_ring.InitialRing]
y:43 [in Coq.Reals.NewtonInt]
y:43 [in Coq.Reals.Rtopology]
y:43 [in Coq.Structures.OrderedType]
y:43 [in Coq.setoid_ring.Ncring_polynom]
y:43 [in Coq.Sets.Permut]
y:43 [in Coq.Sets.Powerset_facts]
y:43 [in Coq.Reals.Ranalysis5]
y:43 [in Coq.Logic.Diaconescu]
y:43 [in Coq.Reals.Rgeom]
y:43 [in Coq.Relations.Relation_Operators]
y:43 [in Coq.FSets.FSetCompat]
y:43 [in Coq.Structures.OrdersFacts]
y:431 [in Coq.Init.Logic]
y:44 [in Coq.Structures.Orders]
y:44 [in Coq.setoid_ring.Ncring_initial]
y:44 [in Coq.Logic.ConstructiveEpsilon]
y:44 [in Coq.Reals.Ranalysis4]
y:44 [in Coq.micromega.RingMicromega]
y:44 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:44 [in Coq.ZArith.Wf_Z]
y:44 [in Coq.Reals.Abstract.ConstructiveAbs]
y:44 [in Coq.Structures.OrderedTypeEx]
y:44 [in Coq.Reals.NewtonInt]
y:44 [in Coq.Logic.HLevels]
y:44 [in Coq.Sets.Multiset]
y:44 [in Coq.PArith.BinPosDef]
y:44 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:44 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:44 [in Coq.Floats.FloatAxioms]
y:44 [in Coq.QArith.QArith_base]
y:44 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:448 [in Coq.Reals.Ranalysis5]
Y:45 [in Coq.Logic.Decidable]
y:45 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:45 [in Coq.Reals.Ranalysis1]
y:45 [in Coq.ZArith.BinIntDef]
y:45 [in Coq.Lists.List]
y:45 [in Coq.Logic.JMeq]
y:45 [in Coq.Init.Wf]
y:45 [in Coq.setoid_ring.InitialRing]
y:45 [in Coq.Reals.Rpower]
y:45 [in Coq.Program.Equality]
y:45 [in Coq.Reals.NewtonInt]
y:45 [in Coq.Sets.Uniset]
y:45 [in Coq.Structures.OrderedType]
y:45 [in Coq.Reals.Rbasic_fun]
y:45 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:45 [in Coq.Reals.RList]
y:45 [in Coq.Logic.Diaconescu]
y:45 [in Coq.Structures.OrdersTac]
y:45 [in Coq.Reals.R_sqr]
y:45 [in Coq.Structures.OrdersFacts]
y:450 [in Coq.Reals.Ranalysis5]
y:451 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:452 [in Coq.Reals.Ranalysis5]
y:453 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:455 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:456 [in Coq.MSets.MSetRBT]
y:459 [in Coq.MSets.MSetRBT]
y:46 [in Coq.Structures.Orders]
y:46 [in Coq.setoid_ring.Ncring_initial]
y:46 [in Coq.QArith.Qcanon]
y:46 [in Coq.Logic.Eqdep_dec]
Y:46 [in Coq.Sets.Finite_sets_facts]
y:46 [in Coq.Logic.EqdepFacts]
y:46 [in Coq.Reals.R_sqrt]
y:46 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:46 [in Coq.FSets.FMapFacts]
y:46 [in Coq.Logic.ChoiceFacts]
y:46 [in Coq.Structures.OrderedTypeEx]
y:46 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y:46 [in Coq.Classes.EquivDec]
y:46 [in Coq.Reals.Ranalysis5]
y:46 [in Coq.Reals.Rgeom]
y:46 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:46 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:46 [in Coq.QArith.QArith_base]
y:46 [in Coq.FSets.FSetCompat]
y:464 [in Coq.setoid_ring.Field_theory]
y:47 [in Coq.Logic.Decidable]
y:47 [in Coq.Relations.Operators_Properties]
y:47 [in Coq.Logic.ConstructiveEpsilon]
y:47 [in Coq.ZArith.BinIntDef]
y:47 [in Coq.Reals.Rsqrt_def]
y:47 [in Coq.setoid_ring.InitialRing]
y:47 [in Coq.Structures.OrderedType]
y:47 [in Coq.Structures.GenericMinMax]
y:47 [in Coq.Sets.Permut]
y:47 [in Coq.Reals.RList]
y:47 [in Coq.Logic.Diaconescu]
y:47 [in Coq.Reals.R_sqr]
y:470 [in Coq.setoid_ring.Field_theory]
y:472 [in Coq.setoid_ring.Field_theory]
y:474 [in Coq.setoid_ring.Field_theory]
y:476 [in Coq.setoid_ring.Field_theory]
y:479 [in Coq.setoid_ring.Field_theory]
y:48 [in Coq.Structures.Orders]
y:48 [in Coq.QArith.Qcanon]
y:48 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Y:48 [in Coq.Sets.Finite_sets_facts]
y:48 [in Coq.Reals.Rtrigo1]
y:48 [in Coq.Reals.Ranalysis4]
y:48 [in Coq.ssr.ssrfun]
y:48 [in Coq.Reals.Rpower]
y:48 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y:48 [in Coq.Sets.Uniset]
y:48 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:48 [in Coq.Sets.Multiset]
y:48 [in Coq.Structures.OrdersTac]
y:48 [in Coq.Reals.Rgeom]
y:48 [in Coq.QArith.QArith_base]
y:48 [in Coq.Lists.SetoidList]
y:483 [in Coq.setoid_ring.Field_theory]
y:485 [in Coq.setoid_ring.Field_theory]
y:487 [in Coq.setoid_ring.Field_theory]
y:49 [in Coq.Logic.ConstructiveEpsilon]
Y:49 [in Coq.Sets.Finite_sets_facts]
y:49 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:49 [in Coq.ZArith.Wf_Z]
y:49 [in Coq.Structures.OrderedTypeEx]
y:49 [in Coq.Structures.OrderedType]
y:49 [in Coq.Logic.Diaconescu]
y:49 [in Coq.Reals.R_sqr]
y:49 [in Coq.FSets.FSetCompat]
y:493 [in Coq.MSets.MSetAVL]
y:497 [in Coq.PArith.BinPos]
y:498 [in Coq.MSets.MSetAVL]
y:499 [in Coq.PArith.BinPos]
y:5 [in Coq.Wellfounded.Union]
y:5 [in Coq.Structures.DecidableTypeEx]
y:5 [in Coq.setoid_ring.RealField]
y:5 [in Coq.Sorting.PermutSetoid]
y:5 [in Coq.Wellfounded.Transitive_Closure]
y:5 [in Coq.QArith.Qreals]
y:5 [in Coq.QArith.Qfield]
y:5 [in Coq.Reals.Rdefinitions]
y:5 [in Coq.Reals.Raxioms]
y:5 [in Coq.micromega.ZifyNat]
y:5 [in Coq.Logic.RelationalChoice]
y:5 [in Coq.Structures.OrderedType]
y:5 [in Coq.Classes.SetoidDec]
y:5 [in Coq.Sets.Permut]
y:5 [in Coq.Reals.Rtrigo_calc]
y:5 [in Coq.Sets.Multiset]
y:5 [in Coq.micromega.RMicromega]
y:5 [in Coq.PArith.BinPosDef]
y:5 [in Coq.Reals.R_sqr]
y:5 [in Coq.micromega.ZifyN]
y:5 [in Coq.micromega.ZifyInst]
y:5 [in Coq.Sets.Relations_1]
y:5 [in Coq.Relations.Relation_Definitions]
y:5 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:5 [in Coq.Sorting.Heap]
y:5 [in Coq.Logic.FinFun]
y:5 [in Coq.Reals.Cos_plus]
y:50 [in Coq.Logic.Decidable]
y:50 [in Coq.Structures.Orders]
y:50 [in Coq.Relations.Operators_Properties]
y:50 [in Coq.Reals.Rtrigo1]
y:50 [in Coq.Logic.JMeq]
y:50 [in Coq.Reals.Rpower]
y:50 [in Coq.Reals.PSeries_reg]
y:50 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:50 [in Coq.Relations.Relation_Operators]
y:50 [in Coq.QArith.QArith_base]
y:50 [in Coq.Structures.OrdersFacts]
y:50 [in Coq.Reals.Cos_plus]
y:501 [in Coq.PArith.BinPos]
y:501 [in Coq.Lists.List]
y:502 [in Coq.ssr.ssrbool]
y:503 [in Coq.PArith.BinPos]
y:505 [in Coq.Lists.List]
y:507 [in Coq.ssr.ssrbool]
y:508 [in Coq.Lists.List]
y:509 [in Coq.ssr.ssrbool]
y:509 [in Coq.MSets.MSetAVL]
y:51 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:51 [in Coq.Reals.Ranalysis4]
y:51 [in Coq.FSets.FMapFacts]
y:51 [in Coq.Reals.Rsqrt_def]
y:51 [in Coq.ssr.ssrfun]
y:51 [in Coq.Sets.Uniset]
y:51 [in Coq.Reals.Ranalysis5]
y:51 [in Coq.Sets.Multiset]
y:51 [in Coq.Logic.Diaconescu]
y:51 [in Coq.Structures.OrdersTac]
y:51 [in Coq.Reals.R_sqr]
y:51 [in Coq.Sorting.Mergesort]
y:51 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:515 [in Coq.ssr.ssrbool]
y:515 [in Coq.MSets.MSetRBT]
y:517 [in Coq.Lists.List]
y:519 [in Coq.ZArith.BinInt]
y:519 [in Coq.MSets.MSetAVL]
y:52 [in Coq.Logic.Decidable]
y:52 [in Coq.Structures.Orders]
y:52 [in Coq.Relations.Operators_Properties]
y:52 [in Coq.Logic.EqdepFacts]
y:52 [in Coq.Reals.Ranalysis4]
y:52 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:52 [in Coq.Init.Wf]
y:52 [in Coq.Structures.OrderedTypeEx]
y:52 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y:52 [in Coq.Structures.OrderedType]
y:52 [in Coq.Sets.Powerset_facts]
y:52 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:52 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:52 [in Coq.QArith.QArith_base]
y:52 [in Coq.FSets.FSetCompat]
y:52 [in Coq.Structures.OrdersFacts]
y:521 [in Coq.micromega.Tauto]
y:522 [in Coq.MSets.MSetAVL]
y:524 [in Coq.ssr.ssrbool]
y:526 [in Coq.micromega.Tauto]
y:529 [in Coq.FSets.FMapWeakList]
y:53 [in Coq.Reals.Rderiv]
y:53 [in Coq.Reals.Abstract.ConstructiveReals]
y:53 [in Coq.QArith.Qcanon]
y:53 [in Coq.Logic.Eqdep_dec]
y:53 [in Coq.Reals.Rtrigo1]
y:53 [in Coq.FSets.FSetDecide]
y:53 [in Coq.Reals.Ranalysis4]
y:53 [in Coq.MSets.MSetDecide]
y:53 [in Coq.ssr.ssrfun]
y:53 [in Coq.Reals.Rpower]
y:53 [in Coq.FSets.FSetPositive]
y:53 [in Coq.MSets.MSetPositive]
y:53 [in Coq.Reals.Ranalysis5]
y:53 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:53 [in Coq.Reals.R_sqr]
y:53 [in Coq.micromega.ZifyInst]
y:53 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:53 [in Coq.Relations.Relation_Operators]
y:530 [in Coq.MSets.MSetAVL]
y:533 [in Coq.ssr.ssrbool]
y:539 [in Coq.PArith.BinPos]
y:539 [in Coq.ssr.ssrbool]
y:54 [in Coq.Structures.Orders]
y:54 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:54 [in Coq.Logic.JMeq]
y:54 [in Coq.Logic.ChoiceFacts]
y:54 [in Coq.Structures.OrderedTypeEx]
y:54 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y:54 [in Coq.ZArith.Zpower]
y:54 [in Coq.Sets.Uniset]
y:54 [in Coq.Logic.Diaconescu]
y:54 [in Coq.Structures.OrdersTac]
y:54 [in Coq.Reals.ClassicalConstructiveReals]
y:54 [in Coq.QArith.QArith_base]
y:54 [in Coq.Logic.FinFun]
y:54 [in Coq.Structures.OrdersFacts]
y:540 [in Coq.ssr.ssrbool]
y:541 [in Coq.Init.Specif]
y:541 [in Coq.MSets.MSetAVL]
y:542 [in Coq.FSets.FMapWeakList]
y:543 [in Coq.MSets.MSetRBT]
y:544 [in Coq.ssr.ssrbool]
y:546 [in Coq.ssr.ssrbool]
y:548 [in Coq.ssr.ssrbool]
y:549 [in Coq.Strings.Byte]
y:549 [in Coq.FSets.FMapList]
y:55 [in Coq.Relations.Operators_Properties]
y:55 [in Coq.Reals.Ranalysis4]
y:55 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:55 [in Coq.FSets.FMapFacts]
y:55 [in Coq.ssr.ssrfun]
y:55 [in Coq.ZArith.Zbool]
y:55 [in Coq.Structures.OrderedType]
y:55 [in Coq.Sets.Powerset_facts]
y:55 [in Coq.Reals.Ranalysis5]
y:55 [in Coq.Sets.Multiset]
y:55 [in Coq.Reals.R_sqr]
y:55 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:55 [in Coq.Relations.Relation_Operators]
y:55 [in Coq.FSets.FSetCompat]
y:552 [in Coq.ssr.ssrbool]
y:552 [in Coq.FSets.FMapWeakList]
y:554 [in Coq.ssr.ssrbool]
y:555 [in Coq.MSets.MSetAVL]
y:556 [in Coq.FSets.FMapWeakList]
y:558 [in Coq.ssr.ssrbool]
y:56 [in Coq.Structures.Orders]
y:56 [in Coq.Reals.Rsqrt_def]
y:56 [in Coq.Bool.Bool]
y:56 [in Coq.Structures.OrderedTypeEx]
y:56 [in Coq.Classes.EquivDec]
y:56 [in Coq.Reals.Rbasic_fun]
y:56 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:56 [in Coq.QArith.QArith_base]
y:561 [in Coq.FSets.FMapWeakList]
y:562 [in Coq.FSets.FMapList]
y:563 [in Coq.ssr.ssrbool]
y:565 [in Coq.MSets.MSetAVL]
y:566 [in Coq.ssr.ssrbool]
y:566 [in Coq.FSets.FMapWeakList]
y:568 [in Coq.ssr.ssrbool]
y:569 [in Coq.FSets.FMapWeakList]
y:57 [in Coq.Program.Wf]
y:57 [in Coq.Relations.Operators_Properties]
y:57 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:57 [in Coq.Logic.Eqdep_dec]
y:57 [in Coq.FSets.FSetDecide]
y:57 [in Coq.Reals.Ranalysis4]
y:57 [in Coq.Classes.RelationClasses]
y:57 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:57 [in Coq.MSets.MSetDecide]
y:57 [in Coq.ssr.ssrfun]
y:57 [in Coq.Reals.Rpower]
y:57 [in Coq.ZArith.Zpower]
y:57 [in Coq.ZArith.Zbool]
y:57 [in Coq.Logic.Diaconescu]
y:57 [in Coq.Structures.OrdersTac]
y:57 [in Coq.Reals.R_sqr]
y:57 [in Coq.Structures.OrdersFacts]
y:572 [in Coq.MSets.MSetAVL]
y:572 [in Coq.FSets.FMapList]
y:573 [in Coq.FSets.FMapWeakList]
y:575 [in Coq.MSets.MSetRBT]
y:576 [in Coq.FSets.FMapList]
y:58 [in Coq.Program.Wf]
y:58 [in Coq.setoid_ring.Ncring_initial]
y:58 [in Coq.Logic.EqdepFacts]
y:58 [in Coq.Reals.Ranalysis4]
y:58 [in Coq.Lists.List]
y:58 [in Coq.Sets.Uniset]
y:58 [in Coq.Structures.OrderedType]
y:58 [in Coq.Reals.Rbasic_fun]
y:58 [in Coq.Reals.PSeries_reg]
y:58 [in Coq.Reals.Ranalysis5]
y:58 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:58 [in Coq.micromega.RMicromega]
y:58 [in Coq.micromega.ZifyInst]
y:58 [in Coq.QArith.QArith_base]
y:58 [in Coq.FSets.FSetCompat]
y:581 [in Coq.FSets.FMapList]
y:582 [in Coq.MSets.MSetAVL]
y:585 [in Coq.ssr.ssrbool]
y:585 [in Coq.Reals.RIneq]
y:586 [in Coq.MSets.MSetAVL]
y:586 [in Coq.FSets.FMapList]
y:587 [in Coq.Reals.RIneq]
y:588 [in Coq.ssr.ssrbool]
y:589 [in Coq.Reals.RIneq]
y:589 [in Coq.FSets.FMapList]
y:59 [in Coq.Relations.Operators_Properties]
y:59 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:59 [in Coq.Reals.Ranalysis1]
y:59 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:59 [in Coq.Logic.JMeq]
y:59 [in Coq.ZArith.Zbool]
y:59 [in Coq.Sets.Multiset]
y:59 [in Coq.Structures.OrdersTac]
y:59 [in Coq.Reals.R_sqr]
y:59 [in Coq.Lists.SetoidList]
y:591 [in Coq.ssr.ssrbool]
y:591 [in Coq.Reals.RIneq]
y:593 [in Coq.Reals.RIneq]
y:593 [in Coq.FSets.FMapList]
y:594 [in Coq.Lists.List]
y:594 [in Coq.MSets.MSetAVL]
y:595 [in Coq.ssr.ssrbool]
y:595 [in Coq.MSets.MSetAVL]
y:596 [in Coq.MSets.MSetAVL]
y:597 [in Coq.Lists.List]
y:597 [in Coq.MSets.MSetAVL]
y:597 [in Coq.Reals.RIneq]
y:599 [in Coq.ssr.ssrbool]
y:6 [in Coq.Program.Wf]
y:6 [in Coq.micromega.Ztac]
y:6 [in Coq.Reals.Abstract.ConstructiveReals]
y:6 [in Coq.Wellfounded.Inverse_Image]
y:6 [in Coq.Reals.Rminmax]
y:6 [in Coq.PArith.BinPos]
y:6 [in Coq.MSets.MSetProperties]
y:6 [in Coq.ZArith.BinInt]
y:6 [in Coq.Numbers.NatInt.NZBase]
y:6 [in Coq.Reals.Exp_prop]
y:6 [in Coq.Reals.Rsqrt_def]
y:6 [in Coq.Logic.ChoiceFacts]
y:6 [in Coq.Init.Wf]
y:6 [in Coq.Relations.Relations]
y:6 [in Coq.NArith.BinNat]
y:6 [in Coq.Classes.EquivDec]
y:6 [in Coq.Logic.ClassicalUniqueChoice]
y:6 [in Coq.ZArith.Zbool]
y:6 [in Coq.Structures.Equalities]
y:6 [in Coq.Reals.Rtopology]
y:6 [in Coq.ZArith.Zpow_alt]
y:6 [in Coq.Bool.BoolEq]
y:6 [in Coq.micromega.ZifyComparison]
y:6 [in Coq.Structures.GenericMinMax]
y:6 [in Coq.Strings.Byte]
y:6 [in Coq.micromega.Fourier_util]
y:6 [in Coq.Logic.HLevels]
y:6 [in Coq.Unicode.Utf8_core]
y:6 [in Coq.Reals.Ranalysis5]
y:6 [in Coq.Sets.Relations_2]
y:6 [in Coq.omega.PreOmega]
y:6 [in Coq.Logic.Adjointification]
y:6 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:6 [in Coq.FSets.FSetProperties]
y:6 [in Coq.Reals.ClassicalConstructiveReals]
y:6 [in Coq.Relations.Relation_Operators]
y:6 [in Coq.Bool.DecBool]
y:6 [in Coq.Lists.SetoidList]
y:6 [in Coq.Structures.OrdersFacts]
y:60 [in Coq.Reals.Ranalysis4]
y:60 [in Coq.FSets.FMapFacts]
y:60 [in Coq.Reals.Rsqrt_def]
y:60 [in Coq.Init.Wf]
y:60 [in Coq.Reals.Rdefinitions]
y:60 [in Coq.Reals.Rpower]
y:60 [in Coq.Reals.Rbasic_fun]
y:60 [in Coq.Sets.Powerset_facts]
y:60 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:60 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:60 [in Coq.Relations.Relation_Operators]
y:60 [in Coq.QArith.QArith_base]
y:60 [in Coq.Structures.OrdersFacts]
y:602 [in Coq.Lists.List]
y:603 [in Coq.ssr.ssrbool]
y:605 [in Coq.PArith.BinPos]
y:608 [in Coq.FSets.FMapFacts]
y:608 [in Coq.MSets.MSetAVL]
y:61 [in Coq.Relations.Operators_Properties]
y:61 [in Coq.Logic.Eqdep_dec]
y:61 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:61 [in Coq.Sets.Uniset]
y:61 [in Coq.ZArith.Zbool]
y:61 [in Coq.Structures.OrderedType]
y:61 [in Coq.Reals.Ranalysis5]
y:61 [in Coq.Structures.OrdersTac]
y:61 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:61 [in Coq.micromega.Tauto]
y:61 [in Coq.Lists.SetoidList]
y:611 [in Coq.FSets.FMapFacts]
y:611 [in Coq.MSets.MSetAVL]
y:612 [in Coq.ssr.ssrbool]
y:618 [in Coq.FSets.FMapWeakList]
y:62 [in Coq.Program.Wf]
y:62 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:62 [in Coq.Reals.Ranalysis4]
y:62 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
y:62 [in Coq.Lists.List]
y:62 [in Coq.Reals.Rpower]
y:62 [in Coq.Reals.Rbasic_fun]
y:62 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:62 [in Coq.Reals.R_sqr]
y:62 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:62 [in Coq.QArith.QArith_base]
y:62 [in Coq.Logic.FinFun]
y:622 [in Coq.MSets.MSetAVL]
y:625 [in Coq.MSets.MSetAVL]
y:63 [in Coq.Relations.Operators_Properties]
y:63 [in Coq.Reals.Rtrigo1]
y:63 [in Coq.FSets.FSetDecide]
y:63 [in Coq.Classes.RelationClasses]
y:63 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:63 [in Coq.MSets.MSetDecide]
y:63 [in Coq.setoid_ring.InitialRing]
y:63 [in Coq.Structures.OrderedTypeEx]
y:63 [in Coq.Structures.OrdersTac]
y:63 [in Coq.Logic.FinFun]
y:63 [in Coq.Structures.OrdersFacts]
y:634 [in Coq.Lists.List]
y:634 [in Coq.MSets.MSetAVL]
y:638 [in Coq.Lists.List]
y:639 [in Coq.FSets.FMapList]
y:64 [in Coq.QArith.Qcanon]
y:64 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:64 [in Coq.Logic.EqdepFacts]
y:64 [in Coq.FSets.FMapFacts]
y:64 [in Coq.Reals.Rsqrt_def]
y:64 [in Coq.Structures.OrderedType]
y:64 [in Coq.Reals.Rbasic_fun]
y:64 [in Coq.Sets.Powerset_facts]
y:64 [in Coq.Reals.Ranalysis5]
y:64 [in Coq.Sets.Multiset]
y:64 [in Coq.Sets.Image]
y:64 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:64 [in Coq.Lists.SetoidList]
y:644 [in Coq.Init.Logic]
y:645 [in Coq.Lists.List]
y:65 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:65 [in Coq.setoid_ring.InitialRing]
y:65 [in Coq.Reals.Rpower]
y:65 [in Coq.Sets.Uniset]
y:65 [in Coq.micromega.RMicromega]
y:65 [in Coq.Reals.R_sqr]
y:65 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:65 [in Coq.Relations.Relation_Operators]
y:65 [in Coq.QArith.QArith_base]
y:650 [in Coq.Lists.List]
y:652 [in Coq.Lists.List]
y:658 [in Coq.Lists.List]
y:66 [in Coq.Program.Wf]
y:66 [in Coq.Relations.Operators_Properties]
y:66 [in Coq.Reals.Abstract.ConstructiveReals]
y:66 [in Coq.QArith.Qcanon]
y:66 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:66 [in Coq.Logic.JMeq]
y:66 [in Coq.Logic.ChoiceFacts]
y:66 [in Coq.Structures.OrderedTypeEx]
y:66 [in Coq.Reals.Raxioms]
y:66 [in Coq.Classes.CRelationClasses]
y:66 [in Coq.Reals.Rbasic_fun]
y:66 [in Coq.Reals.PSeries_reg]
y:66 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:66 [in Coq.Structures.OrdersFacts]
y:662 [in Coq.Lists.List]
y:667 [in Coq.ssr.ssrbool]
y:669 [in Coq.ssr.ssrbool]
y:67 [in Coq.Reals.Ranalysis4]
y:67 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:67 [in Coq.Init.Wf]
y:67 [in Coq.setoid_ring.InitialRing]
y:67 [in Coq.Reals.Rtopology]
y:67 [in Coq.Structures.OrderedType]
y:67 [in Coq.setoid_ring.Ring_theory]
y:67 [in Coq.micromega.RMicromega]
y:67 [in Coq.QArith.QArith_base]
y:671 [in Coq.ssr.ssrbool]
y:673 [in Coq.ssr.ssrbool]
y:68 [in Coq.Relations.Operators_Properties]
y:68 [in Coq.FSets.FSetDecide]
y:68 [in Coq.Reals.Ranalysis4]
y:68 [in Coq.FSets.FMapFacts]
y:68 [in Coq.Logic.ChoiceFacts]
y:68 [in Coq.FSets.FMapInterface]
y:68 [in Coq.MSets.MSetDecide]
y:68 [in Coq.Classes.EquivDec]
y:68 [in Coq.Reals.Raxioms]
y:68 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:69 [in Coq.QArith.Qcanon]
y:69 [in Coq.Logic.Eqdep_dec]
y:69 [in Coq.micromega.ZifyClasses]
y:69 [in Coq.Reals.Ranalysis4]
y:69 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:69 [in Coq.Sets.Uniset]
y:69 [in Coq.Structures.OrderedType]
y:69 [in Coq.Reals.Rbasic_fun]
y:69 [in Coq.Reals.Ranalysis5]
y:69 [in Coq.micromega.RMicromega]
y:69 [in Coq.PArith.BinPosDef]
y:69 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:69 [in Coq.Structures.OrdersFacts]
y:7 [in Coq.Program.Wf]
y:7 [in Coq.Relations.Operators_Properties]
y:7 [in Coq.Structures.DecidableTypeEx]
y:7 [in Coq.Wellfounded.Inverse_Image]
y:7 [in Coq.Sets.Relations_3]
y:7 [in Coq.Arith.Bool_nat]
y:7 [in Coq.Logic.SetoidChoice]
y:7 [in Coq.Reals.R_sqrt]
y:7 [in Coq.micromega.ZifyBool]
y:7 [in Coq.QArith.Qreals]
y:7 [in Coq.Arith.Cantor]
y:7 [in Coq.QArith.Qfield]
y:7 [in Coq.Sets.Cpo]
y:7 [in Coq.Wellfounded.Lexicographic_Exponentiation]
y:7 [in Coq.Reals.Raxioms]
y:7 [in Coq.Reals.PSeries_reg]
y:7 [in Coq.ssr.ssrunder]
y:7 [in Coq.micromega.RMicromega]
Y:7 [in Coq.Sets.Classical_sets]
y:7 [in Coq.PArith.BinPosDef]
y:7 [in Coq.Reals.R_sqr]
y:7 [in Coq.Relations.Relation_Operators]
y:7 [in Coq.Sorting.Heap]
y:7 [in Coq.Reals.Cos_plus]
y:70 [in Coq.Program.Wf]
y:70 [in Coq.Relations.Operators_Properties]
y:70 [in Coq.Logic.EqdepFacts]
y:70 [in Coq.Reals.Ranalysis4]
y:70 [in Coq.Structures.OrderedTypeEx]
y:70 [in Coq.setoid_ring.Ring_theory]
y:70 [in Coq.Relations.Relation_Operators]
y:70 [in Coq.QArith.QArith_base]
y:70 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:708 [in Coq.ssr.ssrbool]
y:71 [in Coq.Program.Wf]
y:71 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:71 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:71 [in Coq.FSets.FMapFacts]
y:71 [in Coq.ssr.ssrfun]
y:71 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:71 [in Coq.micromega.RMicromega]
y:71 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:710 [in Coq.ssr.ssrbool]
y:712 [in Coq.Lists.List]
y:72 [in Coq.Relations.Operators_Properties]
y:72 [in Coq.QArith.Qcanon]
y:72 [in Coq.Logic.JMeq]
y:72 [in Coq.Reals.Rsqrt_def]
y:72 [in Coq.Structures.OrderedTypeEx]
y:72 [in Coq.Reals.Raxioms]
y:72 [in Coq.Classes.CRelationClasses]
y:72 [in Coq.Structures.OrderedType]
y:72 [in Coq.Logic.Diaconescu]
y:72 [in Coq.QArith.QArith_base]
y:72 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:72 [in Coq.Structures.OrdersFacts]
y:73 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:73 [in Coq.micromega.RingMicromega]
y:73 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
y:73 [in Coq.Reals.Exp_prop]
y:73 [in Coq.Init.Wf]
y:73 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:73 [in Coq.micromega.RMicromega]
y:73 [in Coq.Logic.Diaconescu]
y:73 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:73 [in Coq.micromega.ZifyInst]
y:73 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:73 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:74 [in Coq.QArith.Qcanon]
y:74 [in Coq.Reals.Ranalysis4]
y:74 [in Coq.Classes.RelationClasses]
y:74 [in Coq.Reals.Rpower]
y:74 [in Coq.Structures.OrderedTypeEx]
y:74 [in Coq.Reals.Raxioms]
y:74 [in Coq.Sets.Uniset]
y:74 [in Coq.Structures.OrderedType]
y:74 [in Coq.Logic.Diaconescu]
y:74 [in Coq.Reals.R_sqr]
y:74 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:74 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:74 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:742 [in Coq.ssr.ssrbool]
y:75 [in Coq.FSets.FSetDecide]
y:75 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:75 [in Coq.FSets.FMapFacts]
y:75 [in Coq.MSets.MSetDecide]
y:75 [in Coq.Reals.Rbasic_fun]
y:75 [in Coq.Reals.Ranalysis5]
y:75 [in Coq.micromega.RMicromega]
y:75 [in Coq.Logic.Diaconescu]
y:75 [in Coq.micromega.ZifyInst]
y:75 [in Coq.Relations.Relation_Operators]
y:75 [in Coq.QArith.QArith_base]
y:75 [in Coq.Structures.OrdersFacts]
y:757 [in Coq.ssr.ssrbool]
y:759 [in Coq.ssr.ssrbool]
y:76 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:76 [in Coq.Logic.Eqdep_dec]
y:76 [in Coq.Reals.Rfunctions]
y:76 [in Coq.Arith.PeanoNat]
y:76 [in Coq.Vectors.Fin]
y:76 [in Coq.Reals.Rtopology]
y:76 [in Coq.Structures.OrderedType]
y:76 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:76 [in Coq.Logic.Diaconescu]
y:76 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:76 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:761 [in Coq.ssr.ssrbool]
y:763 [in Coq.ssr.ssrbool]
y:766 [in Coq.ssr.ssrbool]
y:768 [in Coq.ssr.ssrbool]
y:77 [in Coq.Reals.Abstract.ConstructiveReals]
y:77 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:77 [in Coq.Logic.ChoiceFacts]
y:77 [in Coq.Reals.Rpower]
y:77 [in Coq.omega.OmegaLemmas]
y:77 [in Coq.Reals.Rbasic_fun]
y:77 [in Coq.Init.Datatypes]
y:77 [in Coq.Reals.Ranalysis5]
y:77 [in Coq.Logic.Diaconescu]
y:77 [in Coq.micromega.ZifyInst]
y:77 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:770 [in Coq.ssr.ssrbool]
y:772 [in Coq.ssr.ssrbool]
y:774 [in Coq.ssr.ssrbool]
y:776 [in Coq.ssr.ssrbool]
y:778 [in Coq.ssr.ssrbool]
y:78 [in Coq.Logic.JMeq]
y:78 [in Coq.Structures.OrderedType]
y:78 [in Coq.setoid_ring.Ring_theory]
y:78 [in Coq.Structures.EqualitiesFacts]
y:78 [in Coq.QArith.QArith_base]
y:78 [in Coq.Structures.OrdersFacts]
y:780 [in Coq.ssr.ssrbool]
y:782 [in Coq.ssr.ssrbool]
y:784 [in Coq.ssr.ssrbool]
y:786 [in Coq.ssr.ssrbool]
y:788 [in Coq.ssr.ssrbool]
y:79 [in Coq.Classes.RelationClasses]
y:79 [in Coq.MSets.MSetWeakList]
y:79 [in Coq.Reals.Rtopology]
y:79 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:79 [in Coq.micromega.ZifyInst]
y:790 [in Coq.ssr.ssrbool]
y:792 [in Coq.ssr.ssrbool]
y:794 [in Coq.ssr.ssrbool]
y:796 [in Coq.ssr.ssrbool]
y:798 [in Coq.ssr.ssrbool]
y:8 [in Coq.Structures.Orders]
y:8 [in Coq.micromega.Ztac]
y:8 [in Coq.Structures.OrdersLists]
y:8 [in Coq.ZArith.BinIntDef]
y:8 [in Coq.FSets.FSetBridge]
y:8 [in Coq.Reals.Rminmax]
y:8 [in Coq.Sets.Constructive_sets]
y:8 [in Coq.PArith.BinPos]
y:8 [in Coq.Classes.RelationClasses]
y:8 [in Coq.ZArith.BinInt]
y:8 [in Coq.Logic.JMeq]
y:8 [in Coq.Structures.OrdersAlt]
y:8 [in Coq.Wellfounded.Lexicographic_Product]
y:8 [in Coq.Program.Subset]
y:8 [in Coq.Init.Wf]
y:8 [in Coq.NArith.BinNat]
y:8 [in Coq.Sorting.Permutation]
y:8 [in Coq.funind.Recdef]
y:8 [in Coq.Structures.OrderedTypeEx]
y:8 [in Coq.Structures.OrderedTypeAlt]
y:8 [in Coq.Logic.RelationalChoice]
y:8 [in Coq.ZArith.Zbool]
y:8 [in Coq.micromega.ZifyComparison]
y:8 [in Coq.Sets.Permut]
Y:8 [in Coq.Sets.Powerset_Classical_facts]
y:8 [in Coq.setoid_ring.Ring_theory]
y:8 [in Coq.omega.PreOmega]
y:8 [in Coq.Sets.Image]
y:8 [in Coq.Sets.Relations_1]
y:8 [in Coq.Relations.Relation_Definitions]
y:8 [in Coq.Numbers.Cyclic.Int63.Sint63]
y:8 [in Coq.Reals.ROrderedType]
y:8 [in Coq.Floats.FloatAxioms]
y:8 [in Coq.Reals.Cos_rel]
y:8 [in Coq.QArith.QArith_base]
y:8 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
y:8 [in Coq.Lists.SetoidList]
y:8 [in Coq.Structures.OrdersFacts]
y:80 [in Coq.QArith.Qcanon]
y:80 [in Coq.Logic.ChoiceFacts]
y:80 [in Coq.Reals.Rpower]
y:80 [in Coq.omega.OmegaLemmas]
y:80 [in Coq.Structures.OrderedType]
y:80 [in Coq.Reals.Rbasic_fun]
y:80 [in Coq.Reals.Ratan]
y:80 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:80 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:800 [in Coq.ssr.ssrbool]
y:802 [in Coq.Init.Specif]
y:802 [in Coq.ssr.ssrbool]
y:804 [in Coq.ssr.ssrbool]
y:806 [in Coq.ssr.ssrbool]
y:808 [in Coq.ssr.ssrbool]
y:81 [in Coq.FSets.FSetDecide]
y:81 [in Coq.Reals.Ranalysis4]
y:81 [in Coq.MSets.MSetDecide]
y:81 [in Coq.setoid_ring.Ring_theory]
y:81 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:81 [in Coq.micromega.ZifyInst]
y:81 [in Coq.Structures.OrdersFacts]
y:82 [in Coq.Program.Wf]
y:82 [in Coq.QArith.Qcanon]
y:82 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:82 [in Coq.Arith.PeanoNat]
y:82 [in Coq.Structures.OrderedTypeEx]
y:82 [in Coq.Structures.OrderedType]
y:82 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:824 [in Coq.ssr.ssrbool]
y:826 [in Coq.ssr.ssrbool]
y:828 [in Coq.ssr.ssrbool]
y:83 [in Coq.Logic.Eqdep_dec]
y:83 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
y:83 [in Coq.Classes.CRelationClasses]
y:83 [in Coq.Reals.Rbasic_fun]
y:83 [in Coq.Reals.Ranalysis5]
y:83 [in Coq.Structures.EqualitiesFacts]
y:83 [in Coq.PArith.BinPosDef]
y:83 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:83 [in Coq.Relations.Relation_Operators]
y:83 [in Coq.Structures.OrdersFacts]
y:830 [in Coq.ssr.ssrbool]
y:836 [in Coq.ssr.ssrbool]
y:838 [in Coq.ssr.ssrbool]
y:84 [in Coq.Reals.Abstract.ConstructiveReals]
y:84 [in Coq.FSets.FSetDecide]
y:84 [in Coq.Reals.Rsqrt_def]
y:84 [in Coq.MSets.MSetDecide]
y:84 [in Coq.Init.Wf]
y:84 [in Coq.Arith.PeanoNat]
y:84 [in Coq.omega.OmegaLemmas]
y:84 [in Coq.Structures.OrderedTypeEx]
y:84 [in Coq.Reals.Rtopology]
y:84 [in Coq.Structures.OrderedType]
y:84 [in Coq.Reals.Ranalysis5]
y:84 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:84 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:84 [in Coq.micromega.Tauto]
y:84 [in Coq.Logic.FinFun]
y:840 [in Coq.ssr.ssrbool]
y:842 [in Coq.ssr.ssrbool]
y:844 [in Coq.ssr.ssrbool]
y:846 [in Coq.ssr.ssrbool]
y:848 [in Coq.ssr.ssrbool]
y:85 [in Coq.QArith.Qcanon]
y:85 [in Coq.micromega.ZifyClasses]
y:85 [in Coq.Classes.RelationClasses]
y:85 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
y:85 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:85 [in Coq.setoid_ring.Ring_theory]
y:85 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:85 [in Coq.PArith.BinPosDef]
y:85 [in Coq.Relations.Relation_Operators]
y:85 [in Coq.Structures.OrdersFacts]
y:850 [in Coq.ssr.ssrbool]
y:852 [in Coq.ssr.ssrbool]
y:854 [in Coq.ssr.ssrbool]
y:856 [in Coq.ssr.ssrbool]
y:858 [in Coq.Lists.List]
y:858 [in Coq.ssr.ssrbool]
y:86 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:86 [in Coq.MSets.MSetWeakList]
y:86 [in Coq.Arith.PeanoNat]
y:86 [in Coq.Structures.OrderedType]
y:86 [in Coq.Reals.Rbasic_fun]
y:86 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:86 [in Coq.Lists.SetoidList]
y:860 [in Coq.ssr.ssrbool]
y:862 [in Coq.ssr.ssrbool]
y:864 [in Coq.ssr.ssrbool]
y:866 [in Coq.ssr.ssrbool]
y:868 [in Coq.ssr.ssrbool]
y:87 [in Coq.QArith.Qcanon]
y:87 [in Coq.Logic.Eqdep_dec]
y:87 [in Coq.Reals.Ranalysis4]
y:87 [in Coq.Reals.Exp_prop]
y:87 [in Coq.Reals.Rpower]
y:87 [in Coq.omega.OmegaLemmas]
y:87 [in Coq.Structures.OrderedTypeEx]
y:87 [in Coq.micromega.Tauto]
y:87 [in Coq.Relations.Relation_Operators]
y:87 [in Coq.Logic.FinFun]
y:87 [in Coq.FSets.FSetCompat]
y:87 [in Coq.Structures.OrdersFacts]
y:87 [in Coq.Reals.Cos_plus]
y:870 [in Coq.ssr.ssrbool]
y:872 [in Coq.ssr.ssrbool]
y:874 [in Coq.ssr.ssrbool]
y:876 [in Coq.ssr.ssrbool]
y:878 [in Coq.ssr.ssrbool]
y:88 [in Coq.Reals.Abstract.ConstructiveReals]
y:88 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:88 [in Coq.Floats.SpecFloat]
y:88 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
y:88 [in Coq.Reals.Rsqrt_def]
y:88 [in Coq.Classes.CRelationClasses]
y:88 [in Coq.Reals.Ranalysis5]
y:88 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:88 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:887 [in Coq.ssr.ssrbool]
y:889 [in Coq.ssr.ssrbool]
y:89 [in Coq.Program.Wf]
y:89 [in Coq.Reals.Exp_prop]
y:89 [in Coq.Logic.ChoiceFacts]
y:89 [in Coq.MSets.MSetGenTree]
y:89 [in Coq.Structures.OrderedType]
y:89 [in Coq.setoid_ring.Ring_theory]
y:89 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:89 [in Coq.FSets.FSetCompat]
y:89 [in Coq.Structures.OrdersFacts]
y:89 [in Coq.Reals.Cos_plus]
y:890 [in Coq.ssr.ssrbool]
y:892 [in Coq.ssr.ssrbool]
y:895 [in Coq.ssr.ssrbool]
y:897 [in Coq.ssr.ssrbool]
y:898 [in Coq.ssr.ssrbool]
y:9 [in Coq.Relations.Operators_Properties]
y:9 [in Coq.Reals.Abstract.ConstructiveReals]
y:9 [in Coq.Logic.Eqdep_dec]
y:9 [in Coq.Arith.Bool_nat]
y:9 [in Coq.Logic.SetoidChoice]
y:9 [in Coq.Reals.R_sqrt]
y:9 [in Coq.Logic.ChoiceFacts]
y:9 [in Coq.QArith.Qreals]
y:9 [in Coq.Reals.Abstract.ConstructiveAbs]
y:9 [in Coq.Sets.Partial_Order]
y:9 [in Coq.Classes.CRelationClasses]
y:9 [in Coq.Reals.Cauchy.ConstructiveExtra]
y:9 [in Coq.Structures.Equalities]
y:9 [in Coq.Bool.BoolEq]
y:9 [in Coq.Strings.Byte]
y:9 [in Coq.Setoids.Setoid]
y:9 [in Coq.Reals.R_sqr]
y:9 [in Coq.Reals.ClassicalConstructiveReals]
y:9 [in Coq.Logic.FinFun]
y:9 [in Coq.Sets.Powerset]
y:90 [in Coq.Program.Wf]
y:90 [in Coq.QArith.Qcanon]
y:90 [in Coq.FSets.FSetDecide]
y:90 [in Coq.MSets.MSetDecide]
y:90 [in Coq.Lists.ListSet]
y:90 [in Coq.Reals.Ranalysis5]
y:90 [in Coq.Reals.Abstract.ConstructiveMinMax]
y:90 [in Coq.Reals.ClassicalDedekindReals]
y:900 [in Coq.ssr.ssrbool]
y:903 [in Coq.ssr.ssrbool]
y:905 [in Coq.ssr.ssrbool]
y:906 [in Coq.ssr.ssrbool]
y:908 [in Coq.ssr.ssrbool]
y:91 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:91 [in Coq.setoid_ring.Ncring]
y:91 [in Coq.micromega.Tauto]
y:91 [in Coq.Structures.OrdersFacts]
y:91 [in Coq.Reals.Cos_plus]
y:911 [in Coq.ssr.ssrbool]
y:913 [in Coq.ssr.ssrbool]
y:914 [in Coq.ssr.ssrbool]
y:916 [in Coq.ssr.ssrbool]
y:919 [in Coq.ssr.ssrbool]
y:92 [in Coq.QArith.Qcanon]
y:92 [in Coq.Logic.Eqdep_dec]
y:92 [in Coq.Structures.OrderedType]
y:92 [in Coq.Reals.Ratan]
y:92 [in Coq.Reals.Ranalysis5]
y:92 [in Coq.setoid_ring.Ring_theory]
y:92 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:92 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:921 [in Coq.ssr.ssrbool]
y:922 [in Coq.ssr.ssrbool]
y:924 [in Coq.ssr.ssrbool]
y:927 [in Coq.ssr.ssrbool]
y:929 [in Coq.ssr.ssrbool]
y:93 [in Coq.Sorting.PermutSetoid]
y:93 [in Coq.MSets.MSetWeakList]
y:93 [in Coq.MSets.MSetGenTree]
y:93 [in Coq.Lists.ListSet]
y:93 [in Coq.Reals.Cos_rel]
y:93 [in Coq.Reals.ClassicalDedekindReals]
y:93 [in Coq.Lists.SetoidList]
y:93 [in Coq.Structures.OrdersFacts]
y:930 [in Coq.ssr.ssrbool]
y:932 [in Coq.ssr.ssrbool]
y:932 [in Coq.FSets.FMapAVL]
y:936 [in Coq.FSets.FMapAVL]
y:94 [in Coq.QArith.Qcanon]
y:94 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:94 [in Coq.Logic.Eqdep_dec]
y:94 [in Coq.Floats.SpecFloat]
y:94 [in Coq.Classes.CRelationClasses]
y:94 [in Coq.Reals.Ranalysis5]
y:94 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:94 [in Coq.setoid_ring.Ncring]
y:942 [in Coq.FSets.FMapAVL]
y:946 [in Coq.FSets.FMapAVL]
y:95 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:95 [in Coq.Reals.Rsqrt_def]
y:95 [in Coq.Init.Nat]
y:95 [in Coq.Logic.Hurkens]
y:95 [in Coq.Reals.Rtopology]
y:95 [in Coq.Structures.OrderedType]
y:95 [in Coq.Reals.PSeries_reg]
y:95 [in Coq.setoid_ring.Ring_theory]
y:95 [in Coq.Structures.OrdersFacts]
y:952 [in Coq.FSets.FMapAVL]
y:958 [in Coq.FSets.FMapAVL]
y:96 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
y:96 [in Coq.Lists.ListSet]
y:96 [in Coq.Reals.PSeries_reg]
y:96 [in Coq.Reals.Ratan]
y:96 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:962 [in Coq.Init.Logic]
y:964 [in Coq.FSets.FMapAVL]
y:97 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
y:97 [in Coq.QArith.Qcanon]
y:97 [in Coq.Logic.Hurkens]
y:97 [in Coq.MSets.MSetGenTree]
y:97 [in Coq.Structures.OrderedType]
y:97 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
y:97 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
y:97 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
y:97 [in Coq.Relations.Relation_Operators]
y:97 [in Coq.Structures.OrdersFacts]
y:970 [in Coq.FSets.FMapAVL]
y:976 [in Coq.FSets.FMapAVL]
y:98 [in Coq.Program.Wf]
y:98 [in Coq.Logic.ConstructiveEpsilon]
y:98 [in Coq.Reals.Rfunctions]
y:98 [in Coq.FSets.FMapFacts]
y:98 [in Coq.Reals.Ranalysis5]
y:984 [in Coq.FSets.FMapAVL]
y:989 [in Coq.FSets.FMapAVL]
y:99 [in Coq.FSets.FSetBridge]
y:99 [in Coq.Floats.SpecFloat]
y:99 [in Coq.Reals.RiemannInt]
y:99 [in Coq.FSets.FMapInterface]
y:99 [in Coq.ssr.ssreflect]
y:99 [in Coq.Structures.OrderedType]
y:99 [in Coq.Lists.ListSet]
y:99 [in Coq.Reals.Ratan]
y:99 [in Coq.Numbers.Cyclic.Int63.Uint63]
y:99 [in Coq.Structures.OrdersFacts]
| 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 | (72745 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 | (47313 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 | (784 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 | (1547 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 | (583 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 | (11764 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 | (627 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 | (492 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 | (903 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 | (1448 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 | (4360 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) |