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 (72487 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 (1049 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 (47021 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 (788 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 (1537 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 (588 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 (11841 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 (1025 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 (634 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 (306 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 (473 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 (486 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 (881 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 (1465 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 (4229 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 (164 entries)

K (binder)

kl:129 [in Coq.btauto.Algebra]
kl:141 [in Coq.btauto.Algebra]
kl:145 [in Coq.btauto.Algebra]
ko:113 [in Coq.MSets.MSetRBT]
kr:130 [in Coq.btauto.Algebra]
kr:142 [in Coq.btauto.Algebra]
kr:146 [in Coq.btauto.Algebra]
k':102 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
k':104 [in Coq.ssr.ssreflect]
k':16 [in Coq.Structures.EqualitiesFacts]
k':209 [in Coq.Structures.OrderedType]
k':21 [in Coq.Structures.EqualitiesFacts]
k':213 [in Coq.Structures.OrderedType]
k':26 [in Coq.Structures.EqualitiesFacts]
k':34 [in Coq.Structures.EqualitiesFacts]
k':398 [in Coq.FSets.FMapFacts]
k':41 [in Coq.Structures.DecidableType]
k':45 [in Coq.Structures.DecidableType]
k':8 [in Coq.Structures.EqualitiesFacts]
k':86 [in Coq.Structures.EqualitiesFacts]
k':91 [in Coq.Structures.EqualitiesFacts]
k0:10 [in Coq.Reals.Rsigma]
k0:11 [in Coq.Reals.Rsigma]
k0:12 [in Coq.Reals.Rsigma]
k0:13 [in Coq.Reals.Rsigma]
k0:18 [in Coq.Reals.Rsigma]
k0:19 [in Coq.Reals.Rsigma]
k0:20 [in Coq.Reals.Rsigma]
k0:21 [in Coq.Reals.Rsigma]
k0:213 [in Coq.Reals.SeqProp]
k0:22 [in Coq.Reals.Rsigma]
k0:227 [in Coq.Reals.Abstract.ConstructiveSum]
k0:228 [in Coq.Reals.Abstract.ConstructiveSum]
k0:229 [in Coq.Reals.Abstract.ConstructiveSum]
k0:23 [in Coq.Reals.Rsigma]
k0:230 [in Coq.Reals.Abstract.ConstructiveSum]
k0:48 [in Coq.Reals.Abstract.ConstructiveSum]
k0:49 [in Coq.Reals.Abstract.ConstructiveSum]
k0:50 [in Coq.Reals.Abstract.ConstructiveSum]
k0:51 [in Coq.Reals.Abstract.ConstructiveSum]
k1:110 [in Coq.omega.OmegaLemmas]
k1:118 [in Coq.omega.OmegaLemmas]
k1:260 [in Coq.FSets.FMapFacts]
k1:405 [in Coq.micromega.Tauto]
k1:46 [in Coq.omega.OmegaLemmas]
k1:50 [in Coq.Vectors.VectorSpec]
k1:52 [in Coq.omega.OmegaLemmas]
k1:85 [in Coq.Vectors.VectorSpec]
k2:111 [in Coq.omega.OmegaLemmas]
k2:125 [in Coq.omega.OmegaLemmas]
k2:133 [in Coq.omega.OmegaLemmas]
k2:261 [in Coq.FSets.FMapFacts]
k2:47 [in Coq.omega.OmegaLemmas]
k2:51 [in Coq.Vectors.VectorSpec]
k2:57 [in Coq.omega.OmegaLemmas]
k2:71 [in Coq.omega.OmegaLemmas]
k2:86 [in Coq.Vectors.VectorSpec]
k:10 [in Coq.Reals.Cauchy_prod]
k:10 [in Coq.Reals.Rprod]
k:10 [in Coq.Numbers.NatInt.NZDomain]
k:10 [in Coq.MSets.MSetRBT]
k:10 [in Coq.Reals.Cos_rel]
k:10 [in Coq.Reals.Rcomplete]
k:100 [in Coq.Logic.FunctionalExtensionality]
k:100 [in Coq.FSets.FMapList]
k:100 [in Coq.Reals.Cos_rel]
k:101 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
k:101 [in Coq.btauto.Algebra]
k:101 [in Coq.micromega.Tauto]
k:101 [in Coq.Reals.Cos_rel]
k:102 [in Coq.Logic.FunctionalExtensionality]
k:102 [in Coq.FSets.FMapWeakList]
k:103 [in Coq.micromega.Tauto]
k:103 [in Coq.Reals.Cos_rel]
k:104 [in Coq.Floats.SpecFloat]
k:104 [in Coq.btauto.Algebra]
k:105 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
k:105 [in Coq.ssr.ssreflect]
k:105 [in Coq.FSets.FMapList]
k:105 [in Coq.micromega.Tauto]
k:1051 [in Coq.Lists.List]
k:1053 [in Coq.Lists.List]
k:106 [in Coq.Floats.SpecFloat]
k:106 [in Coq.FSets.FMapWeakList]
k:106 [in Coq.Reals.PSeries_reg]
k:106 [in Coq.Reals.SeqProp]
k:107 [in Coq.Reals.Alembert]
k:107 [in Coq.Reals.SeqProp]
k:108 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
k:108 [in Coq.Reals.PSeries_reg]
k:108 [in Coq.FSets.FMapList]
k:108 [in Coq.Reals.SeqProp]
k:109 [in Coq.Reals.SeqSeries]
k:109 [in Coq.Reals.SeqProp]
k:11 [in Coq.Reals.Rtrigo_reg]
k:11 [in Coq.Reals.Rtrigo1]
k:11 [in Coq.NArith.Ndist]
k:11 [in Coq.Arith.Between]
k:11 [in Coq.Reals.Cos_plus]
k:110 [in Coq.FSets.FMapWeakList]
k:110 [in Coq.Reals.PSeries_reg]
k:110 [in Coq.Reals.SeqProp]
k:111 [in Coq.Reals.SeqProp]
k:112 [in Coq.btauto.Algebra]
k:112 [in Coq.Init.Nat]
k:112 [in Coq.FSets.FMapList]
k:112 [in Coq.Reals.SeqProp]
k:112 [in Coq.micromega.Tauto]
k:113 [in Coq.ssr.ssreflect]
k:113 [in Coq.Reals.PSeries_reg]
k:113 [in Coq.Reals.SeqProp]
k:114 [in Coq.Reals.SeqSeries]
k:114 [in Coq.Reals.SeqProp]
k:115 [in Coq.Reals.PSeries_reg]
k:115 [in Coq.Reals.SeqProp]
k:116 [in Coq.Numbers.Integer.Abstract.ZBits]
k:116 [in Coq.FSets.FMapList]
k:116 [in Coq.Reals.SeqProp]
k:117 [in Coq.Reals.SeqSeries]
k:117 [in Coq.Reals.SeqProp]
k:118 [in Coq.Reals.Exp_prop]
k:118 [in Coq.Reals.SeqProp]
k:1180 [in Coq.Lists.List]
k:1183 [in Coq.Lists.List]
k:119 [in Coq.setoid_ring.Ncring_polynom]
k:12 [in Coq.Reals.Cauchy_prod]
k:12 [in Coq.Reals.PartSum]
k:12 [in Coq.micromega.Tauto]
k:120 [in Coq.Reals.SeqSeries]
k:120 [in Coq.Init.Nat]
k:121 [in Coq.Reals.Exp_prop]
k:121 [in Coq.Reals.SeqSeries]
k:122 [in Coq.Reals.SeqSeries]
k:123 [in Coq.Reals.Cauchy_prod]
k:123 [in Coq.Reals.SeqSeries]
k:123 [in Coq.Reals.SeqProp]
k:124 [in Coq.Reals.SeqSeries]
k:124 [in Coq.Reals.SeqProp]
k:125 [in Coq.Reals.Cauchy_prod]
k:125 [in Coq.Reals.SeqSeries]
k:125 [in Coq.Reals.SeqProp]
k:126 [in Coq.Reals.SeqProp]
k:1269 [in Coq.FSets.FMapAVL]
k:127 [in Coq.Reals.Cauchy_prod]
k:127 [in Coq.Reals.SeqSeries]
k:127 [in Coq.Reals.Abstract.ConstructiveLimits]
k:127 [in Coq.setoid_ring.Ncring_polynom]
k:127 [in Coq.Reals.SeqProp]
k:1270 [in Coq.FSets.FMapAVL]
k:128 [in Coq.Reals.SeqSeries]
k:128 [in Coq.Reals.SeqProp]
k:129 [in Coq.Reals.Cauchy_prod]
k:129 [in Coq.Reals.SeqSeries]
k:129 [in Coq.Reals.Abstract.ConstructiveSum]
k:129 [in Coq.Reals.SeqProp]
k:13 [in Coq.FSets.FMapWeakList]
k:13 [in Coq.Arith.Between]
k:13 [in Coq.FSets.FMapList]
k:13 [in Coq.micromega.Tauto]
k:13 [in Coq.Reals.Cos_plus]
k:130 [in Coq.Reals.Abstract.ConstructiveSum]
k:130 [in Coq.Reals.SeqProp]
k:131 [in Coq.Reals.Cauchy_prod]
k:131 [in Coq.Reals.SeqProp]
k:132 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
k:132 [in Coq.Reals.Abstract.ConstructiveLimits]
k:132 [in Coq.Reals.SeqProp]
k:133 [in Coq.Reals.Cauchy_prod]
k:133 [in Coq.btauto.Algebra]
k:134 [in Coq.Reals.Cauchy_prod]
k:134 [in Coq.Structures.OrderedType]
k:135 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
k:136 [in Coq.Reals.Cauchy_prod]
k:136 [in Coq.Reals.Alembert]
k:137 [in Coq.Reals.Cauchy_prod]
k:137 [in Coq.Vectors.Fin]
k:138 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
k:138 [in Coq.btauto.Algebra]
k:138 [in Coq.Structures.OrderedType]
k:139 [in Coq.Reals.Cauchy_prod]
k:139 [in Coq.omega.OmegaLemmas]
k:14 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
k:14 [in Coq.Reals.Abstract.ConstructiveSum]
k:14 [in Coq.micromega.Tauto]
k:14 [in Coq.Reals.Cos_rel]
k:140 [in Coq.Reals.PSeries_reg]
k:141 [in Coq.Vectors.Fin]
k:141 [in Coq.Reals.PSeries_reg]
k:142 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
k:142 [in Coq.Reals.SeqSeries]
k:143 [in Coq.Reals.MVT]
k:143 [in Coq.Reals.SeqSeries]
k:144 [in Coq.Reals.SeqSeries]
k:145 [in Coq.Reals.SeqSeries]
k:1456 [in Coq.FSets.FMapAVL]
k:1457 [in Coq.FSets.FMapAVL]
k:146 [in Coq.Reals.SeqSeries]
k:147 [in Coq.Reals.SeqSeries]
k:147 [in Coq.Reals.PartSum]
k:149 [in Coq.btauto.Algebra]
k:15 [in Coq.btauto.Algebra]
k:15 [in Coq.Numbers.NatInt.NZDomain]
k:15 [in Coq.FSets.FMapWeakList]
k:15 [in Coq.Reals.Ratan]
k:15 [in Coq.Structures.EqualitiesFacts]
k:15 [in Coq.FSets.FMapList]
k:15 [in Coq.micromega.Tauto]
k:15 [in Coq.Reals.Cos_plus]
k:152 [in Coq.btauto.Algebra]
k:155 [in Coq.btauto.Algebra]
k:155 [in Coq.MSets.MSetRBT]
k:155 [in Coq.Reals.PartSum]
k:156 [in Coq.Reals.PartSum]
k:156 [in Coq.Reals.SeqProp]
k:157 [in Coq.Reals.SeqSeries]
k:158 [in Coq.Reals.SeqSeries]
k:158 [in Coq.MSets.MSetRBT]
k:159 [in Coq.Reals.Rtrigo1]
k:159 [in Coq.Reals.SeqSeries]
k:159 [in Coq.MSets.MSetRBT]
k:16 [in Coq.Reals.Cauchy_prod]
k:16 [in Coq.NArith.Ndist]
k:16 [in Coq.MSets.MSetRBT]
k:16 [in Coq.Reals.Ratan]
k:16 [in Coq.Arith.Between]
k:16 [in Coq.micromega.Tauto]
k:160 [in Coq.Reals.Cauchy_prod]
k:160 [in Coq.btauto.Algebra]
k:160 [in Coq.Reals.SeqSeries]
k:160 [in Coq.NArith.Ndigits]
k:161 [in Coq.Reals.Rtrigo1]
k:161 [in Coq.Reals.SeqSeries]
k:162 [in Coq.Reals.Cauchy_prod]
k:162 [in Coq.Reals.SeqSeries]
k:163 [in Coq.Reals.Rtrigo1]
k:164 [in Coq.Reals.Cauchy_prod]
k:164 [in Coq.micromega.Tauto]
k:165 [in Coq.Reals.Rtrigo1]
k:166 [in Coq.Reals.Cauchy_prod]
k:167 [in Coq.Reals.PartSum]
k:167 [in Coq.micromega.Tauto]
k:168 [in Coq.FSets.FMapWeakList]
k:168 [in Coq.Reals.PartSum]
k:169 [in Coq.FSets.FMapList]
k:17 [in Coq.btauto.Algebra]
k:17 [in Coq.micromega.Tauto]
k:17 [in Coq.Reals.Cos_plus]
k:170 [in Coq.Structures.OrderedType]
k:171 [in Coq.micromega.Tauto]
k:172 [in Coq.FSets.FMapWeakList]
k:172 [in Coq.Structures.OrderedType]
k:173 [in Coq.FSets.FMapList]
k:174 [in Coq.FSets.FMapWeakList]
k:174 [in Coq.Reals.SeqProp]
k:175 [in Coq.Structures.OrderedType]
k:175 [in Coq.Logic.ClassicalFacts]
k:175 [in Coq.FSets.FMapList]
k:175 [in Coq.micromega.Tauto]
k:177 [in Coq.FSets.FMapWeakList]
k:178 [in Coq.FSets.FMapList]
k:179 [in Coq.micromega.Tauto]
k:18 [in Coq.Reals.Cauchy_prod]
k:18 [in Coq.FSets.FMapWeakList]
k:18 [in Coq.FSets.FMapList]
k:18 [in Coq.micromega.Tauto]
k:180 [in Coq.FSets.FMapWeakList]
k:181 [in Coq.FSets.FMapList]
k:182 [in Coq.micromega.ZMicromega]
k:184 [in Coq.NArith.Ndigits]
k:185 [in Coq.micromega.Tauto]
k:19 [in Coq.Reals.Ratan]
k:19 [in Coq.micromega.Tauto]
k:19 [in Coq.Reals.Cos_rel]
k:19 [in Coq.Reals.Cos_plus]
k:190 [in Coq.micromega.Tauto]
k:191 [in Coq.FSets.FMapAVL]
k:193 [in Coq.Reals.Abstract.ConstructiveSum]
k:193 [in Coq.Reals.SeqProp]
k:194 [in Coq.Reals.Abstract.ConstructiveSum]
k:195 [in Coq.Structures.OrderedType]
k:195 [in Coq.Reals.Abstract.ConstructiveSum]
k:195 [in Coq.Reals.SeqProp]
k:196 [in Coq.Reals.Abstract.ConstructiveSum]
k:196 [in Coq.Reals.SeqProp]
k:196 [in Coq.micromega.Tauto]
k:197 [in Coq.Reals.Abstract.ConstructiveSum]
k:197 [in Coq.Reals.SeqProp]
k:198 [in Coq.Reals.SeqProp]
k:199 [in Coq.Reals.SeqProp]
k:2 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
k:20 [in Coq.Reals.Rprod]
k:20 [in Coq.MSets.MSetRBT]
k:20 [in Coq.Reals.Ratan]
k:20 [in Coq.Structures.EqualitiesFacts]
k:20 [in Coq.Reals.PartSum]
k:20 [in Coq.micromega.Tauto]
k:205 [in Coq.FSets.FMapFullAVL]
k:206 [in Coq.FSets.FMapFacts]
k:206 [in Coq.FSets.FMapFullAVL]
k:206 [in Coq.Structures.OrderedType]
k:208 [in Coq.Structures.OrderedType]
k:21 [in Coq.Reals.Cauchy_prod]
k:21 [in Coq.omega.OmegaLemmas]
k:21 [in Coq.FSets.FMapWeakList]
k:21 [in Coq.Arith.Between]
k:21 [in Coq.FSets.FMapList]
k:21 [in Coq.micromega.Tauto]
k:211 [in Coq.Reals.SeqProp]
k:212 [in Coq.Structures.OrderedType]
k:22 [in Coq.Reals.Exp_prop]
k:224 [in Coq.Reals.Abstract.ConstructiveSum]
k:23 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
k:23 [in Coq.Reals.Cauchy_prod]
k:23 [in Coq.Reals.Rprod]
k:23 [in Coq.btauto.Algebra]
k:23 [in Coq.Arith.Between]
k:23 [in Coq.Reals.Abstract.ConstructiveSum]
k:23 [in Coq.micromega.Tauto]
k:23 [in Coq.Reals.Cos_plus]
k:230 [in Coq.MSets.MSetRBT]
k:238 [in Coq.Logic.ClassicalFacts]
k:239 [in Coq.MSets.MSetRBT]
k:24 [in Coq.Reals.Exp_prop]
k:24 [in Coq.MSets.MSetRBT]
k:240 [in Coq.micromega.Tauto]
k:243 [in Coq.setoid_ring.Ring_polynom]
k:244 [in Coq.micromega.Tauto]
k:246 [in Coq.micromega.EnvRing]
k:248 [in Coq.MSets.MSetRBT]
k:25 [in Coq.btauto.Algebra]
k:25 [in Coq.Structures.DecidableType]
k:25 [in Coq.Arith.Between]
k:25 [in Coq.Structures.EqualitiesFacts]
k:25 [in Coq.Reals.Cos_plus]
k:250 [in Coq.micromega.Tauto]
k:255 [in Coq.micromega.EnvRing]
k:256 [in Coq.Logic.ClassicalFacts]
k:256 [in Coq.micromega.Tauto]
k:26 [in Coq.Reals.Rtrigo_reg]
k:26 [in Coq.Reals.Rtrigo1]
k:26 [in Coq.Reals.Exp_prop]
k:26 [in Coq.Reals.PartSum]
k:26 [in Coq.Numbers.Natural.Abstract.NStrongRec]
k:26 [in Coq.Reals.Rsigma]
k:262 [in Coq.micromega.Tauto]
k:267 [in Coq.FSets.FMapFacts]
k:27 [in Coq.Structures.DecidableType]
k:27 [in Coq.Reals.SeqProp]
k:27 [in Coq.Reals.Cos_rel]
k:270 [in Coq.Reals.Ratan]
k:270 [in Coq.micromega.Tauto]
k:271 [in Coq.Reals.Ratan]
k:277 [in Coq.FSets.FMapFacts]
k:277 [in Coq.micromega.Tauto]
k:279 [in Coq.micromega.Tauto]
k:28 [in Coq.Reals.Rtrigo_reg]
k:28 [in Coq.Reals.Rtrigo1]
k:28 [in Coq.Reals.Exp_prop]
k:28 [in Coq.MSets.MSetRBT]
k:28 [in Coq.Reals.Abstract.ConstructiveSum]
k:28 [in Coq.Reals.Cos_rel]
k:280 [in Coq.FSets.FMapFacts]
k:281 [in Coq.micromega.Tauto]
k:283 [in Coq.Numbers.Cyclic.Int63.Uint63]
k:283 [in Coq.micromega.Tauto]
k:284 [in Coq.FSets.FMapWeakList]
k:285 [in Coq.micromega.Tauto]
k:287 [in Coq.micromega.Tauto]
k:289 [in Coq.micromega.Tauto]
k:29 [in Coq.Logic.ConstructiveEpsilon]
k:29 [in Coq.Reals.Abstract.ConstructiveSum]
k:29 [in Coq.micromega.Tauto]
k:29 [in Coq.Reals.Rsigma]
k:29 [in Coq.Reals.Cos_rel]
k:290 [in Coq.FSets.FMapWeakList]
k:291 [in Coq.micromega.Tauto]
k:293 [in Coq.FSets.FMapFacts]
k:295 [in Coq.micromega.Tauto]
k:297 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
k:298 [in Coq.FSets.FMapFacts]
k:299 [in Coq.micromega.Tauto]
k:3 [in Coq.Reals.Exp_prop]
k:3 [in Coq.MSets.MSetRBT]
k:3 [in Coq.Arith.Between]
k:3 [in Coq.Reals.Cos_rel]
k:3 [in Coq.Reals.Rcomplete]
k:30 [in Coq.Reals.Rtrigo_reg]
k:30 [in Coq.Reals.Ranalysis4]
k:30 [in Coq.Reals.Exp_prop]
k:30 [in Coq.Structures.DecidableType]
k:30 [in Coq.Reals.Abstract.ConstructiveSum]
k:30 [in Coq.Reals.SeqProp]
k:30 [in Coq.Reals.Cos_rel]
k:301 [in Coq.FSets.FMapWeakList]
k:302 [in Coq.FSets.FMapPositive]
k:302 [in Coq.FSets.FMapWeakList]
k:302 [in Coq.micromega.Tauto]
k:303 [in Coq.FSets.FMapFacts]
k:303 [in Coq.FSets.FMapPositive]
k:306 [in Coq.micromega.Tauto]
k:308 [in Coq.FSets.FMapFacts]
k:308 [in Coq.FSets.FMapWeakList]
k:309 [in Coq.FSets.FMapFacts]
k:309 [in Coq.FSets.FMapWeakList]
k:309 [in Coq.micromega.Tauto]
k:31 [in Coq.Reals.Rtrigo_reg]
k:31 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
k:31 [in Coq.Reals.Abstract.ConstructiveSum]
k:31 [in Coq.Reals.Cos_rel]
k:311 [in Coq.micromega.Tauto]
k:314 [in Coq.micromega.Tauto]
k:316 [in Coq.micromega.Tauto]
k:318 [in Coq.FSets.FMapFacts]
k:318 [in Coq.micromega.Tauto]
k:32 [in Coq.Vectors.VectorSpec]
k:32 [in Coq.Reals.Ranalysis4]
k:32 [in Coq.Reals.Exp_prop]
k:32 [in Coq.FSets.FMapInterface]
k:32 [in Coq.Reals.Abstract.ConstructiveSum]
k:32 [in Coq.Reals.Cos_rel]
k:321 [in Coq.micromega.Tauto]
k:325 [in Coq.micromega.Tauto]
k:327 [in Coq.FSets.FMapFacts]
k:33 [in Coq.Reals.Cauchy_prod]
k:33 [in Coq.Reals.Runcountable]
k:33 [in Coq.Logic.ConstructiveEpsilon]
k:33 [in Coq.MSets.MSetRBT]
k:33 [in Coq.Structures.EqualitiesFacts]
k:33 [in Coq.Reals.Abstract.ConstructiveSum]
k:33 [in Coq.Reals.Cos_rel]
k:33 [in Coq.Reals.Cos_plus]
k:330 [in Coq.micromega.Tauto]
k:334 [in Coq.micromega.Tauto]
k:337 [in Coq.FSets.FMapFacts]
k:338 [in Coq.micromega.Tauto]
k:34 [in Coq.Reals.Ranalysis4]
k:34 [in Coq.Reals.Exp_prop]
k:34 [in Coq.Reals.SeqSeries]
k:34 [in Coq.Reals.Abstract.ConstructiveSum]
k:34 [in Coq.Reals.Cos_rel]
k:343 [in Coq.micromega.Tauto]
k:346 [in Coq.micromega.Tauto]
k:349 [in Coq.micromega.Tauto]
k:35 [in Coq.Reals.Cauchy_prod]
k:35 [in Coq.Reals.SeqSeries]
k:35 [in Coq.Reals.Abstract.ConstructiveSum]
k:35 [in Coq.Reals.SeqProp]
k:35 [in Coq.Reals.Cos_rel]
k:35 [in Coq.Reals.Cos_plus]
k:350 [in Coq.FSets.FMapFacts]
k:354 [in Coq.FSets.FMapFacts]
k:354 [in Coq.FSets.FMapList]
k:355 [in Coq.FSets.FMapList]
k:357 [in Coq.micromega.Tauto]
k:358 [in Coq.FSets.FMapFacts]
k:36 [in Coq.Reals.Exp_prop]
k:36 [in Coq.Reals.SeqSeries]
k:36 [in Coq.Reals.Abstract.ConstructiveSum]
k:36 [in Coq.Reals.Cos_rel]
k:364 [in Coq.micromega.Tauto]
k:369 [in Coq.FSets.FMapWeakList]
k:37 [in Coq.Reals.Ranalysis4]
k:37 [in Coq.Reals.SeqSeries]
k:37 [in Coq.ZArith.Zgcd_alt]
k:37 [in Coq.micromega.Tauto]
k:37 [in Coq.Reals.Cos_rel]
k:373 [in Coq.FSets.FMapWeakList]
k:375 [in Coq.micromega.Tauto]
k:376 [in Coq.Numbers.Cyclic.Int63.Uint63]
k:379 [in Coq.Init.Logic]
k:379 [in Coq.micromega.Tauto]
k:38 [in Coq.Reals.Cauchy_prod]
k:38 [in Coq.Reals.Cos_rel]
k:385 [in Coq.Init.Logic]
k:39 [in Coq.Reals.Ranalysis4]
k:39 [in Coq.Reals.SeqSeries]
k:39 [in Coq.micromega.QMicromega]
k:39 [in Coq.Reals.SeqProp]
k:39 [in Coq.Reals.Cos_rel]
k:392 [in Coq.FSets.FMapWeakList]
k:394 [in Coq.FSets.FMapWeakList]
k:396 [in Coq.FSets.FMapWeakList]
k:397 [in Coq.FSets.FMapFacts]
k:398 [in Coq.FSets.FMapWeakList]
k:4 [in Coq.Reals.Rsigma]
k:4 [in Coq.Reals.Rcomplete]
k:40 [in Coq.Reals.Cauchy_prod]
k:40 [in Coq.Reals.Exp_prop]
k:40 [in Coq.Reals.SeqSeries]
k:40 [in Coq.Structures.DecidableType]
k:40 [in Coq.ZArith.Zgcd_alt]
k:40 [in Coq.Reals.Cos_rel]
k:402 [in Coq.micromega.Tauto]
k:405 [in Coq.FSets.FMapFacts]
k:406 [in Coq.micromega.Tauto]
k:41 [in Coq.Reals.ArithProp]
k:41 [in Coq.micromega.QMicromega]
k:41 [in Coq.Reals.Abstract.ConstructiveSum]
k:41 [in Coq.micromega.ZMicromega]
k:41 [in Coq.micromega.Tauto]
k:41 [in Coq.Reals.Cos_rel]
k:410 [in Coq.micromega.Tauto]
k:411 [in Coq.FSets.FMapWeakList]
k:413 [in Coq.FSets.FMapWeakList]
k:415 [in Coq.FSets.FMapWeakList]
k:417 [in Coq.FSets.FMapWeakList]
k:419 [in Coq.FSets.FMapWeakList]
k:419 [in Coq.FSets.FMapList]
k:42 [in Coq.Vectors.VectorSpec]
k:42 [in Coq.Reals.Exp_prop]
k:42 [in Coq.Reals.SeqProp]
k:420 [in Coq.FSets.FMapFacts]
k:421 [in Coq.FSets.FMapWeakList]
k:424 [in Coq.FSets.FMapFacts]
k:428 [in Coq.FSets.FMapWeakList]
k:43 [in Coq.Reals.SeqSeries]
k:43 [in Coq.Reals.SeqProp]
k:43 [in Coq.micromega.ZMicromega]
k:43 [in Coq.Reals.Cos_rel]
k:43 [in Coq.Reals.Cos_plus]
k:430 [in Coq.FSets.FMapWeakList]
k:432 [in Coq.FSets.FMapWeakList]
k:432 [in Coq.Numbers.Cyclic.Int63.Uint63]
k:434 [in Coq.FSets.FMapWeakList]
k:436 [in Coq.FSets.FMapWeakList]
k:438 [in Coq.FSets.FMapWeakList]
k:44 [in Coq.Reals.SeqSeries]
k:44 [in Coq.Structures.DecidableType]
k:44 [in Coq.Reals.SeqProp]
k:443 [in Coq.Numbers.Cyclic.Int63.Uint63]
k:444 [in Coq.FSets.FMapFacts]
k:445 [in Coq.Numbers.Cyclic.Int63.Uint63]
k:448 [in Coq.FSets.FMapFacts]
k:448 [in Coq.Numbers.Cyclic.Int63.Uint63]
k:45 [in Coq.Structures.OrdersLists]
k:45 [in Coq.Arith.Between]
k:45 [in Coq.Reals.SeqProp]
k:45 [in Coq.micromega.Tauto]
k:45 [in Coq.Reals.Cos_rel]
k:45 [in Coq.Reals.Cos_plus]
k:451 [in Coq.FSets.FMapWeakList]
k:452 [in Coq.FSets.FMapFacts]
k:457 [in Coq.FSets.FMapFacts]
k:458 [in Coq.micromega.Tauto]
k:46 [in Coq.Reals.SeqSeries]
k:46 [in Coq.micromega.QMicromega]
k:46 [in Coq.Reals.SeqProp]
k:46 [in Coq.micromega.Tauto]
k:460 [in Coq.Numbers.Cyclic.Int63.Uint63]
k:462 [in Coq.FSets.FMapFacts]
k:467 [in Coq.FSets.FMapFacts]
k:467 [in Coq.Numbers.Cyclic.Int63.Uint63]
k:468 [in Coq.micromega.Tauto]
k:47 [in Coq.Reals.SeqProp]
k:47 [in Coq.Reals.Cos_rel]
k:47 [in Coq.Reals.Cos_plus]
k:471 [in Coq.ssr.ssrbool]
k:473 [in Coq.FSets.FMapFacts]
k:474 [in Coq.Numbers.Cyclic.Int63.Uint63]
k:476 [in Coq.FSets.FMapFacts]
k:478 [in Coq.micromega.Tauto]
k:479 [in Coq.ssr.ssrbool]
k:48 [in Coq.Reals.SeqSeries]
k:48 [in Coq.Arith.Between]
k:48 [in Coq.Reals.SeqProp]
k:48 [in Coq.micromega.ZMicromega]
k:48 [in Coq.micromega.Tauto]
k:48 [in Coq.Reals.Cos_plus]
k:480 [in Coq.FSets.FMapFacts]
k:482 [in Coq.FSets.FMapFacts]
k:482 [in Coq.ssr.ssrbool]
k:485 [in Coq.FSets.FMapFacts]
k:488 [in Coq.micromega.Tauto]
k:489 [in Coq.FSets.FMapFacts]
k:49 [in Coq.Reals.Cauchy_prod]
k:49 [in Coq.Reals.Ranalysis4]
k:49 [in Coq.Reals.Rprod]
k:49 [in Coq.Reals.SeqSeries]
k:49 [in Coq.FSets.FMapWeakList]
k:49 [in Coq.Structures.EqualitiesFacts]
k:49 [in Coq.Reals.SeqProp]
k:49 [in Coq.Reals.Cos_rel]
k:491 [in Coq.FSets.FMapFacts]
k:494 [in Coq.FSets.FMapFacts]
k:498 [in Coq.micromega.Tauto]
k:499 [in Coq.FSets.FMapFacts]
k:5 [in Coq.Reals.Rcomplete]
k:50 [in Coq.Reals.Ranalysis4]
k:50 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
k:50 [in Coq.Reals.SeqProp]
k:50 [in Coq.micromega.Tauto]
k:502 [in Coq.FSets.FMapFacts]
k:507 [in Coq.FSets.FMapFacts]
k:51 [in Coq.Reals.Cauchy_prod]
k:51 [in Coq.Reals.SeqSeries]
k:51 [in Coq.Arith.Between]
k:51 [in Coq.Reals.SeqProp]
k:51 [in Coq.Reals.Cos_rel]
k:514 [in Coq.FSets.FMapFacts]
k:518 [in Coq.FSets.FMapFacts]
k:52 [in Coq.Reals.SeqSeries]
k:52 [in Coq.Structures.EqualitiesFacts]
k:52 [in Coq.Reals.SeqProp]
k:52 [in Coq.micromega.Tauto]
k:52 [in Coq.Reals.Cos_plus]
k:526 [in Coq.FSets.FMapFacts]
k:53 [in Coq.Reals.SeqSeries]
k:53 [in Coq.FSets.FMapWeakList]
k:53 [in Coq.Reals.SeqProp]
k:53 [in Coq.Reals.Cos_rel]
k:533 [in Coq.FSets.FMapWeakList]
k:534 [in Coq.FSets.FMapWeakList]
k:54 [in Coq.Reals.Cauchy_prod]
k:54 [in Coq.Reals.Ranalysis4]
k:54 [in Coq.Reals.SeqSeries]
k:54 [in Coq.Reals.RList]
k:54 [in Coq.FSets.FMapList]
k:54 [in Coq.Reals.SeqProp]
k:54 [in Coq.micromega.Tauto]
k:54 [in Coq.Reals.Cos_plus]
k:540 [in Coq.MSets.MSetRBT]
k:55 [in Coq.Reals.SeqSeries]
k:55 [in Coq.FSets.FMapWeakList]
k:55 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
k:55 [in Coq.Arith.Between]
k:55 [in Coq.Reals.Abstract.ConstructiveSum]
k:55 [in Coq.Reals.SeqProp]
k:55 [in Coq.Reals.Cos_rel]
k:553 [in Coq.FSets.FMapList]
k:554 [in Coq.FSets.FMapList]
k:557 [in Coq.micromega.Tauto]
k:56 [in Coq.Reals.Cauchy_prod]
k:56 [in Coq.Structures.OrdersLists]
k:56 [in Coq.Reals.Ranalysis4]
k:56 [in Coq.Reals.SeqSeries]
k:56 [in Coq.Reals.PSeries_reg]
k:56 [in Coq.Structures.EqualitiesFacts]
k:56 [in Coq.Reals.SeqProp]
k:56 [in Coq.micromega.ZMicromega]
k:56 [in Coq.micromega.Tauto]
k:56 [in Coq.Reals.Cos_plus]
k:560 [in Coq.FSets.FMapFacts]
k:564 [in Coq.FSets.FMapFacts]
k:568 [in Coq.FSets.FMapFacts]
k:569 [in Coq.micromega.Tauto]
k:57 [in Coq.Reals.SeqSeries]
k:57 [in Coq.NArith.Ndist]
k:57 [in Coq.Reals.SeqProp]
k:571 [in Coq.micromega.Tauto]
k:572 [in Coq.FSets.FMapFacts]
k:572 [in Coq.Reals.RiemannInt]
k:572 [in Coq.micromega.Tauto]
k:573 [in Coq.micromega.Tauto]
k:575 [in Coq.FSets.FMapFacts]
k:576 [in Coq.micromega.Tauto]
k:579 [in Coq.FSets.FMapFacts]
k:579 [in Coq.micromega.Tauto]
k:58 [in Coq.Reals.SeqSeries]
k:58 [in Coq.FSets.FMapWeakList]
k:58 [in Coq.Arith.Between]
k:58 [in Coq.FSets.FMapList]
k:58 [in Coq.Reals.RiemannInt_SF]
k:58 [in Coq.Reals.SeqProp]
k:58 [in Coq.micromega.Tauto]
k:58 [in Coq.Reals.Cos_plus]
k:581 [in Coq.micromega.Tauto]
k:582 [in Coq.FSets.FMapFacts]
k:582 [in Coq.MSets.MSetRBT]
k:584 [in Coq.micromega.Tauto]
k:586 [in Coq.FSets.FMapFacts]
k:586 [in Coq.MSets.MSetRBT]
k:587 [in Coq.micromega.Tauto]
k:588 [in Coq.FSets.FMapFacts]
k:59 [in Coq.Vectors.VectorSpec]
k:59 [in Coq.Reals.Cauchy_prod]
k:59 [in Coq.Reals.Ranalysis4]
k:59 [in Coq.btauto.Algebra]
k:59 [in Coq.Reals.SeqSeries]
k:59 [in Coq.Reals.SeqProp]
k:591 [in Coq.FSets.FMapFacts]
k:592 [in Coq.MSets.MSetRBT]
k:594 [in Coq.FSets.FMapFacts]
k:597 [in Coq.FSets.FMapFacts]
k:599 [in Coq.micromega.Tauto]
k:6 [in Coq.Reals.Cos_rel]
k:6 [in Coq.Reals.Rcomplete]
k:60 [in Coq.Reals.SeqSeries]
k:60 [in Coq.Numbers.Integer.Abstract.ZBits]
k:60 [in Coq.FSets.FMapList]
k:60 [in Coq.Reals.Abstract.ConstructiveSum]
k:60 [in Coq.Reals.SeqProp]
k:60 [in Coq.Reals.Cos_plus]
k:604 [in Coq.micromega.Tauto]
k:61 [in Coq.Reals.Ranalysis4]
k:61 [in Coq.Reals.SeqSeries]
k:61 [in Coq.FSets.FMapWeakList]
k:61 [in Coq.Arith.Between]
k:61 [in Coq.Structures.EqualitiesFacts]
k:61 [in Coq.Reals.SeqProp]
k:615 [in Coq.micromega.Tauto]
k:62 [in Coq.Reals.Cauchy_prod]
k:62 [in Coq.Reals.Exp_prop]
k:62 [in Coq.Reals.SeqProp]
k:62 [in Coq.micromega.Tauto]
k:62 [in Coq.Reals.Cos_plus]
k:622 [in Coq.MSets.MSetRBT]
k:626 [in Coq.MSets.MSetRBT]
k:63 [in Coq.Reals.Ranalysis4]
k:63 [in Coq.Reals.Exp_prop]
k:63 [in Coq.ssr.ssreflect]
k:63 [in Coq.FSets.FMapList]
k:63 [in Coq.Reals.SeqProp]
k:63 [in Coq.Reals.Cos_rel]
k:630 [in Coq.MSets.MSetRBT]
k:639 [in Coq.micromega.Tauto]
k:64 [in Coq.Reals.Ranalysis4]
k:64 [in Coq.Reals.Exp_prop]
k:64 [in Coq.Structures.EqualitiesFacts]
k:64 [in Coq.Reals.Abstract.ConstructiveSum]
k:64 [in Coq.Reals.SeqProp]
k:64 [in Coq.micromega.Tauto]
k:641 [in Coq.micromega.Tauto]
k:647 [in Coq.micromega.Tauto]
k:65 [in Coq.Reals.Cauchy_prod]
k:65 [in Coq.Reals.Ranalysis4]
k:65 [in Coq.Reals.Exp_prop]
k:65 [in Coq.Logic.FunctionalExtensionality]
k:65 [in Coq.Reals.SeqProp]
k:65 [in Coq.Reals.Cos_rel]
k:65 [in Coq.Logic.FinFun]
k:66 [in Coq.Reals.Ranalysis4]
k:66 [in Coq.Numbers.Integer.Abstract.ZBits]
k:66 [in Coq.FSets.FMapList]
k:66 [in Coq.micromega.Tauto]
k:66 [in Coq.Reals.Cos_plus]
k:67 [in Coq.Reals.Cauchy_prod]
k:67 [in Coq.Reals.Rtrigo1]
k:67 [in Coq.Arith.Between]
k:67 [in Coq.Logic.FinFun]
k:68 [in Coq.Reals.SeqSeries]
k:68 [in Coq.ssr.ssreflect]
k:68 [in Coq.Structures.EqualitiesFacts]
k:68 [in Coq.Reals.SeqProp]
k:68 [in Coq.Reals.Cos_plus]
k:69 [in Coq.Reals.Cauchy_prod]
k:69 [in Coq.Reals.Rtrigo1]
k:69 [in Coq.Reals.SeqSeries]
k:69 [in Coq.Reals.Abstract.ConstructiveSum]
K:69 [in Coq.Numbers.Cyclic.Int63.Uint63]
k:69 [in Coq.Reals.SeqProp]
k:7 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
k:7 [in Coq.Arith.Between]
k:7 [in Coq.Structures.EqualitiesFacts]
k:7 [in Coq.Reals.Rsigma]
k:7 [in Coq.Reals.Rcomplete]
k:70 [in Coq.Reals.SeqSeries]
k:70 [in Coq.Structures.EqualitiesFacts]
k:70 [in Coq.Reals.SeqProp]
k:70 [in Coq.Reals.Cos_plus]
k:71 [in Coq.Reals.Cauchy_prod]
k:71 [in Coq.Reals.SeqSeries]
k:71 [in Coq.ssr.ssreflect]
k:71 [in Coq.MSets.MSetRBT]
k:71 [in Coq.Reals.SeqProp]
k:71 [in Coq.micromega.Tauto]
k:71 [in Coq.btauto.Reflect]
k:72 [in Coq.FSets.FMapInterface]
k:72 [in Coq.Reals.SeqProp]
k:72 [in Coq.Reals.Cos_plus]
k:73 [in Coq.Reals.Cauchy_prod]
k:73 [in Coq.FSets.FMapInterface]
k:73 [in Coq.Reals.SeqSeries]
k:73 [in Coq.Reals.SeqProp]
k:74 [in Coq.Reals.Rseries]
k:74 [in Coq.Reals.SeqSeries]
k:74 [in Coq.ssr.ssreflect]
k:74 [in Coq.Arith.Between]
k:74 [in Coq.Reals.SeqProp]
k:75 [in Coq.Reals.Cauchy_prod]
k:75 [in Coq.Reals.Ranalysis4]
k:75 [in Coq.omega.OmegaLemmas]
k:75 [in Coq.Arith.Between]
k:75 [in Coq.Reals.SeqProp]
k:75 [in Coq.micromega.Tauto]
k:76 [in Coq.MSets.MSetRBT]
k:76 [in Coq.Reals.PSeries_reg]
k:76 [in Coq.Reals.SeqProp]
k:77 [in Coq.Reals.Cauchy_prod]
k:77 [in Coq.Reals.Ranalysis4]
k:77 [in Coq.Reals.SeqSeries]
k:77 [in Coq.micromega.QMicromega]
k:77 [in Coq.Reals.SeqProp]
k:77 [in Coq.Reals.Cos_rel]
k:78 [in Coq.Vectors.VectorSpec]
k:78 [in Coq.Reals.Rseries]
k:78 [in Coq.Reals.SeqSeries]
k:78 [in Coq.Reals.PSeries_reg]
k:78 [in Coq.Reals.SeqProp]
k:78 [in Coq.micromega.Tauto]
k:79 [in Coq.Reals.Cauchy_prod]
k:79 [in Coq.Reals.Alembert]
k:79 [in Coq.Reals.PSeries_reg]
k:79 [in Coq.micromega.RMicromega]
k:79 [in Coq.Reals.SeqProp]
k:79 [in Coq.Reals.Cos_rel]
k:8 [in Coq.Reals.Rtrigo_reg]
k:8 [in Coq.Reals.Rtrigo1]
k:8 [in Coq.Reals.Exp_prop]
k:8 [in Coq.ZArith.Zpow_alt]
k:8 [in Coq.Reals.Rsigma]
k:8 [in Coq.Reals.Rcomplete]
k:80 [in Coq.btauto.Algebra]
k:80 [in Coq.Reals.SeqSeries]
k:80 [in Coq.Reals.PSeries_reg]
k:80 [in Coq.Reals.SeqProp]
k:80 [in Coq.micromega.Tauto]
k:80 [in Coq.Reals.Cos_plus]
k:81 [in Coq.Reals.Cauchy_prod]
k:81 [in Coq.Reals.Rseries]
k:81 [in Coq.omega.OmegaLemmas]
k:81 [in Coq.Reals.PSeries_reg]
k:81 [in Coq.Reals.SeqProp]
k:81 [in Coq.Reals.Cos_rel]
k:82 [in Coq.Reals.Ranalysis4]
k:82 [in Coq.Reals.SeqSeries]
k:82 [in Coq.Reals.PSeries_reg]
k:82 [in Coq.Reals.Abstract.ConstructiveSum]
k:82 [in Coq.Reals.SeqProp]
k:82 [in Coq.micromega.Tauto]
k:82 [in Coq.Reals.Cos_plus]
k:83 [in Coq.Reals.Cauchy_prod]
k:83 [in Coq.Reals.Ranalysis4]
k:83 [in Coq.Logic.FunctionalExtensionality]
k:83 [in Coq.Numbers.Natural.Abstract.NBits]
k:83 [in Coq.Reals.SeqSeries]
k:83 [in Coq.Reals.PSeries_reg]
k:83 [in Coq.Reals.Abstract.ConstructiveSum]
k:83 [in Coq.Reals.SeqProp]
k:83 [in Coq.Reals.Cos_rel]
k:84 [in Coq.Reals.Cauchy_prod]
k:84 [in Coq.Reals.Ranalysis4]
k:84 [in Coq.Reals.PSeries_reg]
k:84 [in Coq.Reals.Abstract.ConstructiveSum]
k:84 [in Coq.Reals.SeqProp]
k:84 [in Coq.Reals.Cos_plus]
k:85 [in Coq.Reals.SeqSeries]
k:85 [in Coq.Reals.PSeries_reg]
k:85 [in Coq.Structures.EqualitiesFacts]
k:85 [in Coq.Reals.Abstract.ConstructiveSum]
k:85 [in Coq.Reals.SeqProp]
k:85 [in Coq.micromega.Tauto]
k:85 [in Coq.Reals.Cos_plus]
k:86 [in Coq.Reals.Cauchy_prod]
k:86 [in Coq.Reals.SeqSeries]
k:86 [in Coq.Reals.PSeries_reg]
k:86 [in Coq.micromega.RMicromega]
k:86 [in Coq.Reals.Abstract.ConstructiveSum]
k:86 [in Coq.Reals.SeqProp]
k:867 [in Coq.Lists.List]
k:87 [in Coq.Reals.Cauchy_prod]
k:87 [in Coq.Reals.SeqSeries]
k:87 [in Coq.Arith.PeanoNat]
k:87 [in Coq.Reals.PSeries_reg]
k:87 [in Coq.Reals.SeqProp]
k:88 [in Coq.Reals.Ranalysis4]
k:88 [in Coq.Reals.SeqSeries]
k:88 [in Coq.Reals.PSeries_reg]
k:88 [in Coq.Reals.SeqProp]
k:88 [in Coq.Reals.Cos_rel]
k:89 [in Coq.Reals.Cauchy_prod]
k:89 [in Coq.btauto.Algebra]
k:89 [in Coq.Reals.SeqSeries]
k:89 [in Coq.Reals.PSeries_reg]
k:89 [in Coq.Reals.SeqProp]
k:89 [in Coq.micromega.Tauto]
k:9 [in Coq.Numbers.NatInt.NZDomain]
k:9 [in Coq.FSets.FMapWeakList]
k:9 [in Coq.Arith.Between]
k:9 [in Coq.FSets.FMapList]
k:9 [in Coq.Reals.Rsigma]
k:9 [in Coq.Reals.Rcomplete]
k:9 [in Coq.Reals.Cos_plus]
k:90 [in Coq.Reals.Cauchy_prod]
k:90 [in Coq.Reals.SeqSeries]
k:90 [in Coq.Structures.EqualitiesFacts]
k:90 [in Coq.Reals.SeqProp]
k:90 [in Coq.Reals.Cos_rel]
k:91 [in Coq.Reals.Cauchy_prod]
k:91 [in Coq.Logic.FunctionalExtensionality]
k:91 [in Coq.Reals.SeqSeries]
k:91 [in Coq.Reals.SeqProp]
k:92 [in Coq.Reals.Cauchy_prod]
k:92 [in Coq.Reals.SeqSeries]
k:92 [in Coq.Reals.SeqProp]
k:92 [in Coq.micromega.Tauto]
k:922 [in Coq.FSets.FMapAVL]
k:925 [in Coq.FSets.FMapAVL]
k:928 [in Coq.FSets.FMapAVL]
k:93 [in Coq.Reals.Cauchy_prod]
k:93 [in Coq.Reals.SeqSeries]
k:93 [in Coq.ssr.ssreflect]
k:93 [in Coq.Reals.SeqProp]
k:93 [in Coq.micromega.Tauto]
k:94 [in Coq.Reals.SeqSeries]
k:94 [in Coq.FSets.FMapWeakList]
k:94 [in Coq.Reals.Abstract.ConstructiveSum]
k:94 [in Coq.Reals.SeqProp]
k:94 [in Coq.micromega.Tauto]
k:94 [in Coq.Reals.Cos_rel]
k:95 [in Coq.Reals.SeqSeries]
k:95 [in Coq.Numbers.NatInt.NZOrder]
k:95 [in Coq.Reals.SeqProp]
k:95 [in Coq.micromega.Tauto]
k:96 [in Coq.Arith.PeanoNat]
k:96 [in Coq.Reals.SeqProp]
k:96 [in Coq.micromega.Tauto]
k:96 [in Coq.Reals.Cos_rel]
k:97 [in Coq.Reals.SeqProp]
k:97 [in Coq.micromega.Tauto]
k:98 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
k:98 [in Coq.btauto.Algebra]
k:98 [in Coq.Numbers.NatInt.NZOrder]
k:98 [in Coq.micromega.RMicromega]
k:98 [in Coq.micromega.Tauto]
k:99 [in Coq.Reals.Rfunctions]
k:99 [in Coq.FSets.FMapWeakList]
k:99 [in Coq.Reals.Cos_rel]


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 (72487 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 (1049 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 (47021 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 (788 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 (1537 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 (588 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 (11841 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 (1025 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 (634 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 (306 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 (473 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 (486 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 (881 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 (1465 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 (4229 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 (164 entries)