Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (68863 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (985 entries)
Binder Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (44709 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (761 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1497 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (570 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11380 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (976 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (603 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (298 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (460 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (476 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (811 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1157 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4018 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (162 entries)

Z (binder)

zero:176 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
zero:179 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
zero:181 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
zero:184 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
zero:186 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
zero:190 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
zero:6 [in Coq.Numbers.Cyclic.Int63.Ring63]
zero:6 [in Coq.Numbers.Cyclic.Int31.Ring31]
zeta:415 [in Coq.Reals.Rtopology]
zeta:421 [in Coq.Reals.Rtopology]
zeta:427 [in Coq.Reals.Rtopology]
zeta:429 [in Coq.Reals.Rtopology]
zeta:455 [in Coq.Reals.Rtopology]
zeta:457 [in Coq.Reals.Rtopology]
znz:11 [in Coq.Numbers.Cyclic.Abstract.DoubleType]
znz:14 [in Coq.Numbers.Cyclic.Abstract.DoubleType]
z':152 [in Coq.Lists.SetoidList]
z':158 [in Coq.Lists.SetoidList]
z':373 [in Coq.Logic.ChoiceFacts]
z':379 [in Coq.Logic.ChoiceFacts]
z1:1 [in Coq.Reals.DiscrR]
z1:104 [in Coq.Reals.Rtopology]
z1:561 [in Coq.Reals.RIneq]
z2:105 [in Coq.Reals.Rtopology]
z2:2 [in Coq.Reals.DiscrR]
z2:562 [in Coq.Reals.RIneq]
z:1 [in Coq.ZArith.Zeven]
z:1 [in Coq.nsatz.Nsatz]
z:1 [in Coq.Numbers.DecimalZ]
z:1 [in Coq.ZArith.Zpower]
z:1 [in Coq.Numbers.HexadecimalZ]
z:1 [in Coq.Numbers.AltBinNotations]
z:10 [in Coq.Reals.Abstract.ConstructiveReals]
z:10 [in Coq.micromega.ZifyBool]
z:10 [in Coq.ZArith.Zpower]
z:10 [in Coq.Structures.Equalities]
z:10 [in Coq.Sets.Powerset]
z:100 [in Coq.Reals.Rsqrt_def]
z:101 [in Coq.QArith.Qcanon]
z:101 [in Coq.Reals.Rsqrt_def]
z:102 [in Coq.Reals.Rsqrt_def]
z:103 [in Coq.Reals.Rsqrt_def]
z:103 [in Coq.Arith.PeanoNat]
z:103 [in Coq.setoid_ring.Ncring]
z:103 [in Coq.Reals.Abstract.ConstructiveMinMax]
z:104 [in Coq.Reals.Rsqrt_def]
z:105 [in Coq.setoid_ring.Ring_theory]
z:106 [in Coq.Reals.Rsqrt_def]
z:107 [in Coq.setoid_ring.Ncring]
z:108 [in Coq.Reals.Rsqrt_def]
z:11 [in Coq.ZArith.BinInt]
z:11 [in Coq.ZArith.Zcomplements]
z:110 [in Coq.Reals.Rsqrt_def]
z:110 [in Coq.Reals.Rpower]
z:110 [in Coq.Lists.SetoidList]
z:111 [in Coq.setoid_ring.Ncring]
z:112 [in Coq.Reals.Rsqrt_def]
z:112 [in Coq.QArith.QArith_base]
z:113 [in Coq.FSets.FSetDecide]
z:113 [in Coq.MSets.MSetDecide]
z:114 [in Coq.setoid_ring.Ring_theory]
z:115 [in Coq.Lists.SetoidList]
z:118 [in Coq.setoid_ring.Ring_theory]
z:119 [in Coq.micromega.ZMicromega]
z:12 [in Coq.Sets.Relations_3]
z:12 [in Coq.ZArith.Zpower]
z:12 [in Coq.Numbers.NatInt.NZParity]
z:12 [in Coq.ZArith.Zcomplements]
z:1208 [in Coq.FSets.FMapAVL]
z:121 [in Coq.Reals.Rsqrt_def]
z:122 [in Coq.Reals.Rsqrt_def]
z:122 [in Coq.Structures.OrderedTypeEx]
z:122 [in Coq.Reals.Ranalysis5]
z:122 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
z:123 [in Coq.Reals.Rsqrt_def]
z:123 [in Coq.Reals.Rbasic_fun]
z:123 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:1236 [in Coq.FSets.FMapAVL]
z:124 [in Coq.QArith.Qcanon]
z:124 [in Coq.Reals.Rfunctions]
z:124 [in Coq.Reals.Rsqrt_def]
z:124 [in Coq.Reals.Rbasic_fun]
z:124 [in Coq.Reals.Ranalysis5]
z:125 [in Coq.Reals.Rsqrt_def]
z:125 [in Coq.Reals.Ranalysis5]
z:125 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
z:126 [in Coq.Reals.Rsqrt_def]
z:126 [in Coq.Reals.Ranalysis5]
z:127 [in Coq.Reals.Abstract.ConstructiveReals]
z:127 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
z:127 [in Coq.Reals.Rsqrt_def]
z:127 [in Coq.Reals.Ranalysis5]
z:127 [in Coq.QArith.QArith_base]
z:128 [in Coq.QArith.Qcanon]
z:128 [in Coq.Reals.Rsqrt_def]
z:128 [in Coq.Reals.Ranalysis5]
z:129 [in Coq.Reals.Rsqrt_def]
z:129 [in Coq.Reals.Ranalysis5]
z:13 [in Coq.Structures.OrdersEx]
z:13 [in Coq.extraction.ExtrOcamlBigIntConv]
z:13 [in Coq.Numbers.NatInt.NZParity]
z:13 [in Coq.Sets.Permut]
z:13 [in Coq.Sets.Relations_2]
z:13 [in Coq.extraction.ExtrOcamlIntConv]
z:13 [in Coq.Sets.Powerset]
z:130 [in Coq.Reals.Rsqrt_def]
z:130 [in Coq.Reals.Ranalysis5]
z:130 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:131 [in Coq.Reals.Abstract.ConstructiveReals]
z:131 [in Coq.QArith.Qcanon]
z:131 [in Coq.Reals.Rsqrt_def]
z:131 [in Coq.Reals.Ranalysis5]
z:132 [in Coq.Reals.Rsqrt_def]
z:133 [in Coq.setoid_ring.Ncring_tac]
z:133 [in Coq.Reals.Ranalysis5]
z:133 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:134 [in Coq.QArith.Qcanon]
z:134 [in Coq.ZArith.BinIntDef]
z:135 [in Coq.Reals.Abstract.ConstructiveReals]
z:135 [in Coq.Reals.Ranalysis5]
z:136 [in Coq.ZArith.BinIntDef]
z:136 [in Coq.Reals.Rfunctions]
z:136 [in Coq.Reals.Rsqrt_def]
z:136 [in Coq.Reals.Rbasic_fun]
z:136 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:136 [in Coq.QArith.QArith_base]
z:137 [in Coq.Reals.Ranalysis5]
z:138 [in Coq.ZArith.BinIntDef]
z:138 [in Coq.Reals.Rfunctions]
z:138 [in Coq.Reals.Rsqrt_def]
z:139 [in Coq.Reals.Ranalysis5]
z:139 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:139 [in Coq.QArith.QArith_base]
z:14 [in Coq.Reals.Rsqrt_def]
z:14 [in Coq.ZArith.Zwf]
z:14 [in Coq.Sets.Partial_Order]
z:14 [in Coq.Relations.Relation_Operators]
z:140 [in Coq.ZArith.BinIntDef]
z:142 [in Coq.ZArith.BinIntDef]
z:142 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:144 [in Coq.Reals.Abstract.ConstructiveReals]
z:144 [in Coq.Reals.Rtopology]
z:145 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:148 [in Coq.Reals.Rtopology]
z:148 [in Coq.Reals.Ranalysis5]
z:149 [in Coq.Reals.Ranalysis5]
z:15 [in Coq.Classes.SetoidClass]
z:15 [in Coq.Setoids.Setoid]
z:150 [in Coq.Reals.Ranalysis5]
z:151 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
z:151 [in Coq.Reals.Rtopology]
z:151 [in Coq.Reals.Ranalysis5]
z:151 [in Coq.QArith.QArith_base]
z:151 [in Coq.Lists.SetoidList]
z:152 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
z:152 [in Coq.Reals.Rtopology]
z:152 [in Coq.Reals.Ranalysis5]
z:153 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
z:153 [in Coq.Reals.Ranalysis5]
z:154 [in Coq.Reals.Ranalysis5]
z:154 [in Coq.QArith.QArith_base]
z:155 [in Coq.Reals.Rpower]
z:155 [in Coq.Reals.Ranalysis5]
z:156 [in Coq.Reals.Ranalysis5]
z:157 [in Coq.Reals.Ranalysis5]
z:157 [in Coq.Lists.SetoidList]
z:158 [in Coq.Reals.Ranalysis5]
z:158 [in Coq.ZArith.Znat]
z:159 [in Coq.Reals.Ranalysis5]
z:16 [in Coq.Numbers.NatInt.NZBase]
z:16 [in Coq.ZArith.Zpower]
z:16 [in Coq.Reals.PSeries_reg]
z:160 [in Coq.Reals.Rfunctions]
z:160 [in Coq.Reals.Ranalysis5]
z:161 [in Coq.Reals.Ranalysis5]
z:161 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:162 [in Coq.Reals.Ranalysis5]
z:163 [in Coq.Reals.Ranalysis5]
z:164 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:167 [in Coq.ZArith.Znumtheory]
z:169 [in Coq.Reals.Rpower]
z:17 [in Coq.setoid_ring.Ncring_initial]
z:17 [in Coq.setoid_ring.InitialRing]
z:17 [in Coq.ZArith.Zdigits]
z:17 [in Coq.Sets.Permut]
z:17 [in Coq.ZArith.Zcomplements]
z:17 [in Coq.micromega.ZCoeff]
z:17 [in Coq.Sorting.Heap]
z:172 [in Coq.Reals.Rpower]
z:172 [in Coq.Reals.PSeries_reg]
z:174 [in Coq.Reals.PSeries_reg]
z:175 [in Coq.Reals.Rpower]
z:176 [in Coq.Reals.PSeries_reg]
z:178 [in Coq.Reals.Rpower]
z:178 [in Coq.Reals.PSeries_reg]
z:179 [in Coq.Reals.PSeries_reg]
z:18 [in Coq.Floats.FloatLemmas]
z:18 [in Coq.Logic.JMeq]
z:18 [in Coq.Reals.Rsqrt_def]
z:18 [in Coq.Structures.OrderedTypeEx]
z:18 [in Coq.Structures.OrderedType]
z:18 [in Coq.Sets.Powerset_facts]
z:18 [in Coq.ZArith.Zcomplements]
z:180 [in Coq.Reals.PSeries_reg]
z:180 [in Coq.QArith.QArith_base]
z:183 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
z:183 [in Coq.Reals.PSeries_reg]
z:183 [in Coq.QArith.QArith_base]
z:184 [in Coq.Reals.Rtopology]
z:185 [in Coq.Reals.Rtopology]
z:186 [in Coq.Reals.PSeries_reg]
z:189 [in Coq.QArith.QArith_base]
z:19 [in Coq.setoid_ring.Ncring_initial]
z:19 [in Coq.Logic.EqdepFacts]
z:19 [in Coq.Floats.FloatLemmas]
z:19 [in Coq.setoid_ring.InitialRing]
z:19 [in Coq.Sets.Partial_Order]
z:19 [in Coq.Sets.Relations_2]
z:191 [in Coq.Logic.EqdepFacts]
z:192 [in Coq.Reals.Ranalysis5]
z:193 [in Coq.Reals.Ranalysis1]
z:193 [in Coq.Reals.PSeries_reg]
z:194 [in Coq.Logic.EqdepFacts]
z:194 [in Coq.Reals.Rtopology]
z:195 [in Coq.Bool.Bool]
z:195 [in Coq.omega.OmegaLemmas]
z:195 [in Coq.Reals.Rtopology]
z:195 [in Coq.Reals.PSeries_reg]
z:195 [in Coq.Reals.Ranalysis5]
z:199 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
z:2 [in Coq.micromega.ZifyBool]
z:2 [in Coq.ZArith.Zpower]
z:20 [in Coq.ZArith.Wf_Z]
z:20 [in Coq.Reals.Rpower]
z:20 [in Coq.Classes.SetoidClass]
z:20 [in Coq.micromega.RMicromega]
z:20 [in Coq.Relations.Relation_Operators]
z:200 [in Coq.Reals.Ranalysis1]
z:202 [in Coq.Reals.Ranalysis5]
z:203 [in Coq.QArith.QArith_base]
z:204 [in Coq.Reals.Rfunctions]
z:205 [in Coq.Reals.Ranalysis5]
z:206 [in Coq.QArith.QArith_base]
z:209 [in Coq.QArith.QArith_base]
z:21 [in Coq.setoid_ring.Ncring_initial]
z:21 [in Coq.Reals.Abstract.ConstructiveLUB]
z:21 [in Coq.ZArith.Wf_Z]
z:21 [in Coq.setoid_ring.InitialRing]
z:21 [in Coq.Wellfounded.Lexicographic_Exponentiation]
z:21 [in Coq.ZArith.Zpower]
z:21 [in Coq.Sets.Permut]
z:21 [in Coq.Sets.Multiset]
z:210 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
z:216 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
z:219 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
z:22 [in Coq.Strings.OctalString]
z:22 [in Coq.Strings.HexString]
z:22 [in Coq.Sets.Partial_Order]
z:22 [in Coq.Strings.BinaryString]
z:22 [in Coq.Structures.OrderedType]
z:22 [in Coq.Structures.OrdersTac]
z:220 [in Coq.setoid_ring.Field_theory]
z:225 [in Coq.setoid_ring.Ncring]
z:228 [in Coq.setoid_ring.Ncring]
z:23 [in Coq.Reals.Abstract.ConstructiveLUB]
z:23 [in Coq.ZArith.Wf_Z]
z:23 [in Coq.ZArith.Zpower]
z:23 [in Coq.Sets.Powerset_facts]
z:23 [in Coq.Sets.Relations_2]
z:23 [in Coq.micromega.RMicromega]
z:232 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
z:232 [in Coq.Reals.Ranalysis5]
z:233 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
z:234 [in Coq.QArith.QArith_base]
z:235 [in Coq.Reals.Ranalysis5]
z:238 [in Coq.Reals.Ranalysis5]
z:238 [in Coq.QArith.QArith_base]
z:24 [in Coq.ZArith.Wf_Z]
z:24 [in Coq.Numbers.DecimalQ]
z:24 [in Coq.Reals.Rpower]
z:24 [in Coq.omega.OmegaLemmas]
z:240 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
z:241 [in Coq.Reals.Ranalysis5]
z:242 [in Coq.QArith.QArith_base]
z:243 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
z:245 [in Coq.QArith.QArith_base]
z:248 [in Coq.QArith.QArith_base]
z:249 [in Coq.micromega.ZMicromega]
z:25 [in Coq.Structures.OrdersAlt]
z:25 [in Coq.ZArith.Zdigits]
z:25 [in Coq.ZArith.Zpower]
z:25 [in Coq.Reals.RList]
z:25 [in Coq.Structures.OrdersTac]
z:251 [in Coq.QArith.QArith_base]
z:254 [in Coq.QArith.QArith_base]
z:257 [in Coq.QArith.QArith_base]
z:26 [in Coq.ZArith.BinIntDef]
z:260 [in Coq.QArith.QArith_base]
z:263 [in Coq.QArith.QArith_base]
z:265 [in Coq.setoid_ring.Ring_theory]
z:266 [in Coq.QArith.QArith_base]
z:268 [in Coq.setoid_ring.Ring_theory]
z:269 [in Coq.QArith.QArith_base]
z:27 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
z:27 [in Coq.Classes.RelationClasses]
z:27 [in Coq.ZArith.Zdigits]
z:27 [in Coq.omega.OmegaLemmas]
z:27 [in Coq.Structures.OrderedTypeEx]
z:27 [in Coq.Reals.Abstract.ConstructiveMinMax]
z:27 [in Coq.QArith.QArith_base]
z:271 [in Coq.setoid_ring.Ring_theory]
z:272 [in Coq.QArith.QArith_base]
z:273 [in Coq.Init.Logic]
z:274 [in Coq.setoid_ring.Ring_theory]
z:277 [in Coq.setoid_ring.Ring_theory]
z:28 [in Coq.Structures.OrdersAlt]
z:28 [in Coq.ZArith.Zdigits]
z:28 [in Coq.Reals.Rbasic_fun]
z:28 [in Coq.Logic.HLevels]
z:28 [in Coq.Sets.Permut]
z:28 [in Coq.micromega.RMicromega]
z:28 [in Coq.ZArith.Znat]
z:28 [in Coq.Structures.OrdersTac]
z:29 [in Coq.ZArith.Zdigits]
z:291 [in Coq.Reals.Ranalysis5]
z:294 [in Coq.Reals.Ranalysis5]
z:297 [in Coq.Reals.Ranalysis5]
z:3 [in Coq.ZArith.Zeven]
z:3 [in Coq.QArith.Qfield]
z:30 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
z:30 [in Coq.ZArith.Zdigits]
z:30 [in Coq.omega.OmegaLemmas]
z:30 [in Coq.Sets.Relations_2_facts]
z:30 [in Coq.micromega.RMicromega]
z:300 [in Coq.Reals.Ranalysis5]
z:300 [in Coq.QArith.QArith_base]
z:301 [in Coq.Numbers.Cyclic.Int63.Int63]
z:303 [in Coq.Reals.Ranalysis5]
z:304 [in Coq.MSets.MSetInterface]
z:306 [in Coq.Reals.Ranalysis5]
z:307 [in Coq.Init.Logic]
z:307 [in Coq.micromega.ZMicromega]
z:308 [in Coq.Numbers.Cyclic.Int63.Int63]
z:31 [in Coq.Sets.Uniset]
z:31 [in Coq.Structures.OrderedTypeAlt]
z:31 [in Coq.Reals.Rbasic_fun]
z:31 [in Coq.micromega.RMicromega]
z:31 [in Coq.Structures.OrdersTac]
z:311 [in Coq.Numbers.Cyclic.Int63.Int63]
z:318 [in Coq.Init.Logic]
z:32 [in Coq.Reals.Rtrigo1]
z:32 [in Coq.Reals.Rlimit]
z:32 [in Coq.Numbers.NatInt.NZOrder]
z:32 [in Coq.Logic.HLevels]
z:32 [in Coq.Sets.Permut]
z:328 [in Coq.Reals.Rtopology]
z:33 [in Coq.Strings.OctalString]
z:33 [in Coq.Sets.Constructive_sets]
z:33 [in Coq.Strings.HexString]
z:33 [in Coq.ZArith.Zdigits]
z:33 [in Coq.omega.OmegaLemmas]
z:33 [in Coq.Strings.BinaryString]
z:33 [in Coq.Sets.Multiset]
z:33 [in Coq.micromega.RMicromega]
z:335 [in Coq.ssr.ssrfun]
z:34 [in Coq.Sets.Ensembles]
z:34 [in Coq.ZArith.Zdigits]
z:34 [in Coq.Sets.Cpo]
z:34 [in Coq.Structures.OrdersTac]
z:34 [in Coq.Relations.Relation_Operators]
z:341 [in Coq.ssr.ssrfun]
z:345 [in Coq.Reals.Rtopology]
z:346 [in Coq.ssr.ssrfun]
z:346 [in Coq.Reals.Rtopology]
z:35 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
z:35 [in Coq.ZArith.Zpow_facts]
z:35 [in Coq.ZArith.Zdigits]
z:35 [in Coq.Numbers.NatInt.NZOrder]
z:35 [in Coq.Lists.ListSet]
z:35 [in Coq.Sets.Permut]
z:35 [in Coq.Relations.Relation_Definitions]
z:35 [in Coq.Structures.OrdersFacts]
z:351 [in Coq.micromega.ZMicromega]
z:353 [in Coq.Reals.Rtopology]
z:354 [in Coq.Reals.Rtopology]
z:354 [in Coq.Init.Logic]
z:356 [in Coq.ssr.ssrfun]
z:358 [in Coq.Reals.Abstract.ConstructiveReals]
z:36 [in Coq.Relations.Operators_Properties]
z:36 [in Coq.ZArith.BinIntDef]
z:36 [in Coq.Logic.HLevels]
z:36 [in Coq.Sets.Powerset_Classical_facts]
z:36 [in Coq.Sets.Multiset]
z:362 [in Coq.Reals.Abstract.ConstructiveReals]
z:362 [in Coq.ssr.ssrfun]
z:367 [in Coq.ssr.ssrfun]
z:367 [in Coq.Init.Logic]
z:37 [in Coq.ZArith.Zpow_facts]
z:37 [in Coq.ZArith.Zdigits]
z:37 [in Coq.Sets.Relations_2_facts]
z:37 [in Coq.Structures.OrdersTac]
z:37 [in Coq.Reals.Abstract.ConstructiveMinMax]
z:371 [in Coq.Reals.Rtopology]
z:372 [in Coq.Logic.ChoiceFacts]
z:372 [in Coq.Reals.Rtopology]
z:373 [in Coq.Reals.Rtopology]
z:374 [in Coq.Reals.Rtopology]
z:374 [in Coq.Init.Logic]
z:376 [in Coq.Reals.Rtopology]
z:378 [in Coq.Logic.ChoiceFacts]
z:379 [in Coq.Reals.Rtopology]
z:38 [in Coq.Relations.Operators_Properties]
z:38 [in Coq.Classes.CRelationClasses]
z:38 [in Coq.Structures.OrderedType]
z:38 [in Coq.Numbers.NatInt.NZOrder]
z:38 [in Coq.Sets.Permut]
z:38 [in Coq.Reals.Ranalysis5]
z:38 [in Coq.Structures.OrdersFacts]
z:385 [in Coq.ssr.ssrfun]
z:39 [in Coq.ZArith.Zdigits]
z:39 [in Coq.omega.OmegaLemmas]
z:39 [in Coq.Numbers.HexadecimalQ]
z:39 [in Coq.Sets.Multiset]
z:39 [in Coq.Relations.Relation_Operators]
z:390 [in Coq.ssr.ssrfun]
z:4 [in Coq.Wellfounded.Inclusion]
z:4 [in Coq.Reals.R_Ifp]
z:4 [in Coq.nsatz.Nsatz]
z:4 [in Coq.ZArith.Zpower]
z:4 [in Coq.Reals.RiemannInt_SF]
z:4 [in Coq.Numbers.AltBinNotations]
z:40 [in Coq.Relations.Operators_Properties]
z:40 [in Coq.Reals.Rbasic_fun]
z:40 [in Coq.Logic.HLevels]
z:40 [in Coq.Structures.OrdersTac]
z:41 [in Coq.Structures.OrderedType]
z:41 [in Coq.Numbers.NatInt.NZOrder]
z:41 [in Coq.Lists.ListSet]
z:41 [in Coq.Sets.Permut]
z:41 [in Coq.Reals.Ranalysis5]
z:41 [in Coq.Numbers.HexadecimalQ]
z:414 [in Coq.Reals.Rtopology]
z:416 [in Coq.Reals.Rtopology]
z:42 [in Coq.ZArith.Wf_Z]
z:42 [in Coq.Sets.Multiset]
z:420 [in Coq.Reals.Rtopology]
z:422 [in Coq.Reals.Rtopology]
z:428 [in Coq.Reals.Rtopology]
z:429 [in Coq.Init.Logic]
z:43 [in Coq.Sets.Uniset]
z:43 [in Coq.Reals.Rbasic_fun]
z:43 [in Coq.Structures.OrdersTac]
z:430 [in Coq.Reals.Rtopology]
z:44 [in Coq.Structures.OrdersAlt]
z:44 [in Coq.Sets.Permut]
z:44 [in Coq.Reals.Ranalysis5]
z:44 [in Coq.Relations.Relation_Operators]
z:441 [in Coq.Reals.Rtopology]
z:442 [in Coq.Reals.Rtopology]
z:445 [in Coq.Reals.Rtopology]
z:446 [in Coq.Reals.Rtopology]
z:449 [in Coq.Reals.Rtopology]
z:45 [in Coq.Relations.Operators_Properties]
z:45 [in Coq.Logic.HLevels]
z:45 [in Coq.Sets.Multiset]
z:45 [in Coq.Reals.Abstract.ConstructiveMinMax]
z:450 [in Coq.Reals.Rtopology]
z:453 [in Coq.Reals.Rtopology]
z:454 [in Coq.Reals.Rtopology]
z:456 [in Coq.Reals.Rtopology]
z:458 [in Coq.Reals.Rtopology]
z:46 [in Coq.Numbers.DecimalQ]
z:46 [in Coq.ZArith.Zdigits]
z:46 [in Coq.Sets.Uniset]
z:46 [in Coq.Structures.OrdersTac]
z:47 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
z:47 [in Coq.ZArith.Wf_Z]
z:47 [in Coq.Numbers.DecimalQ]
z:47 [in Coq.Structures.OrderedTypeEx]
z:47 [in Coq.Reals.Ranalysis5]
z:48 [in Coq.Numbers.Cyclic.Int63.Int63]
z:48 [in Coq.ZArith.Zdigits]
z:48 [in Coq.Reals.Rpower]
z:48 [in Coq.Sets.Permut]
z:480 [in Coq.Lists.List]
z:49 [in Coq.QArith.Qcanon]
z:49 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
z:49 [in Coq.Sets.Uniset]
z:49 [in Coq.Sets.Multiset]
z:49 [in Coq.micromega.RMicromega]
z:49 [in Coq.Structures.OrdersTac]
z:5 [in Coq.Relations.Operators_Properties]
z:5 [in Coq.Sets.Relations_3]
z:5 [in Coq.ZArith.Zdigits]
z:5 [in Coq.ZArith.Zeven]
z:5 [in Coq.ZArith.Zwf]
z:5 [in Coq.Structures.OrderedTypeEx]
z:5 [in Coq.Wellfounded.Lexicographic_Exponentiation]
z:50 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
z:50 [in Coq.Structures.OrderedTypeEx]
z:50 [in Coq.Structures.OrderedType]
z:506 [in Coq.ssr.ssrbool]
z:51 [in Coq.Reals.Rpower]
z:51 [in Coq.Numbers.HexadecimalQ]
z:51 [in Coq.micromega.RMicromega]
z:52 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
z:52 [in Coq.Sets.Uniset]
z:52 [in Coq.Numbers.HexadecimalQ]
z:52 [in Coq.Sets.Multiset]
z:52 [in Coq.Structures.OrdersTac]
z:523 [in Coq.ssr.ssrbool]
z:53 [in Coq.Relations.Operators_Properties]
z:53 [in Coq.Structures.OrderedType]
z:53 [in Coq.Reals.Abstract.ConstructiveMinMax]
z:533 [in Coq.ssr.ssrbool]
z:536 [in Coq.Reals.RIneq]
z:54 [in Coq.ZArith.BinIntDef]
z:54 [in Coq.FSets.FSetDecide]
z:54 [in Coq.MSets.MSetDecide]
z:542 [in Coq.PArith.BinPos]
z:55 [in Coq.Reals.Rdefinitions]
z:55 [in Coq.Sets.Uniset]
z:55 [in Coq.Structures.OrdersTac]
z:55 [in Coq.Structures.OrdersFacts]
z:556 [in Coq.ssr.ssrbool]
z:56 [in Coq.ZArith.BinIntDef]
z:56 [in Coq.Structures.OrderedType]
z:56 [in Coq.Sets.Powerset_facts]
z:56 [in Coq.Reals.Ranalysis5]
z:56 [in Coq.Sets.Multiset]
z:56 [in Coq.Relations.Relation_Operators]
z:560 [in Coq.ssr.ssrbool]
z:564 [in Coq.ssr.ssrbool]
z:568 [in Coq.ssr.ssrbool]
z:57 [in Coq.Numbers.HexadecimalQ]
z:58 [in Coq.ZArith.BinIntDef]
z:58 [in Coq.FSets.FSetDecide]
z:58 [in Coq.MSets.MSetDecide]
z:58 [in Coq.Reals.Rpower]
z:58 [in Coq.Numbers.HexadecimalQ]
z:58 [in Coq.Reals.R_sqr]
z:58 [in Coq.Structures.OrdersFacts]
z:59 [in Coq.Sets.Uniset]
z:59 [in Coq.Structures.OrderedType]
z:59 [in Coq.Reals.Ranalysis5]
z:6 [in Coq.Wellfounded.Union]
z:6 [in Coq.Reals.R_Ifp]
z:6 [in Coq.ZArith.Zeven]
z:6 [in Coq.Sets.Relations_1]
z:6 [in Coq.Relations.Relation_Definitions]
z:60 [in Coq.ZArith.BinIntDef]
z:60 [in Coq.Sets.Multiset]
z:61 [in Coq.ssr.ssrfun]
z:61 [in Coq.Reals.R_sqr]
z:61 [in Coq.Relations.Relation_Operators]
z:61 [in Coq.Structures.OrdersFacts]
z:62 [in Coq.ZArith.BinIntDef]
z:62 [in Coq.Sets.Uniset]
z:62 [in Coq.Structures.OrderedType]
z:62 [in Coq.Reals.Ranalysis5]
z:62 [in Coq.Reals.Abstract.ConstructiveMinMax]
z:63 [in Coq.Reals.Rpower]
z:64 [in Coq.Relations.Operators_Properties]
z:64 [in Coq.nsatz.NsatzTactic]
z:64 [in Coq.FSets.FSetDecide]
z:64 [in Coq.MSets.MSetDecide]
z:64 [in Coq.Structures.OrderedTypeEx]
z:64 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:64 [in Coq.Reals.R_sqr]
z:64 [in Coq.Structures.OrdersFacts]
z:65 [in Coq.Structures.OrderedType]
z:65 [in Coq.Sets.Powerset_facts]
z:65 [in Coq.Reals.Ranalysis5]
z:65 [in Coq.Sets.Multiset]
z:65 [in Coq.Lists.SetoidList]
z:66 [in Coq.Sets.Uniset]
z:66 [in Coq.Relations.Relation_Operators]
z:67 [in Coq.QArith.Qcanon]
z:67 [in Coq.Structures.OrderedTypeEx]
z:67 [in Coq.Reals.Rbasic_fun]
z:67 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:67 [in Coq.Structures.OrdersFacts]
z:68 [in Coq.ZArith.BinIntDef]
z:69 [in Coq.FSets.FSetDecide]
z:69 [in Coq.MSets.MSetDecide]
z:694 [in Coq.Init.Specif]
z:697 [in Coq.Init.Specif]
z:698 [in Coq.Init.Specif]
z:7 [in Coq.Reals.Abstract.ConstructiveReals]
z:7 [in Coq.Numbers.NatInt.NZBase]
z:7 [in Coq.ZArith.Zpower]
z:7 [in Coq.Sets.Relations_2]
z:7 [in Coq.QArith.Qround]
z:70 [in Coq.QArith.Qcanon]
z:70 [in Coq.Sets.Uniset]
z:70 [in Coq.Structures.OrderedType]
z:70 [in Coq.Reals.Rbasic_fun]
z:70 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:70 [in Coq.Structures.OrdersFacts]
z:700 [in Coq.Init.Specif]
z:703 [in Coq.Init.Specif]
z:704 [in Coq.Init.Specif]
z:708 [in Coq.Init.Specif]
z:709 [in Coq.Init.Specif]
z:71 [in Coq.setoid_ring.Ring_theory]
z:73 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:73 [in Coq.Structures.OrdersFacts]
z:75 [in Coq.Logic.Hurkens]
z:75 [in Coq.Sets.Uniset]
z:76 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:76 [in Coq.Structures.OrdersFacts]
z:77 [in Coq.Reals.Abstract.ConstructiveMinMax]
z:78 [in Coq.omega.OmegaLemmas]
z:78 [in Coq.Reals.Rbasic_fun]
z:79 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:79 [in Coq.Structures.OrdersFacts]
z:8 [in Coq.Structures.DecidableTypeEx]
z:8 [in Coq.Sets.Relations_3]
z:8 [in Coq.QArith.Qfield]
z:8 [in Coq.Wellfounded.Lexicographic_Exponentiation]
z:8 [in Coq.ZArith.Zpower]
z:8 [in Coq.Reals.PSeries_reg]
z:8 [in Coq.QArith.Qround]
z:8 [in Coq.Numbers.AltBinNotations]
z:8 [in Coq.Relations.Relation_Operators]
z:80 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
z:81 [in Coq.Reals.Rbasic_fun]
z:81 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
z:82 [in Coq.FSets.FSetDecide]
z:82 [in Coq.MSets.MSetDecide]
z:82 [in Coq.setoid_ring.Ring_theory]
z:82 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:83 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
z:84 [in Coq.Reals.Rbasic_fun]
z:84 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
z:84 [in Coq.QArith.QArith_base]
z:85 [in Coq.omega.OmegaLemmas]
z:85 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:86 [in Coq.Classes.RelationClasses]
z:86 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
z:86 [in Coq.setoid_ring.Ring_theory]
z:87 [in Coq.Structures.OrderedTypeEx]
z:87 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
z:88 [in Coq.QArith.Qcanon]
z:88 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:89 [in Coq.Logic.Hurkens]
z:9 [in Coq.Structures.OrdersAlt]
z:9 [in Coq.ZArith.Zdigits]
z:9 [in Coq.Structures.OrderedTypeAlt]
z:9 [in Coq.Sets.Permut]
z:9 [in Coq.setoid_ring.Ring_theory]
z:91 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:91 [in Coq.Reals.Abstract.ConstructiveMinMax]
z:92 [in Coq.Numbers.NatInt.NZOrder]
z:94 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
z:95 [in Coq.QArith.Qcanon]
z:95 [in Coq.ZArith.BinInt]
z:95 [in Coq.Classes.CRelationClasses]
z:95 [in Coq.setoid_ring.Ncring]
z:96 [in Coq.Reals.Rsqrt_def]
z:96 [in Coq.Numbers.NatInt.NZOrder]
z:97 [in Coq.Reals.Rsqrt_def]
z:98 [in Coq.QArith.Qcanon]
z:98 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
z:98 [in Coq.Reals.Rsqrt_def]
z:99 [in Coq.ZArith.BinInt]
z:99 [in Coq.Reals.Rsqrt_def]
z:99 [in Coq.Numbers.NatInt.NZOrder]


Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (68863 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (985 entries)
Binder Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (44709 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (761 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1497 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (570 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11380 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (976 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (603 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (298 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (460 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (476 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (811 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1157 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4018 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (162 entries)