Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (73252 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1016 entries)
Binder Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (47569 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (800 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1555 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (592 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11846 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (959 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (629 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (308 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (475 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (494 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (912 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1503 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4428 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (166 entries)

Q (binder)

qe:29 [in Coq.nsatz.NsatzTactic]
qe:59 [in Coq.nsatz.NsatzTactic]
qn:131 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
qPos:332 [in Coq.Reals.Abstract.ConstructiveReals]
QP':114 [in Coq.setoid_ring.Ring_polynom]
QP':116 [in Coq.micromega.EnvRing]
QQ':111 [in Coq.setoid_ring.Ring_polynom]
QQ':112 [in Coq.setoid_ring.Ring_polynom]
QQ':113 [in Coq.micromega.EnvRing]
QQ':114 [in Coq.micromega.EnvRing]
qrd:61 [in Coq.ZArith.Zpower]
qr:259 [in Coq.ZArith.Zdiv]
qr:37 [in Coq.ZArith.Zdiv]
qr:66 [in Coq.ZArith.Zpower]
qs:74 [in Coq.btauto.Algebra]
qs:88 [in Coq.btauto.Algebra]
qs:93 [in Coq.btauto.Algebra]
qs:97 [in Coq.btauto.Algebra]
quo:123 [in Coq.Numbers.Cyclic.Int31.Int31]
quo:137 [in Coq.Numbers.Cyclic.Int31.Int31]
quo:162 [in Coq.Numbers.Cyclic.Int63.Uint63]
quo:178 [in Coq.Numbers.Cyclic.Int63.Uint63]
quo:398 [in Coq.Numbers.Cyclic.Int63.Uint63]
Q_hprop:1038 [in Coq.Init.Specif]
Q_hprop:914 [in Coq.Init.Specif]
Q_hprop:776 [in Coq.Init.Specif]
Q_hprop:652 [in Coq.Init.Specif]
Q_hprop:938 [in Coq.Init.Logic]
Q_hprop:804 [in Coq.Init.Logic]
Q_hprop:783 [in Coq.Init.Logic]
Q_hprop:771 [in Coq.Init.Logic]
q':10 [in Coq.QArith.Qcanon]
q':10 [in Coq.QArith.Qreduction]
q':125 [in Coq.PArith.BinPos]
q':14 [in Coq.QArith.Qcanon]
q':152 [in Coq.Numbers.Cyclic.Int63.Uint63]
q':216 [in Coq.Init.Specif]
q':226 [in Coq.Init.Specif]
q':27 [in Coq.QArith.Qreduction]
q':29 [in Coq.QArith.Qreduction]
q':31 [in Coq.Numbers.HexadecimalR]
q':31 [in Coq.Numbers.DecimalR]
q':45 [in Coq.Numbers.DecimalQ]
q':45 [in Coq.Numbers.HexadecimalQ]
q':79 [in Coq.Arith.PeanoNat]
q':8 [in Coq.QArith.Qcanon]
q0:150 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:152 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:158 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:160 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:162 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:164 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:170 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:172 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:174 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:176 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:177 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:178 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:180 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:182 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q1:101 [in Coq.micromega.ZifyClasses]
q1:105 [in Coq.micromega.ZifyClasses]
q1:12 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q1:14 [in Coq.Numbers.NatInt.NZDiv]
Q1:158 [in Coq.micromega.EnvRing]
Q1:165 [in Coq.setoid_ring.Ring_polynom]
q1:18 [in Coq.Numbers.NatInt.NZDiv]
q1:2 [in Coq.QArith.Qreduction]
q1:22 [in Coq.Numbers.NatInt.NZDiv]
q1:34 [in Coq.micromega.QMicromega]
q1:37 [in Coq.micromega.QMicromega]
q1:39 [in Coq.micromega.ZMicromega]
q1:41 [in Coq.ZArith.Zdiv]
q1:43 [in Coq.micromega.QMicromega]
q1:45 [in Coq.micromega.ZMicromega]
q1:46 [in Coq.ZArith.Zdiv]
q1:53 [in Coq.setoid_ring.Field_theory]
q1:54 [in Coq.micromega.ZifyClasses]
q1:6 [in Coq.Numbers.Natural.Abstract.NDiv]
q1:6 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
q1:60 [in Coq.micromega.ZifyClasses]
q1:7 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
q1:83 [in Coq.micromega.RMicromega]
q2:102 [in Coq.micromega.ZifyClasses]
Q2:122 [in Coq.micromega.EnvRing]
q2:13 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q2:15 [in Coq.Numbers.NatInt.NZDiv]
q2:19 [in Coq.Numbers.NatInt.NZDiv]
q2:23 [in Coq.Numbers.NatInt.NZDiv]
q2:3 [in Coq.QArith.Qreduction]
q2:35 [in Coq.micromega.QMicromega]
q2:38 [in Coq.micromega.QMicromega]
q2:40 [in Coq.micromega.ZMicromega]
q2:42 [in Coq.ZArith.Zdiv]
q2:44 [in Coq.micromega.QMicromega]
q2:46 [in Coq.micromega.ZMicromega]
q2:47 [in Coq.ZArith.Zdiv]
q2:54 [in Coq.setoid_ring.Field_theory]
q2:55 [in Coq.micromega.ZifyClasses]
q2:7 [in Coq.Numbers.Natural.Abstract.NDiv]
q2:7 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
q2:8 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
q2:84 [in Coq.micromega.RMicromega]
q:1 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
q:1 [in Coq.QArith.Qreduction]
q:10 [in Coq.Numbers.NatInt.NZAddOrder]
q:10 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
q:10 [in Coq.NArith.BinNat]
Q:10 [in Coq.Logic.Classical_Prop]
q:10 [in Coq.Reals.ClassicalConstructiveReals]
q:100 [in Coq.FSets.FSetDecide]
q:100 [in Coq.MSets.MSetDecide]
q:100 [in Coq.Reals.ClassicalDedekindReals]
Q:1000 [in Coq.Lists.List]
Q:1002 [in Coq.Init.Specif]
Q:1004 [in Coq.Lists.List]
Q:1008 [in Coq.Lists.List]
q:101 [in Coq.Reals.Abstract.ConstructiveLUB]
q:101 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
Q:101 [in Coq.Init.Specif]
q:101 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:101 [in Coq.Reals.Rdefinitions]
q:1014 [in Coq.Init.Specif]
Q:1018 [in Coq.Init.Specif]
q:102 [in Coq.Reals.Rdefinitions]
q:102 [in Coq.Reals.ClassicalDedekindReals]
Q:1026 [in Coq.Init.Specif]
q:103 [in Coq.Reals.Abstract.ConstructiveLUB]
q:103 [in Coq.PArith.BinPos]
q:103 [in Coq.ZArith.Znumtheory]
Q:1034 [in Coq.Init.Specif]
q:1037 [in Coq.Init.Specif]
q:104 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
Q:104 [in Coq.Logic.Eqdep_dec]
q:104 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:105 [in Coq.ZArith.BinIntDef]
q:105 [in Coq.Reals.Rtrigo1]
Q:105 [in Coq.Init.Specif]
q:105 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:1051 [in Coq.Init.Specif]
Q:1057 [in Coq.Init.Specif]
q:106 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:106 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:106 [in Coq.Reals.Abstract.ConstructiveMinMax]
q:106 [in Coq.Reals.ClassicalDedekindReals]
q:107 [in Coq.Reals.Rtrigo1]
q:107 [in Coq.Logic.Hurkens]
q:108 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:108 [in Coq.ZArith.BinIntDef]
Q:108 [in Coq.Logic.EqdepFacts]
Q:108 [in Coq.ssr.ssrbool]
q:108 [in Coq.Logic.Hurkens]
q:109 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
q:109 [in Coq.Reals.Rtrigo1]
q:109 [in Coq.Arith.Wf_nat]
Q:109 [in Coq.ssr.ssreflect]
q:109 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:109 [in Coq.Reals.ClassicalDedekindReals]
q:11 [in Coq.QArith.Qcanon]
q:11 [in Coq.Logic.EqdepFacts]
Q:11 [in Coq.Logic.Berardi]
Q:11 [in Coq.Logic.PropExtensionalityFacts]
q:11 [in Coq.Arith.Euclid]
q:110 [in Coq.ZArith.BinIntDef]
q:110 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:110 [in Coq.Reals.Abstract.ConstructiveMinMax]
q:111 [in Coq.Reals.Rtrigo1]
Q:112 [in Coq.Logic.EqdepFacts]
Q:112 [in Coq.ssr.ssrbool]
q:112 [in Coq.ZArith.Zdiv]
q:112 [in Coq.Reals.ClassicalDedekindReals]
Q:113 [in Coq.setoid_ring.Ncring_polynom]
q:113 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:113 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Q:114 [in Coq.ssr.ssrbool]
q:114 [in Coq.Init.Nat]
q:115 [in Coq.ZArith.BinIntDef]
q:115 [in Coq.PArith.BinPos]
Q:115 [in Coq.Init.Specif]
q:115 [in Coq.ZArith.Zdiv]
q:115 [in Coq.Vectors.Fin]
q:115 [in Coq.QArith.QArith_base]
q:116 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:116 [in Coq.ZArith.Znumtheory]
q:117 [in Coq.QArith.Qcanon]
q:117 [in Coq.Arith.Wf_nat]
q:118 [in Coq.ZArith.Zdiv]
q:118 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:118 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
q:119 [in Coq.QArith.Qcanon]
Q:119 [in Coq.Init.Specif]
q:12 [in Coq.QArith.Qcanon]
q:12 [in Coq.Numbers.Natural.Abstract.NDiv]
Q:12 [in Coq.Logic.Classical_Prop]
q:12 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:12 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
q:12 [in Coq.QArith.Qreduction]
q:12 [in Coq.Reals.Cauchy.QExtra]
q:12 [in Coq.Reals.ClassicalDedekindReals]
q:120 [in Coq.ZArith.Zdiv]
q:121 [in Coq.QArith.Qcanon]
q:122 [in Coq.Init.Nat]
q:122 [in Coq.Reals.Rbasic_fun]
q:123 [in Coq.ZArith.BinIntDef]
Q:123 [in Coq.setoid_ring.Ncring_polynom]
q:123 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
q:124 [in Coq.PArith.BinPos]
q:124 [in Coq.PArith.BinPosDef]
q:125 [in Coq.ZArith.BinIntDef]
q:125 [in Coq.Arith.Wf_nat]
q:125 [in Coq.ZArith.Znat]
q:127 [in Coq.Logic.Eqdep_dec]
q:127 [in Coq.ZArith.BinIntDef]
q:127 [in Coq.ZArith.BinInt]
q:127 [in Coq.ZArith.Znat]
Q:128 [in Coq.ssr.ssrbool]
q:129 [in Coq.ZArith.BinIntDef]
q:129 [in Coq.ZArith.BinInt]
q:129 [in Coq.Floats.SpecFloat]
q:129 [in Coq.PArith.BinPosDef]
q:13 [in Coq.QArith.Qcanon]
q:13 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
q:13 [in Coq.PArith.Pnat]
q:13 [in Coq.Logic.HLevels]
q:13 [in Coq.Structures.EqualitiesFacts]
q:13 [in Coq.Reals.Cauchy.QExtra]
q:13 [in Coq.rtauto.Rtauto]
q:131 [in Coq.setoid_ring.Ring_polynom]
Q:131 [in Coq.Init.Specif]
q:131 [in Coq.ZArith.Znat]
Q:133 [in Coq.Logic.Eqdep_dec]
q:133 [in Coq.ZArith.Znat]
q:134 [in Coq.PArith.BinPos]
q:134 [in Coq.micromega.OrderedRing]
q:134 [in Coq.PArith.BinPosDef]
q:135 [in Coq.QArith.Qcanon]
q:136 [in Coq.PArith.BinPos]
Q:136 [in Coq.ssr.ssrbool]
Q:137 [in Coq.Init.Specif]
q:137 [in Coq.QArith.QArith_base]
q:137 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:138 [in Coq.PArith.BinPos]
q:138 [in Coq.ZArith.BinInt]
q:138 [in Coq.micromega.OrderedRing]
q:138 [in Coq.QArith.QArith_base]
q:139 [in Coq.PArith.BinPosDef]
q:14 [in Coq.setoid_ring.Field_theory]
Q:14 [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
q:14 [in Coq.Numbers.Natural.Abstract.NMulOrder]
Q:14 [in Coq.Logic.Classical_Prop]
q:14 [in Coq.QArith.Qreduction]
q:14 [in Coq.Reals.Cauchy.QExtra]
q:14 [in Coq.Reals.ClassicalDedekindReals]
q:140 [in Coq.PArith.BinPos]
q:141 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:142 [in Coq.ZArith.BinInt]
q:142 [in Coq.micromega.OrderedRing]
q:143 [in Coq.PArith.BinPos]
Q:143 [in Coq.ssr.ssrbool]
q:146 [in Coq.PArith.BinPos]
q:146 [in Coq.micromega.OrderedRing]
q:148 [in Coq.QArith.QArith_base]
q:148 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:149 [in Coq.PArith.BinPos]
q:149 [in Coq.QArith.QArith_base]
q:15 [in Coq.Logic.EqdepFacts]
q:15 [in Coq.ZArith.Zpow_facts]
q:15 [in Coq.PArith.Pnat]
q:15 [in Coq.Logic.ProofIrrelevanceFacts]
q:15 [in Coq.Reals.Cauchy.QExtra]
q:15 [in Coq.Reals.ClassicalDedekindReals]
q:150 [in Coq.Numbers.Cyclic.Int63.Uint63]
q:151 [in Coq.PArith.BinPos]
q:152 [in Coq.Logic.Eqdep_dec]
q:153 [in Coq.PArith.BinPos]
q:156 [in Coq.PArith.BinPos]
q:156 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:158 [in Coq.PArith.BinPos]
q:158 [in Coq.NArith.BinNat]
q:16 [in Coq.Numbers.Natural.Abstract.NDiv]
q:16 [in Coq.QArith.Qfield]
q:16 [in Coq.QArith.Qabs]
Q:16 [in Coq.Logic.Classical_Prop]
q:16 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
Q:16 [in Coq.Logic.Diaconescu]
q:16 [in Coq.Arith.Euclid]
q:16 [in Coq.Reals.Cauchy.QExtra]
q:16 [in Coq.Reals.ClassicalDedekindReals]
q:160 [in Coq.ZArith.BinInt]
q:161 [in Coq.PArith.BinPos]
q:162 [in Coq.NArith.BinNat]
q:163 [in Coq.FSets.FMapPositive]
q:164 [in Coq.PArith.BinPos]
q:164 [in Coq.Structures.GenericMinMax]
q:166 [in Coq.Vectors.Fin]
q:167 [in Coq.PArith.BinPos]
q:167 [in Coq.ZArith.Zorder]
q:168 [in Coq.FSets.FMapPositive]
q:168 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
Q:17 [in Coq.FSets.FSetDecide]
q:17 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
q:17 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:17 [in Coq.PArith.Pnat]
Q:17 [in Coq.MSets.MSetDecide]
q:17 [in Coq.Arith.Cantor]
q:17 [in Coq.ZArith.Zdiv]
q:17 [in Coq.Reals.Cauchy.QExtra]
q:170 [in Coq.PArith.BinPos]
q:171 [in Coq.ZArith.Zorder]
Q:172 [in Coq.micromega.ZifyClasses]
q:172 [in Coq.PArith.BinPos]
q:173 [in Coq.Vectors.Fin]
Q:174 [in Coq.micromega.ZifyClasses]
Q:176 [in Coq.Logic.ChoiceFacts]
q:176 [in Coq.Vectors.Fin]
q:176 [in Coq.ZArith.Znumtheory]
q:177 [in Coq.ZArith.BinInt]
Q:179 [in Coq.micromega.ZifyClasses]
q:18 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:18 [in Coq.Numbers.Natural.Abstract.NMulOrder]
Q:18 [in Coq.Logic.Classical_Prop]
Q:18 [in Coq.Logic.Diaconescu]
q:18 [in Coq.QArith.Qreduction]
q:18 [in Coq.Reals.Cauchy.QExtra]
q:180 [in Coq.setoid_ring.Ring_theory]
q:180 [in Coq.QArith.QArith_base]
Q:181 [in Coq.ssr.ssrfun]
q:181 [in Coq.ZArith.Znumtheory]
q:183 [in Coq.ZArith.Znumtheory]
q:183 [in Coq.QArith.QArith_base]
Q:185 [in Coq.ssr.ssrbool]
Q:187 [in Coq.Logic.ChoiceFacts]
q:189 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:189 [in Coq.micromega.ZMicromega]
Q:19 [in Coq.FSets.FSetDecide]
q:19 [in Coq.Numbers.HexadecimalPos]
q:19 [in Coq.ZArith.BinInt]
q:19 [in Coq.PArith.Pnat]
Q:19 [in Coq.MSets.MSetDecide]
Q:19 [in Coq.Init.Specif]
q:19 [in Coq.ZArith.Zpow_alt]
q:19 [in Coq.Numbers.DecimalPos]
q:19 [in Coq.Reals.Cauchy.QExtra]
q:190 [in Coq.Init.Specif]
q:191 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
Q:192 [in Coq.Logic.ChoiceFacts]
q:193 [in Coq.ZArith.Zorder]
q:193 [in Coq.Structures.OrderedType]
q:193 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:194 [in Coq.ZArith.BinInt]
q:194 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:194 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
Q:195 [in Coq.ssr.ssrfun]
q:195 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
q:196 [in Coq.PArith.BinPos]
q:196 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:197 [in Coq.ZArith.BinInt]
q:197 [in Coq.ZArith.Zorder]
q:198 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
Q:2 [in Coq.FSets.FSetDecide]
q:2 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
Q:2 [in Coq.Logic.PropExtensionality]
Q:2 [in Coq.MSets.MSetDecide]
Q:2 [in Coq.ssr.ssrfun]
q:2 [in Coq.rtauto.Bintree]
q:2 [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
Q:2 [in Coq.Logic.Diaconescu]
q:2 [in Coq.Numbers.NatInt.NZMulOrder]
q:2 [in Coq.Reals.Cauchy.PosExtra]
q:20 [in Coq.Numbers.Natural.Abstract.NDiv]
q:20 [in Coq.Numbers.NatInt.NZAddOrder]
q:20 [in Coq.btauto.Algebra]
q:20 [in Coq.setoid_ring.Field_theory]
Q:20 [in Coq.Logic.Classical_Prop]
q:20 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
Q:20 [in Coq.Logic.Diaconescu]
q:20 [in Coq.QArith.Qreduction]
q:20 [in Coq.Reals.Cauchy.QExtra]
q:20 [in Coq.Reals.ClassicalDedekindReals]
q:20 [in Coq.Reals.ClassicalConstructiveReals]
q:20 [in Coq.QArith.QArith_base]
Q:200 [in Coq.setoid_ring.Ring_polynom]
q:200 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:203 [in Coq.Init.Specif]
q:206 [in Coq.ZArith.Znumtheory]
Q:21 [in Coq.FSets.FSetDecide]
q:21 [in Coq.Numbers.Natural.Abstract.NDiv0]
q:21 [in Coq.ZArith.BinInt]
q:21 [in Coq.PArith.Pnat]
Q:21 [in Coq.MSets.MSetDecide]
q:21 [in Coq.Logic.ProofIrrelevanceFacts]
Q:21 [in Coq.Logic.HLevels]
q:21 [in Coq.Reals.Cauchy.QExtra]
q:211 [in Coq.ZArith.Znumtheory]
q:214 [in Coq.Init.Specif]
q:215 [in Coq.PArith.BinPos]
Q:217 [in Coq.Logic.EqdepFacts]
q:218 [in Coq.PArith.BinPos]
q:22 [in Coq.Logic.EqdepFacts]
q:22 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:22 [in Coq.Reals.Abstract.ConstructiveLimits]
Q:22 [in Coq.Logic.Classical_Prop]
Q:22 [in Coq.Logic.Diaconescu]
q:22 [in Coq.Arith.Mult]
q:22 [in Coq.Reals.Abstract.ConstructiveMinMax]
q:22 [in Coq.QArith.Qreduction]
q:22 [in Coq.Reals.Cauchy.QExtra]
q:22 [in Coq.Reals.ClassicalConstructiveReals]
q:22 [in Coq.QArith.QArith_base]
q:22 [in Coq.rtauto.Rtauto]
q:220 [in Coq.PArith.BinPos]
Q:221 [in Coq.Logic.ClassicalFacts]
q:222 [in Coq.PArith.BinPos]
Q:223 [in Coq.Logic.EqdepFacts]
q:223 [in Coq.micromega.ZMicromega]
q:225 [in Coq.Init.Specif]
q:225 [in Coq.setoid_ring.Field_theory]
Q:226 [in Coq.setoid_ring.Ring_polynom]
Q:227 [in Coq.Logic.EqdepFacts]
q:228 [in Coq.PArith.BinPos]
Q:229 [in Coq.micromega.EnvRing]
q:23 [in Coq.PArith.BinPos]
q:23 [in Coq.PArith.Pnat]
q:23 [in Coq.Structures.DecidableType]
Q:23 [in Coq.Logic.HLevels]
q:23 [in Coq.Numbers.NatInt.NZMul]
q:23 [in Coq.QArith.Qreduction]
q:23 [in Coq.Reals.Cauchy.QExtra]
q:23 [in Coq.ZArith.Zcompare]
q:230 [in Coq.PArith.BinPos]
Q:231 [in Coq.Logic.EqdepFacts]
Q:233 [in Coq.Vectors.VectorSpec]
q:233 [in Coq.PArith.BinPos]
q:235 [in Coq.Init.Specif]
q:236 [in Coq.PArith.BinPos]
q:238 [in Coq.PArith.BinPos]
q:24 [in Coq.QArith.Qcanon]
q:24 [in Coq.Numbers.Natural.Abstract.NDiv0]
q:24 [in Coq.Numbers.NatInt.NZAddOrder]
q:24 [in Coq.ZArith.BinInt]
q:24 [in Coq.Reals.Abstract.ConstructiveLimits]
Q:24 [in Coq.Logic.Classical_Prop]
q:24 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:24 [in Coq.Reals.ClassicalDedekindReals]
q:24 [in Coq.QArith.QArith_base]
q:241 [in Coq.PArith.BinPos]
q:242 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
q:243 [in Coq.PArith.BinPos]
q:243 [in Coq.Init.Specif]
q:246 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
q:246 [in Coq.PArith.BinPos]
q:248 [in Coq.PArith.BinPos]
q:25 [in Coq.PArith.Pnat]
q:25 [in Coq.Reals.Abstract.ConstructiveAbs]
q:25 [in Coq.Numbers.NatInt.NZAdd]
q:25 [in Coq.Reals.Cauchy.QExtra]
q:250 [in Coq.PArith.BinPos]
q:250 [in Coq.Numbers.Cyclic.Int63.Uint63]
q:251 [in Coq.Init.Specif]
q:251 [in Coq.QArith.QArith_base]
q:255 [in Coq.Logic.EqdepFacts]
q:255 [in Coq.PArith.BinPos]
q:255 [in Coq.QArith.QArith_base]
q:256 [in Coq.Init.Specif]
q:257 [in Coq.QArith.QArith_base]
q:258 [in Coq.PArith.BinPos]
q:259 [in Coq.QArith.QArith_base]
q:26 [in Coq.QArith.Qcanon]
q:26 [in Coq.Reals.Abstract.ConstructiveLUB]
q:26 [in Coq.ZArith.BinInt]
Q:26 [in Coq.Logic.Classical_Prop]
q:26 [in Coq.QArith.Qpower]
q:26 [in Coq.QArith.Qreduction]
q:26 [in Coq.QArith.QArith_base]
q:260 [in Coq.ZArith.Zdiv]
q:261 [in Coq.PArith.BinPos]
q:261 [in Coq.QArith.QArith_base]
q:263 [in Coq.Logic.EqdepFacts]
q:263 [in Coq.PArith.BinPos]
q:265 [in Coq.PArith.BinPos]
Q:266 [in Coq.Arith.PeanoNat]
q:267 [in Coq.PArith.BinPos]
q:269 [in Coq.PArith.BinPos]
q:27 [in Coq.PArith.Pnat]
q:27 [in Coq.Numbers.NatInt.NZMul]
q:27 [in Coq.QArith.Qpower]
q:27 [in Coq.Reals.Cauchy.QExtra]
q:270 [in Coq.Logic.EqdepFacts]
q:271 [in Coq.PArith.BinPos]
Q:271 [in Coq.Arith.PeanoNat]
q:273 [in Coq.PArith.BinPos]
Q:273 [in Coq.Init.Specif]
q:275 [in Coq.PArith.BinPos]
q:275 [in Coq.Init.Specif]
Q:276 [in Coq.setoid_ring.Ring_polynom]
Q:276 [in Coq.Arith.PeanoNat]
q:277 [in Coq.PArith.BinPos]
q:279 [in Coq.PArith.BinPos]
q:28 [in Coq.QArith.Qcanon]
q:28 [in Coq.Reals.Abstract.ConstructiveLUB]
q:28 [in Coq.PArith.BinPos]
q:28 [in Coq.Numbers.NatInt.NZAddOrder]
q:28 [in Coq.ZArith.BinInt]
q:28 [in Coq.ZArith.Zpow_facts]
q:28 [in Coq.btauto.Algebra]
q:28 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
q:28 [in Coq.Numbers.NatInt.NZDiv]
q:28 [in Coq.Arith.Between]
q:28 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:28 [in Coq.QArith.Qreduction]
q:28 [in Coq.Reals.ClassicalDedekindReals]
q:28 [in Coq.Reals.ClassicalConstructiveReals]
q:28 [in Coq.QArith.QArith_base]
q:281 [in Coq.PArith.BinPos]
Q:281 [in Coq.Arith.PeanoNat]
q:283 [in Coq.PArith.BinPos]
Q:283 [in Coq.setoid_ring.Ring_polynom]
Q:283 [in Coq.Init.Specif]
q:284 [in Coq.NArith.BinNat]
q:285 [in Coq.QArith.QArith_base]
q:287 [in Coq.PArith.BinPos]
q:288 [in Coq.QArith.QArith_base]
q:289 [in Coq.PArith.BinPos]
Q:289 [in Coq.Init.Specif]
q:29 [in Coq.Logic.EqdepFacts]
q:29 [in Coq.PArith.Pnat]
q:29 [in Coq.Numbers.NatInt.NZAdd]
q:29 [in Coq.Reals.Cauchy.QExtra]
q:290 [in Coq.QArith.QArith_base]
q:292 [in Coq.PArith.BinPos]
q:292 [in Coq.QArith.QArith_base]
q:294 [in Coq.QArith.QArith_base]
Q:295 [in Coq.Init.Specif]
q:297 [in Coq.PArith.BinPos]
q:297 [in Coq.Init.Specif]
Q:299 [in Coq.micromega.EnvRing]
q:3 [in Coq.Strings.OctalString]
q:3 [in Coq.Strings.HexString]
q:3 [in Coq.PArith.Pnat]
Q:3 [in Coq.Logic.ClassicalChoice]
q:3 [in Coq.ZArith.Zdiv]
q:3 [in Coq.Strings.BinaryString]
q:3 [in Coq.Logic.HLevels]
Q:3 [in Coq.Logic.Eqdep]
q:3 [in Coq.ZArith.Znumtheory]
q:3 [in Coq.Reals.Cauchy.PosExtra]
q:30 [in Coq.QArith.Qcanon]
q:30 [in Coq.Reals.Abstract.ConstructiveLUB]
q:30 [in Coq.PArith.BinPos]
q:30 [in Coq.btauto.Algebra]
q:30 [in Coq.Numbers.HexadecimalR]
q:30 [in Coq.Numbers.DecimalR]
q:30 [in Coq.Reals.ClassicalConstructiveReals]
q:30 [in Coq.QArith.QArith_base]
q:300 [in Coq.PArith.BinPos]
q:302 [in Coq.PArith.BinPos]
Q:303 [in Coq.Arith.PeanoNat]
q:304 [in Coq.PArith.BinPos]
Q:304 [in Coq.Init.Logic]
Q:305 [in Coq.Init.Specif]
q:306 [in Coq.PArith.BinPos]
q:307 [in Coq.Init.Specif]
q:308 [in Coq.PArith.BinPos]
q:308 [in Coq.ZArith.BinInt]
Q:308 [in Coq.Arith.PeanoNat]
q:31 [in Coq.Arith.Between]
q:31 [in Coq.Structures.EqualitiesFacts]
q:31 [in Coq.Reals.Cauchy.QExtra]
q:31 [in Coq.Reals.ClassicalDedekindReals]
q:310 [in Coq.PArith.BinPos]
q:310 [in Coq.ZArith.BinInt]
q:312 [in Coq.PArith.BinPos]
q:314 [in Coq.PArith.BinPos]
Q:314 [in Coq.Init.Logic]
q:316 [in Coq.PArith.BinPos]
Q:316 [in Coq.Init.Specif]
q:317 [in Coq.ZArith.BinInt]
q:318 [in Coq.PArith.BinPos]
q:318 [in Coq.Init.Specif]
q:319 [in Coq.ZArith.BinInt]
q:32 [in Coq.QArith.Qcanon]
q:32 [in Coq.Structures.OrdersLists]
q:32 [in Coq.Reals.Abstract.ConstructiveLUB]
q:32 [in Coq.Logic.EqdepFacts]
q:32 [in Coq.PArith.BinPos]
q:32 [in Coq.btauto.Algebra]
Q:32 [in Coq.Init.Datatypes]
q:32 [in Coq.Numbers.NatInt.NZDiv]
q:32 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:320 [in Coq.Reals.Abstract.ConstructiveReals]
q:320 [in Coq.PArith.BinPos]
q:321 [in Coq.ZArith.BinInt]
q:322 [in Coq.PArith.BinPos]
q:323 [in Coq.Reals.Abstract.ConstructiveReals]
q:324 [in Coq.PArith.BinPos]
q:324 [in Coq.ZArith.BinInt]
q:326 [in Coq.ZArith.BinInt]
Q:326 [in Coq.Init.Specif]
q:327 [in Coq.Reals.Abstract.ConstructiveReals]
q:327 [in Coq.PArith.BinPos]
q:328 [in Coq.ZArith.BinInt]
q:329 [in Coq.Reals.Abstract.ConstructiveReals]
q:33 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:33 [in Coq.PArith.Pnat]
q:33 [in Coq.Numbers.HexadecimalR]
Q:33 [in Coq.Logic.Classical_Prop]
q:33 [in Coq.Numbers.DecimalR]
q:331 [in Coq.Reals.Abstract.ConstructiveReals]
q:331 [in Coq.ZArith.BinInt]
q:332 [in Coq.PArith.BinPos]
q:332 [in Coq.Init.Specif]
q:333 [in Coq.ZArith.BinInt]
q:334 [in Coq.PArith.BinPos]
q:335 [in Coq.ZArith.BinInt]
q:336 [in Coq.PArith.BinPos]
q:337 [in Coq.ZArith.BinInt]
Q:338 [in Coq.Init.Specif]
q:339 [in Coq.ZArith.BinInt]
q:34 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:34 [in Coq.QArith.Qcanon]
q:34 [in Coq.Structures.OrdersLists]
q:34 [in Coq.PArith.BinPos]
q:34 [in Coq.btauto.Algebra]
Q:34 [in Coq.ssr.ssrbool]
q:34 [in Coq.Arith.Between]
q:34 [in Coq.QArith.Qpower]
q:34 [in Coq.Reals.Cauchy.QExtra]
q:341 [in Coq.ZArith.BinInt]
q:344 [in Coq.ZArith.BinInt]
Q:344 [in Coq.Init.Specif]
q:346 [in Coq.ZArith.BinInt]
q:349 [in Coq.Logic.ChoiceFacts]
q:349 [in Coq.Init.Specif]
q:35 [in Coq.PArith.Pnat]
q:350 [in Coq.ZArith.BinInt]
q:351 [in Coq.PArith.BinPos]
q:351 [in Coq.Logic.ChoiceFacts]
q:352 [in Coq.ZArith.BinInt]
q:354 [in Coq.ZArith.BinInt]
q:356 [in Coq.ZArith.BinInt]
Q:357 [in Coq.Logic.ChoiceFacts]
Q:359 [in Coq.Logic.ChoiceFacts]
q:36 [in Coq.PArith.BinPos]
Q:36 [in Coq.ssr.ssrbool]
q:36 [in Coq.Numbers.NatInt.NZDiv]
q:36 [in Coq.QArith.Qpower]
q:36 [in Coq.Reals.ClassicalConstructiveReals]
Q:361 [in Coq.Logic.ChoiceFacts]
q:361 [in Coq.Init.Specif]
q:362 [in Coq.ZArith.BinInt]
q:364 [in Coq.ZArith.BinInt]
Q:364 [in Coq.Logic.ChoiceFacts]
q:365 [in Coq.PArith.BinPos]
q:366 [in Coq.ZArith.BinInt]
Q:366 [in Coq.Init.Specif]
q:367 [in Coq.PArith.BinPos]
q:368 [in Coq.ZArith.BinInt]
q:37 [in Coq.Reals.Abstract.ConstructiveReals]
q:37 [in Coq.Arith.Between]
q:370 [in Coq.PArith.BinPos]
q:370 [in Coq.ZArith.BinInt]
q:372 [in Coq.ZArith.BinInt]
q:373 [in Coq.PArith.BinPos]
q:375 [in Coq.PArith.BinPos]
q:378 [in Coq.PArith.BinPos]
q:38 [in Coq.Logic.EqdepFacts]
q:38 [in Coq.PArith.BinPos]
q:38 [in Coq.ZArith.Zdiv]
q:38 [in Coq.QArith.Qpower]
q:38 [in Coq.Reals.ClassicalDedekindReals]
q:380 [in Coq.ZArith.BinInt]
q:381 [in Coq.PArith.BinPos]
q:382 [in Coq.ZArith.BinInt]
q:384 [in Coq.ZArith.BinInt]
q:384 [in Coq.QArith.QArith_base]
q:385 [in Coq.PArith.BinPos]
q:386 [in Coq.ZArith.BinInt]
q:388 [in Coq.PArith.BinPos]
q:39 [in Coq.ZArith.BinInt]
q:39 [in Coq.micromega.RMicromega]
q:391 [in Coq.PArith.BinPos]
q:395 [in Coq.PArith.BinPos]
q:398 [in Coq.PArith.BinPos]
q:4 [in Coq.QArith.Qcanon]
q:4 [in Coq.Numbers.Integer.Abstract.ZMulOrder]
q:4 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:40 [in Coq.Reals.Abstract.ConstructiveReals]
q:40 [in Coq.Numbers.Natural.Abstract.NLcm]
q:40 [in Coq.ZArith.Zbool]
q:40 [in Coq.Arith.Between]
q:40 [in Coq.QArith.Qpower]
q:401 [in Coq.PArith.BinPos]
q:404 [in Coq.PArith.BinPos]
q:406 [in Coq.Numbers.Cyclic.Int63.Uint63]
q:407 [in Coq.PArith.BinPos]
q:407 [in Coq.Init.Specif]
Q:41 [in Coq.Logic.ConstructiveEpsilon]
q:41 [in Coq.PArith.Pnat]
q:41 [in Coq.micromega.RMicromega]
Q:410 [in Coq.Init.Logic]
q:411 [in Coq.PArith.BinPos]
q:414 [in Coq.PArith.BinPos]
q:414 [in Coq.Init.Specif]
Q:415 [in Coq.Init.Logic]
q:417 [in Coq.PArith.BinPos]
q:42 [in Coq.PArith.BinPos]
q:42 [in Coq.btauto.Algebra]
q:42 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:42 [in Coq.Reals.ClassicalDedekindReals]
q:421 [in Coq.PArith.BinPos]
q:422 [in Coq.Init.Specif]
q:423 [in Coq.PArith.BinPos]
q:427 [in Coq.setoid_ring.Field_theory]
q:429 [in Coq.PArith.BinPos]
q:43 [in Coq.Structures.OrdersLists]
Q:43 [in Coq.setoid_ring.Ring_polynom]
q:43 [in Coq.Program.Equality]
q:43 [in Coq.Arith.Between]
q:43 [in Coq.micromega.RMicromega]
q:43 [in Coq.Structures.EqualitiesFacts]
q:430 [in Coq.Init.Specif]
q:431 [in Coq.PArith.BinPos]
q:434 [in Coq.PArith.BinPos]
Q:436 [in Coq.Init.Specif]
q:436 [in Coq.setoid_ring.Field_theory]
q:437 [in Coq.PArith.BinPos]
q:438 [in Coq.Init.Specif]
q:439 [in Coq.PArith.BinPos]
q:44 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:44 [in Coq.Logic.EqdepFacts]
q:44 [in Coq.Numbers.NatInt.NZAddOrder]
q:44 [in Coq.Numbers.Natural.Abstract.NLcm]
q:44 [in Coq.Numbers.DecimalQ]
q:44 [in Coq.Numbers.HexadecimalQ]
q:441 [in Coq.PArith.BinPos]
Q:442 [in Coq.Init.Logic]
q:444 [in Coq.PArith.BinPos]
q:445 [in Coq.ZArith.BinInt]
Q:446 [in Coq.Init.Specif]
q:447 [in Coq.PArith.BinPos]
q:45 [in Coq.PArith.BinPos]
Q:45 [in Coq.micromega.EnvRing]
q:45 [in Coq.micromega.RMicromega]
q:450 [in Coq.PArith.BinPos]
Q:452 [in Coq.Init.Specif]
q:453 [in Coq.PArith.BinPos]
q:456 [in Coq.PArith.BinPos]
q:457 [in Coq.ssr.ssrbool]
Q:458 [in Coq.Init.Specif]
q:46 [in Coq.Reals.Abstract.ConstructiveReals]
Q:46 [in Coq.Logic.ConstructiveEpsilon]
q:46 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:46 [in Coq.Structures.EqualitiesFacts]
q:460 [in Coq.Init.Specif]
q:461 [in Coq.PArith.BinPos]
q:463 [in Coq.ssr.ssrbool]
q:464 [in Coq.PArith.BinPos]
q:467 [in Coq.PArith.BinPos]
Q:468 [in Coq.Init.Specif]
q:47 [in Coq.Numbers.DecimalQ]
q:47 [in Coq.ZArith.Zquot]
Q:47 [in Coq.setoid_ring.Ncring_polynom]
q:47 [in Coq.Logic.HLevels]
q:47 [in Coq.Numbers.HexadecimalQ]
q:470 [in Coq.Init.Specif]
q:478 [in Coq.PArith.BinPos]
Q:479 [in Coq.Init.Specif]
q:48 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:48 [in Coq.PArith.BinPos]
q:48 [in Coq.Numbers.NatInt.NZAddOrder]
q:48 [in Coq.micromega.RMicromega]
q:480 [in Coq.PArith.BinPos]
q:481 [in Coq.Init.Specif]
q:482 [in Coq.PArith.BinPos]
q:484 [in Coq.PArith.BinPos]
q:487 [in Coq.PArith.BinPos]
Q:489 [in Coq.Init.Specif]
q:49 [in Coq.Reals.Abstract.ConstructiveReals]
q:493 [in Coq.Init.Logic]
q:495 [in Coq.Init.Specif]
q:499 [in Coq.ssr.ssrbool]
q:5 [in Coq.QArith.Qcanon]
Q:5 [in Coq.FSets.FSetDecide]
q:5 [in Coq.Logic.EqdepFacts]
q:5 [in Coq.PArith.Pnat]
Q:5 [in Coq.MSets.MSetDecide]
q:5 [in Coq.Numbers.HexadecimalR]
q:5 [in Coq.Numbers.DecimalR]
q:5 [in Coq.NArith.Ndiv_def]
q:5 [in Coq.Arith.Euclid]
q:5 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:50 [in Coq.Structures.OrdersLists]
q:50 [in Coq.Logic.EqdepFacts]
q:50 [in Coq.ZArith.Zpow_facts]
q:500 [in Coq.Init.Logic]
Q:501 [in Coq.Init.Specif]
Q:507 [in Coq.Init.Specif]
q:508 [in Coq.Init.Logic]
q:51 [in Coq.PArith.BinPos]
q:51 [in Coq.setoid_ring.Field_theory]
q:51 [in Coq.ZArith.Zquot]
q:512 [in Coq.Init.Specif]
q:513 [in Coq.ZArith.BinInt]
q:515 [in Coq.ZArith.BinInt]
q:516 [in Coq.Init.Logic]
q:517 [in Coq.ZArith.BinInt]
q:52 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:52 [in Coq.Numbers.NatInt.NZAddOrder]
q:52 [in Coq.ZArith.Zdiv]
q:528 [in Coq.Init.Specif]
Q:528 [in Coq.Init.Logic]
q:53 [in Coq.Structures.OrdersLists]
q:53 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:53 [in Coq.ZArith.Zpow_facts]
q:530 [in Coq.Init.Logic]
Q:538 [in Coq.Init.Specif]
Q:539 [in Coq.Init.Logic]
q:54 [in Coq.QArith.Qcanon]
q:54 [in Coq.Reals.Abstract.ConstructiveLUB]
q:54 [in Coq.PArith.BinPos]
q:540 [in Coq.Reals.RIneq]
Q:544 [in Coq.ssr.ssrbool]
Q:545 [in Coq.Init.Logic]
Q:547 [in Coq.Init.Specif]
q:55 [in Coq.QArith.Qcanon]
Q:55 [in Coq.Init.Specif]
q:55 [in Coq.ZArith.Zquot]
Q:551 [in Coq.Init.Logic]
q:553 [in Coq.Init.Logic]
Q:556 [in Coq.Init.Specif]
q:558 [in Coq.PArith.BinPos]
q:56 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:56 [in Coq.Logic.EqdepFacts]
q:56 [in Coq.Numbers.NatInt.NZAddOrder]
q:56 [in Coq.ZArith.Zdiv]
q:56 [in Coq.Reals.ClassicalDedekindReals]
q:560 [in Coq.PArith.BinPos]
Q:561 [in Coq.Init.Logic]
q:563 [in Coq.Init.Logic]
Q:564 [in Coq.Init.Specif]
q:565 [in Coq.PArith.BinPos]
q:568 [in Coq.PArith.BinPos]
q:57 [in Coq.PArith.BinPos]
q:57 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
q:57 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:57 [in Coq.ZArith.Zpow_facts]
q:57 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:571 [in Coq.PArith.BinPos]
Q:572 [in Coq.Init.Specif]
Q:572 [in Coq.Init.Logic]
q:573 [in Coq.PArith.BinPos]
q:574 [in Coq.Init.Logic]
q:576 [in Coq.PArith.BinPos]
q:58 [in Coq.Structures.OrderedTypeEx]
Q:580 [in Coq.Init.Specif]
Q:582 [in Coq.Init.Logic]
q:587 [in Coq.Init.Logic]
q:59 [in Coq.Reals.Abstract.ConstructiveLUB]
q:59 [in Coq.ZArith.Zpow_facts]
Q:592 [in Coq.Init.Specif]
Q:593 [in Coq.Init.Logic]
Q:599 [in Coq.Init.Logic]
q:6 [in Coq.Arith.Le]
q:6 [in Coq.QArith.Qcanon]
q:6 [in Coq.Structures.OrdersEx]
q:6 [in Coq.Reals.Cauchy.ConstructiveExtra]
Q:6 [in Coq.Logic.Classical_Prop]
q:6 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
q:6 [in Coq.QArith.Qreduction]
q:6 [in Coq.QArith.QArith_base]
q:60 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:60 [in Coq.Numbers.Natural.Abstract.NDiv]
q:60 [in Coq.PArith.BinPos]
q:60 [in Coq.Numbers.NatInt.NZAddOrder]
q:60 [in Coq.ZArith.Zdiv]
q:60 [in Coq.Reals.ClassicalDedekindReals]
q:60 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
Q:602 [in Coq.Init.Specif]
q:604 [in Coq.Init.Logic]
q:607 [in Coq.PArith.BinPos]
q:61 [in Coq.Reals.Abstract.ConstructiveLUB]
q:61 [in Coq.NArith.BinNatDef]
q:610 [in Coq.Init.Specif]
q:612 [in Coq.PArith.BinPos]
q:614 [in Coq.PArith.BinPos]
Q:614 [in Coq.Init.Specif]
q:614 [in Coq.Init.Logic]
q:617 [in Coq.PArith.BinPos]
q:62 [in Coq.Logic.EqdepFacts]
q:62 [in Coq.Numbers.Natural.Abstract.NLcm0]
q:62 [in Coq.Numbers.NatInt.NZGcd]
q:62 [in Coq.Numbers.NatInt.NZMulOrder]
q:620 [in Coq.PArith.BinPos]
q:620 [in Coq.Init.Specif]
Q:624 [in Coq.Init.Specif]
q:63 [in Coq.Numbers.Natural.Abstract.NDiv]
q:63 [in Coq.PArith.BinPos]
q:63 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
Q:63 [in Coq.setoid_ring.Ncring_polynom]
q:631 [in Coq.Init.Logic]
q:632 [in Coq.Init.Specif]
Q:636 [in Coq.Init.Specif]
Q:64 [in Coq.Program.Wf]
q:64 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:64 [in Coq.ZArith.Zdiv]
q:64 [in Coq.NArith.BinNatDef]
q:64 [in Coq.Reals.ClassicalDedekindReals]
Q:641 [in Coq.Init.Logic]
q:644 [in Coq.Init.Specif]
Q:648 [in Coq.Init.Specif]
q:65 [in Coq.PArith.BinPos]
q:65 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:65 [in Coq.Logic.JMeq]
q:65 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:651 [in Coq.Init.Specif]
q:654 [in Coq.Init.Logic]
q:66 [in Coq.Numbers.Natural.Abstract.NDiv]
q:66 [in Coq.Numbers.Natural.Abstract.NLcm0]
q:66 [in Coq.Numbers.NatInt.NZMulOrder]
q:66 [in Coq.Reals.ClassicalDedekindReals]
Q:661 [in Coq.Init.Specif]
q:661 [in Coq.Init.Logic]
Q:666 [in Coq.Init.Logic]
q:67 [in Coq.PArith.BinPos]
Q:670 [in Coq.Init.Specif]
Q:675 [in Coq.Init.Logic]
q:677 [in Coq.Init.Specif]
q:68 [in Coq.Numbers.Natural.Abstract.NDiv]
q:68 [in Coq.Logic.EqdepFacts]
Q:68 [in Coq.Logic.Diaconescu]
Q:683 [in Coq.Init.Specif]
Q:683 [in Coq.Init.Logic]
q:69 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:69 [in Coq.Numbers.NatInt.NZGcd]
Q:691 [in Coq.Init.Specif]
Q:691 [in Coq.Init.Logic]
Q:699 [in Coq.Init.Specif]
Q:699 [in Coq.Init.Logic]
q:7 [in Coq.QArith.Qcanon]
q:7 [in Coq.Numbers.DecimalQ]
q:7 [in Coq.ZArith.Zdiv]
Q:7 [in Coq.Logic.ProofIrrelevanceFacts]
q:7 [in Coq.Numbers.HexadecimalQ]
Q:7 [in Coq.Logic.PropExtensionalityFacts]
q:70 [in Coq.Logic.JMeq]
q:70 [in Coq.Numbers.Natural.Abstract.NGcd]
q:70 [in Coq.Reals.ClassicalDedekindReals]
q:706 [in Coq.Init.Specif]
q:71 [in Coq.Numbers.Integer.Abstract.ZLcm]
Q:711 [in Coq.Init.Logic]
Q:712 [in Coq.Init.Specif]
q:719 [in Coq.Init.Specif]
q:72 [in Coq.Reals.Abstract.ConstructiveLUB]
q:72 [in Coq.Reals.Rbasic_fun]
Q:721 [in Coq.Init.Logic]
Q:725 [in Coq.Init.Specif]
q:727 [in Coq.Init.Logic]
q:73 [in Coq.Reals.ClassicalDedekindReals]
Q:730 [in Coq.ssr.ssrbool]
Q:731 [in Coq.Init.Logic]
q:734 [in Coq.Init.Specif]
q:739 [in Coq.Init.Logic]
q:74 [in Coq.ZArith.Zquot]
Q:740 [in Coq.Init.Specif]
Q:743 [in Coq.Init.Logic]
q:75 [in Coq.Numbers.Integer.Abstract.ZLcm]
q:75 [in Coq.ZArith.Znumtheory]
q:751 [in Coq.Init.Logic]
q:752 [in Coq.Init.Specif]
Q:755 [in Coq.Init.Logic]
Q:756 [in Coq.Init.Specif]
q:76 [in Coq.Reals.Abstract.ConstructiveLUB]
q:76 [in Coq.Logic.JMeq]
q:76 [in Coq.Numbers.Cyclic.Int31.Int31]
q:763 [in Coq.Init.Logic]
Q:764 [in Coq.Init.Specif]
Q:767 [in Coq.Init.Logic]
q:77 [in Coq.Arith.PeanoNat]
q:77 [in Coq.ZArith.Zpower]
q:77 [in Coq.ZArith.Zquot]
q:770 [in Coq.Init.Logic]
Q:772 [in Coq.Init.Specif]
q:775 [in Coq.Init.Specif]
q:78 [in Coq.Reals.Abstract.ConstructiveReals]
q:78 [in Coq.QArith.Qcanon]
Q:78 [in Coq.Logic.Eqdep_dec]
q:78 [in Coq.PArith.Pnat]
Q:78 [in Coq.Init.Specif]
q:78 [in Coq.Numbers.NatInt.NZDiv]
q:78 [in Coq.PArith.BinPosDef]
q:78 [in Coq.ZArith.Znumtheory]
Q:780 [in Coq.Init.Logic]
q:782 [in Coq.Init.Logic]
q:79 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
q:79 [in Coq.Numbers.Integer.Abstract.ZGcd]
q:79 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
q:791 [in Coq.Init.Specif]
Q:796 [in Coq.Init.Logic]
Q:797 [in Coq.Init.Specif]
q:799 [in Coq.Init.Logic]
q:8 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Q:8 [in Coq.Init.Specif]
q:8 [in Coq.Logic.HLevels]
Q:8 [in Coq.Logic.Classical_Prop]
q:8 [in Coq.Numbers.Integer.Abstract.ZMulOrder]
q:8 [in Coq.QArith.Qreduction]
q:80 [in Coq.Numbers.Cyclic.Int31.Int31]
q:80 [in Coq.ZArith.Zquot]
q:803 [in Coq.Init.Logic]
Q:809 [in Coq.Init.Specif]
q:81 [in Coq.PArith.Pnat]
q:81 [in Coq.Numbers.NatInt.NZDiv]
Q:814 [in Coq.Init.Logic]
Q:818 [in Coq.Init.Specif]
q:82 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
Q:823 [in Coq.Init.Logic]
Q:826 [in Coq.Init.Specif]
q:83 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
q:83 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
q:83 [in Coq.PArith.Pnat]
q:83 [in Coq.ZArith.Zpower]
q:83 [in Coq.QArith.Qpower]
Q:831 [in Coq.Init.Logic]
Q:834 [in Coq.Init.Specif]
q:838 [in Coq.Init.Logic]
q:84 [in Coq.Numbers.NatInt.NZDiv]
q:84 [in Coq.ZArith.Znumtheory]
Q:842 [in Coq.Init.Specif]
Q:845 [in Coq.Init.Logic]
q:85 [in Coq.PArith.Pnat]
q:85 [in Coq.ZArith.Zorder]
Q:85 [in Coq.Init.Logic]
Q:853 [in Coq.Init.Logic]
Q:854 [in Coq.Init.Specif]
q:86 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
q:86 [in Coq.Numbers.NatInt.NZDiv]
q:86 [in Coq.QArith.Qpower]
Q:861 [in Coq.Init.Logic]
Q:864 [in Coq.Init.Specif]
q:868 [in Coq.Init.Logic]
q:87 [in Coq.PArith.Pnat]
q:872 [in Coq.Init.Specif]
Q:874 [in Coq.Init.Logic]
Q:876 [in Coq.Init.Specif]
q:881 [in Coq.Init.Logic]
q:882 [in Coq.Init.Specif]
Q:886 [in Coq.Init.Specif]
Q:887 [in Coq.Init.Logic]
q:89 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
q:89 [in Coq.Arith.PeanoNat]
q:89 [in Coq.QArith.Qpower]
q:894 [in Coq.Init.Specif]
q:896 [in Coq.Init.Logic]
Q:898 [in Coq.Init.Specif]
q:9 [in Coq.QArith.Qcanon]
q:9 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
q:9 [in Coq.QArith.Qreduction]
Q:902 [in Coq.Init.Logic]
q:906 [in Coq.Init.Specif]
q:91 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
Q:91 [in Coq.Init.Logic]
q:91 [in Coq.Reals.ClassicalDedekindReals]
q:91 [in Coq.QArith.QArith_base]
Q:910 [in Coq.Init.Specif]
q:913 [in Coq.Init.Specif]
q:914 [in Coq.Init.Logic]
Q:918 [in Coq.Init.Logic]
q:92 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:92 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
Q:92 [in Coq.Init.Datatypes]
q:92 [in Coq.QArith.Qpower]
Q:923 [in Coq.Init.Specif]
Q:926 [in Coq.Init.Logic]
q:93 [in Coq.Reals.Abstract.ConstructiveLUB]
q:93 [in Coq.PArith.Pnat]
Q:932 [in Coq.Init.Specif]
Q:934 [in Coq.Init.Logic]
q:937 [in Coq.Init.Logic]
q:939 [in Coq.Init.Specif]
q:94 [in Coq.Reals.Abstract.ConstructiveLUB]
q:94 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
Q:945 [in Coq.Init.Specif]
q:95 [in Coq.ZArith.BinIntDef]
q:95 [in Coq.Reals.Abstract.ConstructiveLUB]
q:95 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:95 [in Coq.Reals.ClassicalDedekindReals]
q:951 [in Coq.Init.Logic]
Q:953 [in Coq.Init.Specif]
Q:957 [in Coq.Init.Logic]
Q:96 [in Coq.Program.Wf]
q:96 [in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:96 [in Coq.Reals.Abstract.ConstructiveLUB]
q:96 [in Coq.PArith.Pnat]
q:96 [in Coq.Init.Nat]
q:96 [in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
Q:961 [in Coq.Init.Specif]
q:968 [in Coq.Init.Specif]
q:97 [in Coq.Reals.Abstract.ConstructiveLUB]
q:97 [in Coq.PArith.BinPosDef]
Q:972 [in Coq.Lists.List]
Q:974 [in Coq.Init.Specif]
q:98 [in Coq.ZArith.BinIntDef]
q:98 [in Coq.PArith.BinPos]
q:98 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:98 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:98 [in Coq.Arith.PeanoNat]
q:98 [in Coq.Structures.GenericMinMax]
Q:98 [in Coq.setoid_ring.Ncring_polynom]
q:98 [in Coq.QArith.Qpower]
q:98 [in Coq.Reals.Abstract.ConstructiveMinMax]
q:981 [in Coq.Init.Specif]
Q:987 [in Coq.Init.Specif]
Q:988 [in Coq.Lists.List]
q:99 [in Coq.Reals.Abstract.ConstructiveLUB]
Q:992 [in Coq.Lists.List]
Q:996 [in Coq.Lists.List]
q:996 [in Coq.Init.Specif]


Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (73252 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1016 entries)
Binder Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (47569 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (800 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1555 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (592 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11846 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (959 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (629 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (308 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (475 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (494 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (912 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1503 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4428 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (166 entries)