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)

I (binder)

id:17 [in Coq.micromega.Tauto]
id:7 [in Coq.ssr.ssreflect]
IFF:170 [in Coq.micromega.ZifyClasses]
ih1:200 [in Coq.Numbers.Cyclic.Int63.Int63]
ih:134 [in Coq.Numbers.Cyclic.Int31.Int31]
ih:141 [in Coq.Numbers.Cyclic.Int31.Int31]
ih:146 [in Coq.Numbers.Cyclic.Int31.Int31]
ih:148 [in Coq.Numbers.Cyclic.Int31.Int31]
ih:180 [in Coq.Numbers.Cyclic.Int63.Int63]
ih:186 [in Coq.Numbers.Cyclic.Int63.Int63]
ih:190 [in Coq.Numbers.Cyclic.Int63.Int63]
ih:194 [in Coq.Numbers.Cyclic.Int63.Int63]
ih:196 [in Coq.Numbers.Cyclic.Int63.Int63]
ih:321 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
ih:325 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
ih:328 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
ih:332 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
ih:338 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
ih:400 [in Coq.Numbers.Cyclic.Int63.Int63]
ih:405 [in Coq.Numbers.Cyclic.Int63.Int63]
ih:413 [in Coq.Numbers.Cyclic.Int63.Int63]
ih:417 [in Coq.Numbers.Cyclic.Int63.Int63]
ih:423 [in Coq.Numbers.Cyclic.Int63.Int63]
ij:99 [in Coq.Numbers.Cyclic.Int31.Int31]
il1:201 [in Coq.Numbers.Cyclic.Int63.Int63]
il:135 [in Coq.Numbers.Cyclic.Int31.Int31]
il:142 [in Coq.Numbers.Cyclic.Int31.Int31]
il:147 [in Coq.Numbers.Cyclic.Int31.Int31]
il:149 [in Coq.Numbers.Cyclic.Int31.Int31]
il:181 [in Coq.Numbers.Cyclic.Int63.Int63]
il:187 [in Coq.Numbers.Cyclic.Int63.Int63]
il:191 [in Coq.Numbers.Cyclic.Int63.Int63]
il:195 [in Coq.Numbers.Cyclic.Int63.Int63]
il:197 [in Coq.Numbers.Cyclic.Int63.Int63]
il:322 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
il:326 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
il:329 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
il:333 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
il:339 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
il:401 [in Coq.Numbers.Cyclic.Int63.Int63]
il:406 [in Coq.Numbers.Cyclic.Int63.Int63]
il:414 [in Coq.Numbers.Cyclic.Int63.Int63]
il:418 [in Coq.Numbers.Cyclic.Int63.Int63]
il:424 [in Coq.Numbers.Cyclic.Int63.Int63]
Im:97 [in Coq.Reals.Runcountable]
init:64 [in Coq.Arith.Between]
init:70 [in Coq.Arith.Between]
inj:4 [in Coq.Logic.PropFacts]
Interp:47 [in Coq.nsatz.NsatzTactic]
interp:8 [in Coq.Numbers.Cyclic.Abstract.DoubleType]
inv:103 [in Coq.Program.Wf]
Inv:210 [in Coq.PArith.BinPos]
Inv:296 [in Coq.NArith.BinNat]
inv:321 [in Coq.ssr.ssrfun]
inv:325 [in Coq.ssr.ssrfun]
inv:347 [in Coq.ssr.ssrfun]
inv:350 [in Coq.ssr.ssrfun]
inv:368 [in Coq.ssr.ssrfun]
inv:371 [in Coq.ssr.ssrfun]
inv:72 [in Coq.Program.Wf]
In:96 [in Coq.Reals.Runcountable]
i':155 [in Coq.MSets.MSetProperties]
i':155 [in Coq.FSets.FSetProperties]
i':392 [in Coq.FSets.FMapFacts]
i':70 [in Coq.setoid_ring.Ring_polynom]
i':72 [in Coq.micromega.EnvRing]
i':75 [in Coq.setoid_ring.Ring_polynom]
i':77 [in Coq.micromega.EnvRing]
i0:67 [in Coq.Reals.Cos_rel]
i0:68 [in Coq.Reals.Cos_rel]
I1:109 [in Coq.micromega.ZifyClasses]
I1:126 [in Coq.micromega.ZifyClasses]
I1:13 [in Coq.micromega.ZifyClasses]
I1:25 [in Coq.micromega.ZifyClasses]
i1:353 [in Coq.Numbers.Cyclic.Int63.Int63]
I2:110 [in Coq.micromega.ZifyClasses]
I2:127 [in Coq.micromega.ZifyClasses]
I2:14 [in Coq.micromega.ZifyClasses]
I2:26 [in Coq.micromega.ZifyClasses]
i2:354 [in Coq.Numbers.Cyclic.Int63.Int63]
I3:111 [in Coq.micromega.ZifyClasses]
I3:15 [in Coq.micromega.ZifyClasses]
i:1 [in Coq.FSets.FMapPositive]
I:1 [in Coq.Reals.RiemannInt_SF]
i:10 [in Coq.Reals.Rtrigo_def]
i:10 [in Coq.Reals.Binomial]
i:10 [in Coq.ssr.ssrfun]
i:10 [in Coq.Reals.Rpower]
i:10 [in Coq.FSets.FMapPositive]
i:10 [in Coq.Reals.PartSum]
i:10 [in Coq.Reals.Abstract.ConstructiveSum]
i:10 [in Coq.QArith.QArith_base]
i:100 [in Coq.Reals.Alembert]
i:100 [in Coq.Numbers.Cyclic.Int31.Int31]
i:100 [in Coq.Reals.PartSum]
i:100 [in Coq.Reals.Abstract.ConstructiveSum]
i:101 [in Coq.MSets.MSetWeakList]
i:101 [in Coq.Reals.Alembert]
i:101 [in Coq.Reals.PartSum]
i:102 [in Coq.Reals.Alembert]
i:102 [in Coq.rtauto.Bintree]
i:102 [in Coq.Reals.PartSum]
i:102 [in Coq.Reals.Cos_rel]
i:103 [in Coq.Reals.Alembert]
i:103 [in Coq.Reals.PartSum]
i:103 [in Coq.Reals.SeqProp]
i:104 [in Coq.Reals.Abstract.ConstructiveReals]
i:104 [in Coq.FSets.FMapPositive]
i:104 [in Coq.Reals.PartSum]
i:104 [in Coq.Reals.Cos_rel]
i:105 [in Coq.Reals.PartSum]
i:105 [in Coq.Reals.SeqProp]
i:105 [in Coq.Reals.Cos_rel]
i:106 [in Coq.Reals.PartSum]
i:106 [in Coq.Reals.Cos_rel]
i:107 [in Coq.Reals.PartSum]
i:107 [in Coq.Reals.Cos_rel]
i:108 [in Coq.Reals.Exp_prop]
i:108 [in Coq.Reals.PartSum]
i:108 [in Coq.Reals.Cos_rel]
i:109 [in Coq.Reals.Exp_prop]
i:109 [in Coq.FSets.FMapPositive]
i:109 [in Coq.Reals.RList]
i:109 [in Coq.Reals.PartSum]
i:11 [in Coq.Init.Decimal]
i:11 [in Coq.Numbers.Cyclic.Int63.Int63]
i:11 [in Coq.Reals.Rtrigo_alt]
i:11 [in Coq.Init.Hexadecimal]
i:11 [in Coq.Reals.Rpower]
i:11 [in Coq.FSets.FSetPositive]
i:11 [in Coq.MSets.MSetPositive]
i:11 [in Coq.Reals.PartSum]
i:11 [in Coq.Reals.RiemannInt_SF]
i:110 [in Coq.Reals.Exp_prop]
i:110 [in Coq.rtauto.Bintree]
i:110 [in Coq.Reals.PartSum]
i:111 [in Coq.Reals.Exp_prop]
i:111 [in Coq.rtauto.Bintree]
i:111 [in Coq.setoid_ring.Ncring_polynom]
i:111 [in Coq.Reals.PartSum]
i:112 [in Coq.FSets.FMapPositive]
i:112 [in Coq.Reals.PartSum]
i:113 [in Coq.Logic.Hurkens]
i:113 [in Coq.Numbers.Cyclic.Int31.Int31]
i:113 [in Coq.Reals.PartSum]
i:114 [in Coq.Logic.Hurkens]
i:114 [in Coq.Reals.Abstract.ConstructiveLimits]
i:114 [in Coq.Reals.PartSum]
i:115 [in Coq.rtauto.Bintree]
i:115 [in Coq.Reals.Abstract.ConstructiveLimits]
i:115 [in Coq.FSets.FMapPositive]
i:115 [in Coq.Reals.PartSum]
i:116 [in Coq.btauto.Algebra]
i:116 [in Coq.Reals.PartSum]
i:117 [in Coq.Reals.PartSum]
i:118 [in Coq.Numbers.Cyclic.Int63.Int63]
i:118 [in Coq.Numbers.Cyclic.Int31.Int31]
i:118 [in Coq.FSets.FMapPositive]
i:118 [in Coq.Reals.PartSum]
i:119 [in Coq.MSets.MSetProperties]
i:119 [in Coq.FSets.FMapPositive]
i:119 [in Coq.Reals.PartSum]
i:119 [in Coq.FSets.FSetProperties]
i:12 [in Coq.Reals.Rtrigo_def]
i:12 [in Coq.Numbers.Cyclic.Int63.Int63]
i:12 [in Coq.Reals.Rtrigo_alt]
i:12 [in Coq.Reals.Rpower]
i:12 [in Coq.setoid_ring.Ring_theory]
I:120 [in Coq.ssr.ssrfun]
i:120 [in Coq.MSets.MSetPositive]
i:120 [in Coq.Reals.PartSum]
i:120 [in Coq.Reals.SeqProp]
i:121 [in Coq.Logic.Hurkens]
i:121 [in Coq.Numbers.Cyclic.Int31.Int31]
i:121 [in Coq.Reals.PartSum]
i:122 [in Coq.Reals.Alembert]
i:122 [in Coq.Reals.PartSum]
i:122 [in Coq.Reals.SeqProp]
i:1225 [in Coq.FSets.FMapAVL]
i:123 [in Coq.btauto.Algebra]
i:123 [in Coq.FSets.FSetPositive]
i:123 [in Coq.Reals.PartSum]
i:124 [in Coq.setoid_ring.Ring_polynom]
i:124 [in Coq.ssr.ssrfun]
i:124 [in Coq.FSets.FMapPositive]
i:124 [in Coq.Reals.PartSum]
i:125 [in Coq.Reals.Alembert]
I:125 [in Coq.ssr.ssrfun]
i:125 [in Coq.Reals.PartSum]
i:126 [in Coq.Reals.SeqSeries]
i:126 [in Coq.Logic.Hurkens]
i:126 [in Coq.Numbers.Cyclic.Int31.Int31]
i:126 [in Coq.Reals.PartSum]
i:127 [in Coq.MSets.MSetProperties]
i:127 [in Coq.FSets.FMapPositive]
i:127 [in Coq.Reals.PartSum]
i:127 [in Coq.FSets.FSetProperties]
i:128 [in Coq.MSets.MSetEqProperties]
i:128 [in Coq.Reals.Alembert]
i:128 [in Coq.Logic.Hurkens]
i:128 [in Coq.FSets.FSetEqProperties]
i:128 [in Coq.Reals.PartSum]
i:129 [in Coq.Reals.RList]
i:129 [in Coq.Reals.PartSum]
i:129 [in Coq.setoid_ring.Ncring]
i:13 [in Coq.Reals.Rtrigo_def]
i:13 [in Coq.Init.Numeral]
i:13 [in Coq.Numbers.Cyclic.Int63.Int63]
i:13 [in Coq.setoid_ring.Ncring_tac]
i:13 [in Coq.Reals.Rtrigo_alt]
i:13 [in Coq.Reals.Rpower]
i:13 [in Coq.Logic.ClassicalDescription]
i:13 [in Coq.Reals.RiemannInt_SF]
i:13 [in Coq.QArith.QArith_base]
i:130 [in Coq.Reals.SeqSeries]
i:130 [in Coq.Numbers.Cyclic.Int31.Int31]
i:130 [in Coq.FSets.FMapPositive]
i:130 [in Coq.Reals.PartSum]
i:131 [in Coq.Reals.SeqSeries]
i:131 [in Coq.Reals.Alembert]
i:131 [in Coq.Numbers.Cyclic.Int31.Int31]
i:131 [in Coq.Reals.PartSum]
i:132 [in Coq.micromega.EnvRing]
i:132 [in Coq.Reals.SeqSeries]
i:132 [in Coq.Reals.Alembert]
i:132 [in Coq.Reals.RList]
i:132 [in Coq.Reals.PartSum]
i:133 [in Coq.Reals.SeqSeries]
i:133 [in Coq.Reals.Alembert]
i:133 [in Coq.FSets.FMapFullAVL]
i:133 [in Coq.Reals.PartSum]
i:134 [in Coq.Reals.SeqSeries]
i:134 [in Coq.Reals.PartSum]
i:135 [in Coq.MSets.MSetProperties]
i:135 [in Coq.Reals.SeqSeries]
I:135 [in Coq.ssr.ssrfun]
i:135 [in Coq.FSets.FSetProperties]
i:136 [in Coq.btauto.Algebra]
i:136 [in Coq.Reals.SeqSeries]
I:137 [in Coq.micromega.ZifyClasses]
i:137 [in Coq.Reals.SeqSeries]
i:138 [in Coq.Reals.SeqSeries]
i:1384 [in Coq.FSets.FMapAVL]
i:139 [in Coq.MSets.MSetProperties]
i:139 [in Coq.btauto.Algebra]
i:139 [in Coq.Reals.SeqSeries]
i:139 [in Coq.ssr.ssrfun]
i:139 [in Coq.FSets.FSetProperties]
i:14 [in Coq.Init.Numeral]
i:14 [in Coq.Reals.Binomial]
i:14 [in Coq.Numbers.Cyclic.Int63.Int63]
i:14 [in Coq.Reals.Alembert]
i:14 [in Coq.Reals.Rtrigo_alt]
i:14 [in Coq.Reals.PartSum]
i:14 [in Coq.Reals.Rsigma]
i:140 [in Coq.Reals.SeqSeries]
i:141 [in Coq.Reals.SeqSeries]
i:141 [in Coq.ssr.ssrfun]
i:141 [in Coq.Lists.SetoidList]
i:142 [in Coq.Reals.Alembert]
i:143 [in Coq.ssr.ssrfun]
i:1437 [in Coq.FSets.FMapAVL]
i:144 [in Coq.ssr.ssrfun]
i:145 [in Coq.Reals.Alembert]
i:146 [in Coq.Reals.Alembert]
i:147 [in Coq.MSets.MSetProperties]
i:147 [in Coq.Reals.Alembert]
i:147 [in Coq.FSets.FSetProperties]
i:149 [in Coq.Reals.RiemannInt_SF]
i:15 [in Coq.setoid_ring.BinList]
i:15 [in Coq.Numbers.DecimalQ]
i:15 [in Coq.Numbers.Cyclic.Int63.Int63]
i:15 [in Coq.Reals.Alembert]
i:15 [in Coq.Reals.Rtrigo_alt]
i:15 [in Coq.Reals.AltSeries]
i:15 [in Coq.Reals.PartSum]
i:15 [in Coq.Reals.Rsigma]
i:150 [in Coq.Reals.RiemannInt_SF]
i:154 [in Coq.MSets.MSetProperties]
i:154 [in Coq.FSets.FSetProperties]
I:155 [in Coq.ssr.ssrfun]
i:157 [in Coq.MSets.MSetProperties]
i:157 [in Coq.FSets.FSetProperties]
i:158 [in Coq.btauto.Algebra]
I:158 [in Coq.ssr.ssrfun]
i:158 [in Coq.Numbers.Cyclic.Int31.Int31]
i:16 [in Coq.Reals.Alembert]
i:16 [in Coq.Reals.Rtrigo_alt]
i:16 [in Coq.Reals.AltSeries]
i:16 [in Coq.Logic.ClassicalDescription]
i:16 [in Coq.Reals.PartSum]
i:16 [in Coq.Reals.Rsigma]
i:160 [in Coq.MSets.MSetProperties]
i:160 [in Coq.Numbers.Cyclic.Int31.Int31]
i:160 [in Coq.FSets.FSetProperties]
i:161 [in Coq.MSets.MSetProperties]
i:161 [in Coq.MSets.MSetGenTree]
i:161 [in Coq.FSets.FSetProperties]
i:162 [in Coq.ssr.ssrfun]
i:162 [in Coq.Numbers.Cyclic.Int31.Int31]
i:163 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
I:163 [in Coq.ssr.ssrfun]
i:163 [in Coq.Lists.SetoidList]
i:164 [in Coq.MSets.MSetProperties]
i:164 [in Coq.Reals.RiemannInt]
i:164 [in Coq.FSets.FSetProperties]
i:165 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:165 [in Coq.Numbers.Cyclic.Int63.Int63]
i:166 [in Coq.MSets.MSetGenTree]
i:167 [in Coq.MSets.MSetProperties]
i:167 [in Coq.FSets.FSetProperties]
i:168 [in Coq.MSets.MSetInterface]
i:168 [in Coq.Numbers.Cyclic.Int31.Int31]
i:168 [in Coq.setoid_ring.Ncring_polynom]
i:168 [in Coq.Lists.SetoidList]
i:17 [in Coq.Numbers.Cyclic.Int63.Int63]
i:17 [in Coq.Reals.Alembert]
i:17 [in Coq.Reals.Rtrigo_alt]
i:17 [in Coq.FSets.FSetPositive]
i:17 [in Coq.MSets.MSetPositive]
i:17 [in Coq.Reals.AltSeries]
i:17 [in Coq.Reals.PartSum]
i:17 [in Coq.Reals.Rsigma]
i:17 [in Coq.QArith.QArith_base]
i:170 [in Coq.MSets.MSetProperties]
i:170 [in Coq.Numbers.Cyclic.Int63.Int63]
i:170 [in Coq.FSets.FSetProperties]
I:171 [in Coq.ssr.ssrfun]
i:172 [in Coq.Lists.SetoidList]
i:173 [in Coq.MSets.MSetProperties]
i:173 [in Coq.Numbers.Cyclic.Int63.Int63]
i:173 [in Coq.Reals.RiemannInt]
i:173 [in Coq.FSets.FSetProperties]
i:175 [in Coq.FSets.FMapPositive]
i:176 [in Coq.MSets.MSetProperties]
i:176 [in Coq.Numbers.Cyclic.Int63.Int63]
i:176 [in Coq.FSets.FSetProperties]
i:177 [in Coq.Numbers.Cyclic.Int63.Int63]
i:177 [in Coq.FSets.FSetCompat]
i:178 [in Coq.Lists.SetoidList]
i:179 [in Coq.MSets.MSetProperties]
i:179 [in Coq.FSets.FSetProperties]
i:18 [in Coq.setoid_ring.BinList]
i:18 [in Coq.Reals.Binomial]
i:18 [in Coq.Reals.Alembert]
i:18 [in Coq.Reals.Rtrigo_alt]
i:18 [in Coq.Numbers.Cyclic.Int31.Int31]
i:18 [in Coq.FSets.FMapPositive]
i:18 [in Coq.Reals.AltSeries]
i:18 [in Coq.Reals.PartSum]
i:182 [in Coq.Reals.RiemannInt]
i:182 [in Coq.Reals.SeqProp]
i:183 [in Coq.Lists.SetoidList]
i:184 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:184 [in Coq.FSets.FMapPositive]
i:185 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:185 [in Coq.Reals.SeqProp]
i:186 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:186 [in Coq.FSets.FMapFullAVL]
i:187 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:187 [in Coq.Reals.Rfunctions]
i:187 [in Coq.Lists.SetoidList]
i:188 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:188 [in Coq.Reals.Rfunctions]
i:189 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:189 [in Coq.Reals.Rfunctions]
i:189 [in Coq.Reals.RiemannInt]
i:19 [in Coq.btauto.Algebra]
i:19 [in Coq.Reals.Alembert]
i:19 [in Coq.Reals.AltSeries]
i:190 [in Coq.Reals.Rfunctions]
i:190 [in Coq.FSets.FMapPositive]
i:191 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:191 [in Coq.Reals.Rfunctions]
i:192 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:192 [in Coq.Reals.Rfunctions]
i:193 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:195 [in Coq.Reals.RiemannInt]
i:196 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:197 [in Coq.Reals.RiemannInt]
i:199 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:199 [in Coq.setoid_ring.Ncring_tac]
i:2 [in Coq.Reals.ArithProp]
i:2 [in Coq.Reals.Rtrigo_alt]
i:2 [in Coq.Reals.AltSeries]
i:20 [in Coq.Reals.ArithProp]
i:20 [in Coq.Reals.Alembert]
i:203 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:203 [in Coq.Numbers.Cyclic.Int63.Int63]
i:204 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:204 [in Coq.setoid_ring.Ncring]
i:204 [in Coq.Reals.SeqProp]
i:206 [in Coq.setoid_ring.Ring_polynom]
i:209 [in Coq.micromega.EnvRing]
i:21 [in Coq.Reals.Alembert]
i:21 [in Coq.Reals.Rtrigo_alt]
i:21 [in Coq.Reals.Ratan]
i:21 [in Coq.QArith.QArith_base]
i:212 [in Coq.Reals.Ratan]
i:216 [in Coq.MSets.MSetList]
i:217 [in Coq.Numbers.Cyclic.Int63.Int63]
i:218 [in Coq.Reals.Ratan]
i:219 [in Coq.setoid_ring.Ring_polynom]
i:22 [in Coq.Reals.Alembert]
i:22 [in Coq.Reals.Rtrigo_alt]
i:22 [in Coq.rtauto.Bintree]
i:22 [in Coq.Reals.AltSeries]
i:22 [in Coq.Reals.Ratan]
i:22 [in Coq.setoid_ring.Ring_theory]
i:22 [in Coq.Reals.PartSum]
i:222 [in Coq.micromega.EnvRing]
i:222 [in Coq.Numbers.Cyclic.Int63.Int63]
i:222 [in Coq.FSets.FMapPositive]
i:224 [in Coq.Numbers.Cyclic.Int63.Int63]
i:224 [in Coq.MSets.MSetPositive]
i:225 [in Coq.setoid_ring.Ring_polynom]
i:227 [in Coq.FSets.FMapPositive]
i:228 [in Coq.micromega.EnvRing]
i:228 [in Coq.Reals.SeqProp]
i:229 [in Coq.Reals.SeqProp]
i:23 [in Coq.Logic.Epsilon]
i:23 [in Coq.Reals.Binomial]
i:23 [in Coq.Reals.Alembert]
i:23 [in Coq.Reals.Rtrigo_alt]
i:23 [in Coq.micromega.Env]
i:23 [in Coq.extraction.ExtrOcamlBigIntConv]
i:23 [in Coq.FSets.FSetPositive]
i:23 [in Coq.MSets.MSetPositive]
i:23 [in Coq.FSets.FMapPositive]
i:23 [in Coq.Reals.AltSeries]
i:23 [in Coq.Reals.Ratan]
i:23 [in Coq.extraction.ExtrOcamlIntConv]
i:230 [in Coq.Reals.SeqProp]
i:231 [in Coq.Reals.SeqProp]
i:232 [in Coq.Numbers.Cyclic.Int63.Int63]
i:232 [in Coq.Reals.SeqProp]
i:233 [in Coq.MSets.MSetPositive]
i:234 [in Coq.FSets.FMapPositive]
i:235 [in Coq.Numbers.Cyclic.Int63.Int63]
i:237 [in Coq.Numbers.Cyclic.Int63.Int63]
i:237 [in Coq.MSets.MSetPositive]
i:24 [in Coq.Reals.Binomial]
i:24 [in Coq.Logic.ClassicalEpsilon]
i:24 [in Coq.Reals.Alembert]
i:24 [in Coq.Reals.Rtrigo_alt]
i:24 [in Coq.extraction.ExtrOcamlBigIntConv]
i:24 [in Coq.Reals.AltSeries]
i:24 [in Coq.Reals.Ratan]
i:24 [in Coq.extraction.ExtrOcamlIntConv]
i:240 [in Coq.FSets.FSetBridge]
i:241 [in Coq.Numbers.Cyclic.Int63.Int63]
i:242 [in Coq.Numbers.Cyclic.Int63.Int63]
i:242 [in Coq.FSets.FSetInterface]
i:244 [in Coq.Vectors.VectorSpec]
i:245 [in Coq.FSets.FSetBridge]
i:246 [in Coq.MSets.MSetInterface]
i:25 [in Coq.Reals.Rtrigo_def]
i:25 [in Coq.Reals.Binomial]
i:25 [in Coq.Reals.Alembert]
i:25 [in Coq.extraction.ExtrOcamlBigIntConv]
i:25 [in Coq.Reals.AltSeries]
i:25 [in Coq.Reals.Ratan]
i:25 [in Coq.extraction.ExtrOcamlIntConv]
i:250 [in Coq.MSets.MSetPositive]
i:251 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:251 [in Coq.Vectors.VectorSpec]
i:256 [in Coq.MSets.MSetPositive]
i:257 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:26 [in Coq.Logic.Epsilon]
i:26 [in Coq.Reals.ArithProp]
i:26 [in Coq.Reals.Binomial]
i:26 [in Coq.Numbers.Cyclic.Int31.Int31]
i:26 [in Coq.Reals.AltSeries]
i:26 [in Coq.Reals.Ratan]
i:260 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:263 [in Coq.MSets.MSetPositive]
i:264 [in Coq.FSets.FMapPositive]
i:269 [in Coq.FSets.FMapPositive]
i:27 [in Coq.Reals.Rtrigo_reg]
i:27 [in Coq.Reals.Rtrigo1]
i:27 [in Coq.Reals.Binomial]
i:27 [in Coq.Logic.ClassicalEpsilon]
i:27 [in Coq.btauto.Algebra]
i:27 [in Coq.rtauto.Bintree]
i:271 [in Coq.setoid_ring.Ring_polynom]
i:276 [in Coq.Numbers.Cyclic.Int63.Int63]
i:277 [in Coq.FSets.FMapPositive]
i:279 [in Coq.FSets.FMapWeakList]
i:28 [in Coq.MSets.MSetProperties]
i:28 [in Coq.Reals.Binomial]
i:28 [in Coq.Reals.PartSum]
i:28 [in Coq.Reals.SeqProp]
i:28 [in Coq.FSets.FSetProperties]
i:28 [in Coq.QArith.QArith_base]
i:281 [in Coq.FSets.FMapPositive]
i:282 [in Coq.MSets.MSetProperties]
i:282 [in Coq.FSets.FSetProperties]
i:284 [in Coq.micromega.EnvRing]
i:285 [in Coq.FSets.FMapFacts]
i:287 [in Coq.FSets.FMapList]
i:29 [in Coq.Reals.Rtrigo_reg]
i:29 [in Coq.Reals.Rtrigo1]
i:29 [in Coq.Reals.Binomial]
i:29 [in Coq.FSets.FMapPositive]
i:29 [in Coq.Reals.RList]
i:29 [in Coq.Reals.PartSum]
i:29 [in Coq.Reals.RiemannInt_SF]
i:290 [in Coq.micromega.RingMicromega]
i:290 [in Coq.MSets.MSetProperties]
i:290 [in Coq.FSets.FMapFacts]
i:290 [in Coq.FSets.FSetProperties]
i:291 [in Coq.ZArith.BinInt]
i:294 [in Coq.ZArith.BinInt]
i:294 [in Coq.micromega.EnvRing]
i:297 [in Coq.MSets.MSetProperties]
i:297 [in Coq.ZArith.BinInt]
i:298 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:298 [in Coq.Reals.Ratan]
i:3 [in Coq.Reals.Rtrigo_def]
i:3 [in Coq.Reals.RiemannInt_SF]
i:30 [in Coq.Logic.Epsilon]
i:30 [in Coq.Reals.ArithProp]
i:30 [in Coq.Reals.Binomial]
i:30 [in Coq.Reals.PartSum]
i:300 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:300 [in Coq.MSets.MSetProperties]
i:300 [in Coq.FSets.FSetPositive]
i:300 [in Coq.Reals.Ratan]
i:301 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:301 [in Coq.FSets.FSetProperties]
i:303 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:303 [in Coq.MSets.MSetProperties]
i:304 [in Coq.FSets.FSetProperties]
i:306 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:307 [in Coq.FSets.FSetProperties]
i:308 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:308 [in Coq.Reals.RiemannInt_SF]
i:309 [in Coq.FSets.FSetPositive]
i:31 [in Coq.Reals.Binomial]
i:31 [in Coq.Logic.ClassicalEpsilon]
i:31 [in Coq.rtauto.Bintree]
i:31 [in Coq.Reals.PartSum]
i:31 [in Coq.Reals.SeqProp]
i:311 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:312 [in Coq.MSets.MSetGenTree]
i:313 [in Coq.FSets.FMapFacts]
i:313 [in Coq.FSets.FSetPositive]
i:316 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:316 [in Coq.MSets.MSetGenTree]
i:317 [in Coq.FSets.FMapPositive]
i:318 [in Coq.Numbers.Cyclic.Int63.Int63]
i:319 [in Coq.Numbers.Cyclic.Int63.Int63]
i:32 [in Coq.Reals.Binomial]
i:321 [in Coq.Numbers.Cyclic.Int63.Int63]
i:322 [in Coq.FSets.FMapPositive]
i:324 [in Coq.Numbers.Cyclic.Int63.Int63]
i:325 [in Coq.FSets.FMapFacts]
i:325 [in Coq.Numbers.Cyclic.Int63.Int63]
i:326 [in Coq.FSets.FSetPositive]
i:33 [in Coq.MSets.MSetProperties]
i:33 [in Coq.Logic.Epsilon]
i:33 [in Coq.Reals.Binomial]
i:33 [in Coq.Reals.Alembert]
i:33 [in Coq.Reals.Ratan]
i:33 [in Coq.FSets.FSetProperties]
i:330 [in Coq.Numbers.Cyclic.Int63.Int63]
i:330 [in Coq.FSets.FMapPositive]
i:332 [in Coq.Numbers.Cyclic.Int63.Int63]
i:333 [in Coq.FSets.FMapFacts]
i:333 [in Coq.Numbers.Cyclic.Int63.Int63]
i:335 [in Coq.Numbers.Cyclic.Int63.Int63]
i:338 [in Coq.Numbers.Cyclic.Int63.Int63]
i:338 [in Coq.FSets.FSetPositive]
i:338 [in Coq.FSets.FMapPositive]
I:34 [in Coq.micromega.ZifyClasses]
i:34 [in Coq.Reals.Binomial]
i:34 [in Coq.Numbers.Cyclic.Int63.Int63]
i:34 [in Coq.Reals.Alembert]
i:34 [in Coq.Reals.Ratan]
i:34 [in Coq.Reals.SeqProp]
i:340 [in Coq.FSets.FMapPositive]
i:341 [in Coq.Numbers.Cyclic.Int63.Int63]
i:342 [in Coq.FSets.FMapPositive]
i:344 [in Coq.Numbers.Cyclic.Int63.Int63]
i:347 [in Coq.FSets.FMapFacts]
i:347 [in Coq.Numbers.Cyclic.Int63.Int63]
i:348 [in Coq.FSets.FSetPositive]
i:35 [in Coq.Reals.Binomial]
i:35 [in Coq.Numbers.Cyclic.Int63.Int63]
i:35 [in Coq.Reals.Alembert]
i:35 [in Coq.Reals.Ratan]
i:35 [in Coq.Reals.RiemannInt_SF]
i:351 [in Coq.Numbers.Cyclic.Int63.Int63]
i:355 [in Coq.Numbers.Cyclic.Int63.Int63]
i:36 [in Coq.Reals.Binomial]
i:36 [in Coq.Numbers.Cyclic.Int63.Int63]
i:36 [in Coq.Reals.Alembert]
i:36 [in Coq.FSets.FMapPositive]
i:36 [in Coq.Reals.Ratan]
i:36 [in Coq.Reals.RiemannInt_SF]
i:37 [in Coq.Reals.Binomial]
i:37 [in Coq.Reals.Rtrigo_alt]
i:37 [in Coq.Reals.Ratan]
i:37 [in Coq.Reals.RList]
i:371 [in Coq.micromega.ZMicromega]
i:376 [in Coq.Numbers.Cyclic.Int63.Int63]
i:378 [in Coq.Numbers.Cyclic.Int63.Int63]
i:38 [in Coq.Numbers.HexadecimalPos]
i:38 [in Coq.Reals.Binomial]
i:38 [in Coq.Reals.Rtrigo_alt]
i:38 [in Coq.Reals.Ratan]
i:38 [in Coq.Numbers.DecimalPos]
i:38 [in Coq.Reals.PartSum]
i:38 [in Coq.Reals.SeqProp]
i:382 [in Coq.Numbers.Cyclic.Int63.Int63]
i:384 [in Coq.Numbers.Cyclic.Int63.Int63]
i:386 [in Coq.Numbers.Cyclic.Int63.Int63]
i:389 [in Coq.Numbers.Cyclic.Int63.Int63]
i:39 [in Coq.Reals.Binomial]
i:39 [in Coq.Reals.Rtrigo_alt]
i:391 [in Coq.FSets.FMapFacts]
i:394 [in Coq.FSets.FMapFacts]
i:394 [in Coq.Numbers.Cyclic.Int63.Int63]
i:397 [in Coq.Numbers.Cyclic.Int63.Int63]
i:4 [in Coq.Reals.Binomial]
i:4 [in Coq.setoid_ring.Ncring_tac]
i:4 [in Coq.Reals.Rtrigo_alt]
I:4 [in Coq.ssr.ssrfun]
i:4 [in Coq.Reals.Rpower]
i:40 [in Coq.Reals.Rtrigo_def]
i:40 [in Coq.Reals.Binomial]
i:40 [in Coq.Numbers.Cyclic.Int63.Int63]
i:40 [in Coq.Reals.Rtrigo_alt]
i:40 [in Coq.Reals.Ratan]
i:403 [in Coq.FSets.FMapFacts]
i:41 [in Coq.FSets.FSetBridge]
I:41 [in Coq.micromega.ZifyClasses]
i:41 [in Coq.Numbers.HexadecimalPos]
i:41 [in Coq.Reals.Binomial]
i:41 [in Coq.Reals.Rtrigo_alt]
i:41 [in Coq.Reals.RList]
i:41 [in Coq.Numbers.DecimalPos]
i:413 [in Coq.FSets.FMapFacts]
i:416 [in Coq.FSets.FMapFacts]
i:42 [in Coq.setoid_ring.Ring_polynom]
i:42 [in Coq.Reals.Binomial]
i:42 [in Coq.Reals.Rtrigo_alt]
i:42 [in Coq.Reals.Ratan]
i:42 [in Coq.QArith.QArith_base]
i:422 [in Coq.FSets.FMapFacts]
i:426 [in Coq.FSets.FMapFacts]
i:43 [in Coq.Reals.Cauchy_prod]
i:43 [in Coq.Reals.Binomial]
i:43 [in Coq.Reals.PartSum]
i:43 [in Coq.Reals.ClassicalConstructiveReals]
i:44 [in Coq.Reals.Cauchy_prod]
i:44 [in Coq.Reals.ArithProp]
i:44 [in Coq.Reals.Binomial]
i:44 [in Coq.micromega.EnvRing]
i:44 [in Coq.FSets.FMapPositive]
i:445 [in Coq.Lists.List]
i:448 [in Coq.Numbers.Cyclic.Int63.Int63]
i:448 [in Coq.FSets.FMapList]
i:45 [in Coq.Reals.Cauchy_prod]
i:45 [in Coq.setoid_ring.Ring_polynom]
i:45 [in Coq.Reals.Binomial]
i:45 [in Coq.setoid_ring.Ncring_polynom]
i:46 [in Coq.Reals.Cauchy_prod]
i:46 [in Coq.Reals.Binomial]
i:46 [in Coq.Reals.Abstract.ConstructiveLimits]
i:46 [in Coq.Reals.ClassicalConstructiveReals]
I:460 [in Coq.ssr.ssrbool]
i:463 [in Coq.Numbers.Cyclic.Int63.Int63]
i:465 [in Coq.Lists.List]
i:465 [in Coq.Numbers.Cyclic.Int63.Int63]
i:468 [in Coq.Numbers.Cyclic.Int63.Int63]
i:469 [in Coq.Numbers.Cyclic.Int63.Int63]
i:47 [in Coq.Reals.Cauchy_prod]
i:47 [in Coq.Reals.Binomial]
i:47 [in Coq.micromega.EnvRing]
i:47 [in Coq.MSets.MSetList]
i:47 [in Coq.Reals.PartSum]
i:470 [in Coq.Lists.List]
i:470 [in Coq.Numbers.Cyclic.Int63.Int63]
i:472 [in Coq.Numbers.Cyclic.Int63.Int63]
I:474 [in Coq.ssr.ssrbool]
i:475 [in Coq.Numbers.Cyclic.Int63.Int63]
i:476 [in Coq.Numbers.Cyclic.Int63.Int63]
i:477 [in Coq.Numbers.Cyclic.Int63.Int63]
i:479 [in Coq.Numbers.Cyclic.Int63.Int63]
i:48 [in Coq.Reals.Cauchy_prod]
i:48 [in Coq.Reals.Binomial]
i:482 [in Coq.Numbers.Cyclic.Int63.Int63]
I:482 [in Coq.ssr.ssrbool]
i:483 [in Coq.Numbers.Cyclic.Int63.Int63]
i:49 [in Coq.setoid_ring.Ncring_polynom]
i:49 [in Coq.Reals.RList]
I:492 [in Coq.ssr.ssrbool]
i:5 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
i:5 [in Coq.Reals.Rpower]
i:5 [in Coq.FSets.FMapPositive]
i:5 [in Coq.Numbers.HexadecimalQ]
i:50 [in Coq.Reals.PartSum]
i:51 [in Coq.ZArith.Zpow_facts]
i:51 [in Coq.FSets.FMapPositive]
i:51 [in Coq.setoid_ring.Ncring_polynom]
i:517 [in Coq.FSets.FMapWeakList]
i:52 [in Coq.Reals.Abstract.ConstructiveLimits]
i:52 [in Coq.FSets.FMapPositive]
i:53 [in Coq.MSets.MSetProperties]
i:53 [in Coq.Reals.Rtrigo_alt]
i:53 [in Coq.FSets.FSetProperties]
i:537 [in Coq.FSets.FMapList]
i:54 [in Coq.ZArith.Zpow_facts]
i:54 [in Coq.Reals.Rtrigo_alt]
i:54 [in Coq.Reals.PartSum]
i:549 [in Coq.FSets.FMapFacts]
i:55 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
i:55 [in Coq.Reals.Rtrigo_alt]
i:55 [in Coq.FSets.FMapPositive]
i:56 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
i:56 [in Coq.MSets.MSetInterface]
i:56 [in Coq.Reals.Rtrigo_alt]
i:56 [in Coq.FSets.FMapPositive]
i:56 [in Coq.Reals.Ratan]
i:57 [in Coq.Reals.Rtrigo_alt]
i:57 [in Coq.btauto.Reflect]
i:58 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
i:58 [in Coq.Reals.Rtrigo_alt]
i:58 [in Coq.Reals.Abstract.ConstructiveLimits]
i:58 [in Coq.Reals.PartSum]
i:59 [in Coq.Reals.Rtrigo_alt]
i:591 [in Coq.FSets.FMapWeakList]
i:6 [in Coq.Reals.Binomial]
i:6 [in Coq.Reals.Rseries]
i:6 [in Coq.Reals.Rpower]
i:6 [in Coq.FSets.FSetPositive]
i:6 [in Coq.MSets.MSetPositive]
I:6 [in Coq.Reals.RiemannInt_SF]
i:60 [in Coq.Reals.Rtrigo_alt]
i:60 [in Coq.FSets.FMapPositive]
i:60 [in Coq.Reals.Ratan]
i:61 [in Coq.Reals.Cauchy_prod]
i:61 [in Coq.FSets.FMapInterface]
i:61 [in Coq.FSets.FMapPositive]
i:61 [in Coq.setoid_ring.Ncring_polynom]
i:61 [in Coq.Logic.Diaconescu]
i:612 [in Coq.FSets.FMapList]
I:62 [in Coq.micromega.ZifyClasses]
i:62 [in Coq.Reals.Alembert]
i:62 [in Coq.FSets.FSetPositive]
i:62 [in Coq.MSets.MSetPositive]
i:63 [in Coq.Reals.Alembert]
i:63 [in Coq.Reals.Rtrigo_alt]
i:63 [in Coq.FSets.FMapPositive]
i:64 [in Coq.Reals.Cauchy_prod]
i:64 [in Coq.MSets.MSetProperties]
i:64 [in Coq.Reals.Rtrigo_alt]
i:64 [in Coq.FSets.FSetProperties]
i:65 [in Coq.Reals.Rtrigo_alt]
i:65 [in Coq.rtauto.Bintree]
i:65 [in Coq.Reals.Ratan]
i:65 [in Coq.Reals.PartSum]
i:65 [in Coq.btauto.Reflect]
i:66 [in Coq.Reals.Rtrigo_alt]
i:66 [in Coq.FSets.FSetPositive]
i:66 [in Coq.MSets.MSetPositive]
i:66 [in Coq.Reals.Ratan]
i:66 [in Coq.Logic.Diaconescu]
i:67 [in Coq.FSets.FMapPositive]
i:683 [in Coq.FSets.FMapFacts]
i:69 [in Coq.FSets.FSetPositive]
i:69 [in Coq.MSets.MSetPositive]
i:69 [in Coq.btauto.Reflect]
i:692 [in Coq.FSets.FMapFacts]
i:7 [in Coq.Init.Numeral]
i:7 [in Coq.Numbers.Cyclic.Int63.Int63]
i:7 [in Coq.ssr.ssrfun]
i:7 [in Coq.Reals.Rpower]
i:7 [in Coq.FSets.FMapPositive]
i:7 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
i:7 [in Coq.Reals.PartSum]
i:702 [in Coq.FSets.FMapFacts]
I:71 [in Coq.micromega.ZifyClasses]
i:71 [in Coq.MSets.MSetProperties]
i:71 [in Coq.FSets.FMapPositive]
i:71 [in Coq.FSets.FSetProperties]
i:72 [in Coq.Init.Decimal]
i:720 [in Coq.Lists.List]
I:73 [in Coq.Reals.Runcountable]
i:73 [in Coq.Init.Decimal]
i:73 [in Coq.FSets.FMapPositive]
i:74 [in Coq.rtauto.Bintree]
i:74 [in Coq.FSets.FSetPositive]
i:74 [in Coq.MSets.MSetPositive]
i:75 [in Coq.Reals.RList]
i:76 [in Coq.Reals.Rsqrt_def]
i:76 [in Coq.FSets.FSetInterface]
i:76 [in Coq.rtauto.Bintree]
i:77 [in Coq.Reals.Rsqrt_def]
i:78 [in Coq.Reals.Abstract.ConstructiveSum]
I:79 [in Coq.Reals.Runcountable]
i:79 [in Coq.Reals.Rtrigo_alt]
i:79 [in Coq.Logic.Hurkens]
i:79 [in Coq.FSets.FSetPositive]
i:79 [in Coq.MSets.MSetPositive]
i:8 [in Coq.Init.Numeral]
i:8 [in Coq.Numbers.Cyclic.Int63.Int63]
i:8 [in Coq.Reals.Rpower]
i:8 [in Coq.Reals.PartSum]
i:8 [in Coq.Reals.RiemannInt_SF]
i:80 [in Coq.Reals.Rtrigo_alt]
i:80 [in Coq.FSets.FMapPositive]
i:81 [in Coq.Reals.Rtrigo_alt]
i:81 [in Coq.Reals.RList]
i:82 [in Coq.Reals.Rtrigo1]
i:82 [in Coq.Reals.Rsqrt_def]
i:82 [in Coq.Reals.Rtrigo_alt]
i:82 [in Coq.rtauto.Bintree]
i:83 [in Coq.Reals.Rtrigo1]
i:83 [in Coq.Reals.Rtrigo_alt]
i:84 [in Coq.Reals.Rtrigo1]
i:84 [in Coq.MSets.MSetProperties]
i:84 [in Coq.Reals.Rtrigo_alt]
i:84 [in Coq.rtauto.Bintree]
i:84 [in Coq.FSets.FSetPositive]
i:84 [in Coq.MSets.MSetPositive]
i:84 [in Coq.FSets.FSetProperties]
i:843 [in Coq.Lists.List]
i:847 [in Coq.Lists.List]
i:85 [in Coq.Reals.Rtrigo1]
i:85 [in Coq.Reals.Rtrigo_alt]
i:85 [in Coq.Logic.Hurkens]
i:86 [in Coq.Reals.Rtrigo1]
i:86 [in Coq.Reals.Rtrigo_alt]
i:86 [in Coq.Vectors.Fin]
i:86 [in Coq.Numbers.Cyclic.Int31.Int31]
i:86 [in Coq.FSets.FMapPositive]
i:86 [in Coq.Reals.Cos_rel]
I:87 [in Coq.micromega.ZifyClasses]
i:87 [in Coq.Reals.Rtrigo1]
i:87 [in Coq.Reals.Rtrigo_alt]
i:87 [in Coq.Logic.Hurkens]
i:87 [in Coq.rtauto.Bintree]
i:88 [in Coq.Reals.Rtrigo_alt]
i:88 [in Coq.Reals.PartSum]
i:89 [in Coq.Reals.Abstract.ConstructiveLimits]
i:89 [in Coq.Reals.Cos_rel]
i:894 [in Coq.Lists.List]
i:9 [in Coq.Init.Decimal]
i:9 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
i:9 [in Coq.Numbers.Cyclic.Int63.Int63]
i:9 [in Coq.ssr.ssrfun]
i:9 [in Coq.Init.Hexadecimal]
i:9 [in Coq.Reals.Rpower]
i:9 [in Coq.micromega.Env]
i:9 [in Coq.FSets.FMapPositive]
i:9 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
i:9 [in Coq.Reals.PartSum]
i:90 [in Coq.Numbers.Cyclic.Int63.Int63]
i:90 [in Coq.FSets.FMapPositive]
i:91 [in Coq.Logic.Hurkens]
i:91 [in Coq.Reals.Cos_rel]
i:914 [in Coq.Lists.List]
i:92 [in Coq.Reals.Alembert]
i:92 [in Coq.FSets.FSetCompat]
i:93 [in Coq.Reals.Alembert]
i:93 [in Coq.Logic.Hurkens]
i:93 [in Coq.Reals.Abstract.ConstructiveSum]
i:94 [in Coq.Numbers.Cyclic.Int63.Int63]
i:94 [in Coq.Reals.Alembert]
i:94 [in Coq.Logic.Hurkens]
i:94 [in Coq.ZArith.Int]
i:94 [in Coq.FSets.FSetPositive]
i:94 [in Coq.MSets.MSetPositive]
i:94 [in Coq.FSets.FMapPositive]
i:95 [in Coq.Reals.Alembert]
i:95 [in Coq.Reals.Abstract.ConstructiveLimits]
i:95 [in Coq.Reals.PartSum]
i:95 [in Coq.Reals.Cos_rel]
i:96 [in Coq.Reals.Alembert]
i:96 [in Coq.Logic.Hurkens]
i:96 [in Coq.ZArith.Int]
i:96 [in Coq.setoid_ring.Ncring_polynom]
i:96 [in Coq.Reals.RList]
i:96 [in Coq.Reals.PartSum]
i:97 [in Coq.Reals.Alembert]
i:97 [in Coq.Numbers.Cyclic.Int31.Int31]
i:97 [in Coq.Reals.PartSum]
i:97 [in Coq.Reals.Cos_rel]
i:98 [in Coq.Reals.Abstract.ConstructiveReals]
i:98 [in Coq.Numbers.Cyclic.Int63.Int63]
i:98 [in Coq.Reals.Alembert]
i:98 [in Coq.FSets.FMapPositive]
i:98 [in Coq.Reals.PartSum]
i:99 [in Coq.Reals.Alembert]
i:99 [in Coq.Reals.RList]
i:99 [in Coq.Reals.PartSum]
i:99 [in Coq.Reals.Abstract.ConstructiveSum]


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)