| 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 | (70451 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 | (1003 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 | (45703 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 | (771 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 | (1516 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 | (579 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 | (11670 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 | (1018 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 | (622 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 | (304 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 | (472 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 | (482 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 | (844 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 | (1187 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 | (4117 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 | (163 entries) |
B (binder)
base:142 [in Coq.micromega.RingMicromega]base:16 [in Coq.Strings.OctalString]
base:16 [in Coq.Strings.HexString]
base:16 [in Coq.Strings.BinaryString]
base:19 [in Coq.MSets.MSetGenTree]
base:424 [in Coq.micromega.ZMicromega]
bas:10 [in Coq.Vectors.VectorDef]
bas:54 [in Coq.Vectors.VectorDef]
bb:602 [in Coq.PArith.BinPos]
be:36 [in Coq.setoid_ring.Ncring_initial]
bg:38 [in Coq.setoid_ring.Ncring_initial]
bl:37 [in Coq.setoid_ring.Ncring_initial]
Bn:104 [in Coq.Reals.SeqSeries]
Bn:16 [in Coq.Reals.Rprod]
Bn:179 [in Coq.Reals.SeqProp]
Bn:201 [in Coq.Reals.SeqProp]
Bn:225 [in Coq.Reals.SeqProp]
Bn:35 [in Coq.Reals.PartSum]
Bn:4 [in Coq.Reals.Cauchy_prod]
Bn:52 [in Coq.Reals.PartSum]
Bn:55 [in Coq.Reals.Abstract.ConstructiveLimits]
Bn:56 [in Coq.Reals.PartSum]
Bn:63 [in Coq.Reals.PartSum]
Bn:74 [in Coq.Reals.PartSum]
Bn:8 [in Coq.Reals.Cauchy_prod]
Bn:8 [in Coq.Reals.Abstract.ConstructiveSum]
Bn:83 [in Coq.Reals.PartSum]
Bn:97 [in Coq.Reals.SeqSeries]
bot:23 [in Coq.Sets.Cpo]
bot:43 [in Coq.Sets.Cpo]
bsup:45 [in Coq.Sets.Cpo]
bsup:50 [in Coq.Sets.Cpo]
bv':176 [in Coq.NArith.Ndigits]
bv':179 [in Coq.NArith.Ndigits]
bv:10 [in Coq.Bool.Bvector]
bv:12 [in Coq.Bool.Bvector]
bv:14 [in Coq.ZArith.Zdigits]
bv:140 [in Coq.NArith.Ndigits]
bv:146 [in Coq.NArith.Ndigits]
bv:148 [in Coq.NArith.Ndigits]
bv:150 [in Coq.NArith.Ndigits]
bv:162 [in Coq.NArith.Ndigits]
bv:164 [in Coq.NArith.Ndigits]
bv:166 [in Coq.NArith.Ndigits]
bv:17 [in Coq.Bool.Bvector]
bv:175 [in Coq.NArith.Ndigits]
bv:178 [in Coq.NArith.Ndigits]
bv:19 [in Coq.ZArith.Zdigits]
bv:21 [in Coq.ZArith.Zdigits]
bv:22 [in Coq.Bool.Bvector]
bv:4 [in Coq.Bool.Bvector]
bv:41 [in Coq.ZArith.Zdigits]
bv:43 [in Coq.ZArith.Zdigits]
bv:7 [in Coq.Bool.Bvector]
b'':163 [in Coq.Bool.Bool]
b'':168 [in Coq.Bool.Bool]
b'':171 [in Coq.Bool.Bool]
b'':174 [in Coq.Bool.Bool]
b'':177 [in Coq.Bool.Bool]
b':105 [in Coq.Sorting.PermutSetoid]
b':15 [in Coq.Logic.Diaconescu]
b':154 [in Coq.Init.Nat]
b':160 [in Coq.Bool.Bool]
b':160 [in Coq.MSets.MSetPositive]
B':161 [in Coq.Init.Logic]
b':162 [in Coq.Bool.Bool]
b':165 [in Coq.Bool.Bool]
b':167 [in Coq.Bool.Bool]
b':170 [in Coq.Bool.Bool]
b':173 [in Coq.Bool.Bool]
b':176 [in Coq.Bool.Bool]
b':179 [in Coq.Bool.Bool]
b':181 [in Coq.Bool.Bool]
b':183 [in Coq.Bool.Bool]
b':184 [in Coq.FSets.FSetPositive]
b':191 [in Coq.Bool.Bool]
b':226 [in Coq.Bool.Bool]
b':245 [in Coq.Bool.Bool]
b':3 [in Coq.ssr.ssrbool]
b':4 [in Coq.FSets.FMapFacts]
b':48 [in Coq.Structures.OrdersFacts]
b':49 [in Coq.Bool.Bool]
b':67 [in Coq.Sorting.PermutSetoid]
b':72 [in Coq.Vectors.Fin]
b':84 [in Coq.Sorting.PermutSetoid]
b':88 [in Coq.Sorting.PermutSetoid]
b':91 [in Coq.Sorting.PermutSetoid]
b':99 [in Coq.Sorting.PermutSetoid]
b0:16 [in Coq.Strings.ByteVector]
b0:29 [in Coq.Numbers.Natural.Abstract.NBits]
b0:29 [in Coq.Numbers.Integer.Abstract.ZBits]
b0:338 [in Coq.Numbers.Natural.Abstract.NBits]
b0:402 [in Coq.Numbers.Integer.Abstract.ZBits]
b0:51 [in Coq.Strings.Ascii]
b1:10 [in Coq.Bool.Bool]
b1:100 [in Coq.Bool.Bool]
b1:104 [in Coq.Bool.Bool]
b1:106 [in Coq.Bool.Bool]
b1:109 [in Coq.Bool.Bool]
b1:11 [in Coq.Bool.BoolOrder]
b1:11 [in Coq.Init.Datatypes]
b1:112 [in Coq.Bool.Bool]
b1:115 [in Coq.Bool.Bool]
b1:118 [in Coq.Bool.Bool]
b1:121 [in Coq.Bool.Bool]
b1:123 [in Coq.Bool.Bool]
b1:125 [in Coq.Sorting.PermutSetoid]
b1:125 [in Coq.Bool.Bool]
b1:127 [in Coq.Bool.Bool]
b1:129 [in Coq.Bool.Bool]
b1:13 [in Coq.Bool.BoolOrder]
b1:13 [in Coq.Bool.Bool]
b1:13 [in Coq.Init.Datatypes]
b1:131 [in Coq.Bool.Bool]
b1:138 [in Coq.Bool.Bool]
b1:140 [in Coq.Bool.Bool]
b1:142 [in Coq.Bool.Bool]
b1:145 [in Coq.Bool.Bool]
b1:148 [in Coq.Bool.Bool]
b1:15 [in Coq.Bool.BoolOrder]
b1:15 [in Coq.Bool.Bool]
b1:150 [in Coq.Sorting.Permutation]
b1:151 [in Coq.Bool.Bool]
b1:165 [in Coq.MSets.MSetPositive]
b1:17 [in Coq.Bool.BoolOrder]
b1:18 [in Coq.Bool.Bool]
b1:18 [in Coq.Strings.ByteVector]
b1:184 [in Coq.Bool.Bool]
b1:186 [in Coq.Bool.Bool]
b1:189 [in Coq.FSets.FSetPositive]
b1:19 [in Coq.Bool.BoolOrder]
b1:2 [in Coq.Bool.BoolOrder]
b1:2 [in Coq.setoid_ring.Ring]
b1:20 [in Coq.Init.Datatypes]
b1:202 [in Coq.Logic.ClassicalFacts]
b1:206 [in Coq.Bool.Bool]
b1:207 [in Coq.Logic.ClassicalFacts]
b1:208 [in Coq.Bool.Bool]
b1:214 [in Coq.Bool.Bool]
b1:216 [in Coq.Bool.Bool]
b1:22 [in Coq.Bool.Bool]
b1:24 [in Coq.Bool.Bool]
b1:261 [in Coq.Logic.ClassicalFacts]
b1:263 [in Coq.Logic.ClassicalFacts]
b1:28 [in Coq.Sorting.PermutEq]
b1:29 [in Coq.Bool.Bool]
b1:3 [in Coq.micromega.ZifyBool]
b1:3 [in Coq.Bool.Bool]
b1:38 [in Coq.Bool.Bool]
b1:4 [in Coq.setoid_ring.Ring]
b1:403 [in Coq.micromega.ZMicromega]
b1:42 [in Coq.Bool.Bool]
b1:44 [in Coq.Bool.Bool]
b1:52 [in Coq.Strings.Ascii]
b1:55 [in Coq.Sorting.CPermutation]
b1:59 [in Coq.Bool.Bool]
b1:61 [in Coq.Bool.Bool]
b1:63 [in Coq.Bool.Bool]
b1:67 [in Coq.Bool.Bool]
b1:69 [in Coq.Bool.Bool]
b1:7 [in Coq.Init.Datatypes]
b1:70 [in Coq.Init.Datatypes]
b1:71 [in Coq.Bool.Bool]
b1:8 [in Coq.Bool.BoolOrder]
b1:80 [in Coq.Bool.Bool]
b1:82 [in Coq.Bool.Bool]
b1:85 [in Coq.Bool.Bool]
b1:87 [in Coq.Bool.Bool]
b1:9 [in Coq.Init.Datatypes]
b1:91 [in Coq.Bool.Bool]
b1:93 [in Coq.Bool.Bool]
b2:10 [in Coq.Init.Datatypes]
b2:101 [in Coq.Bool.Bool]
b2:105 [in Coq.Bool.Bool]
b2:107 [in Coq.Bool.Bool]
b2:11 [in Coq.Bool.Bool]
b2:110 [in Coq.Bool.Bool]
b2:113 [in Coq.Bool.Bool]
b2:116 [in Coq.Bool.Bool]
b2:119 [in Coq.Bool.Bool]
b2:12 [in Coq.Bool.BoolOrder]
b2:12 [in Coq.Init.Datatypes]
b2:122 [in Coq.Bool.Bool]
b2:124 [in Coq.Bool.Bool]
b2:126 [in Coq.Bool.Bool]
b2:127 [in Coq.Sorting.PermutSetoid]
b2:128 [in Coq.Bool.Bool]
b2:130 [in Coq.Bool.Bool]
b2:132 [in Coq.Bool.Bool]
b2:139 [in Coq.Bool.Bool]
b2:14 [in Coq.Bool.BoolOrder]
b2:14 [in Coq.Bool.Bool]
b2:14 [in Coq.Init.Datatypes]
b2:141 [in Coq.Bool.Bool]
b2:143 [in Coq.Bool.Bool]
b2:146 [in Coq.Bool.Bool]
b2:149 [in Coq.Bool.Bool]
b2:151 [in Coq.Sorting.Permutation]
b2:152 [in Coq.Bool.Bool]
b2:16 [in Coq.Bool.BoolOrder]
b2:16 [in Coq.Bool.Bool]
b2:166 [in Coq.MSets.MSetPositive]
b2:18 [in Coq.Bool.BoolOrder]
b2:185 [in Coq.Bool.Bool]
b2:187 [in Coq.Bool.Bool]
b2:19 [in Coq.Bool.Bool]
b2:190 [in Coq.FSets.FSetPositive]
b2:20 [in Coq.Bool.BoolOrder]
b2:20 [in Coq.Strings.ByteVector]
b2:203 [in Coq.Logic.ClassicalFacts]
b2:207 [in Coq.Bool.Bool]
b2:208 [in Coq.Logic.ClassicalFacts]
b2:209 [in Coq.Bool.Bool]
b2:21 [in Coq.Init.Datatypes]
b2:215 [in Coq.Bool.Bool]
b2:217 [in Coq.Bool.Bool]
b2:23 [in Coq.Bool.Bool]
b2:25 [in Coq.Bool.Bool]
b2:262 [in Coq.Logic.ClassicalFacts]
b2:264 [in Coq.Logic.ClassicalFacts]
b2:3 [in Coq.Bool.BoolOrder]
b2:3 [in Coq.setoid_ring.Ring]
b2:30 [in Coq.Sorting.PermutEq]
b2:30 [in Coq.Bool.Bool]
b2:39 [in Coq.Bool.Bool]
b2:4 [in Coq.micromega.ZifyBool]
b2:4 [in Coq.Bool.Bool]
b2:404 [in Coq.micromega.ZMicromega]
b2:43 [in Coq.Bool.Bool]
b2:45 [in Coq.Bool.Bool]
b2:5 [in Coq.setoid_ring.Ring]
b2:53 [in Coq.Strings.Ascii]
b2:56 [in Coq.Sorting.CPermutation]
b2:60 [in Coq.Bool.Bool]
b2:62 [in Coq.Bool.Bool]
b2:64 [in Coq.Bool.Bool]
b2:68 [in Coq.Bool.Bool]
b2:70 [in Coq.Bool.Bool]
b2:71 [in Coq.Init.Datatypes]
b2:72 [in Coq.Bool.Bool]
b2:8 [in Coq.Init.Datatypes]
b2:81 [in Coq.Bool.Bool]
b2:83 [in Coq.Bool.Bool]
b2:86 [in Coq.Bool.Bool]
b2:88 [in Coq.Bool.Bool]
b2:9 [in Coq.Bool.BoolOrder]
b2:92 [in Coq.Bool.Bool]
b2:94 [in Coq.Bool.Bool]
b3:10 [in Coq.Bool.BoolOrder]
b3:108 [in Coq.Bool.Bool]
b3:111 [in Coq.Bool.Bool]
b3:114 [in Coq.Bool.Bool]
b3:117 [in Coq.Bool.Bool]
b3:120 [in Coq.Bool.Bool]
b3:144 [in Coq.Bool.Bool]
b3:147 [in Coq.Bool.Bool]
b3:150 [in Coq.Bool.Bool]
b3:153 [in Coq.Bool.Bool]
b3:22 [in Coq.Strings.ByteVector]
b3:4 [in Coq.Bool.BoolOrder]
b3:40 [in Coq.Bool.Bool]
b3:54 [in Coq.Strings.Ascii]
b3:84 [in Coq.Bool.Bool]
b4:24 [in Coq.Strings.ByteVector]
b4:55 [in Coq.Strings.Ascii]
b5:26 [in Coq.Strings.ByteVector]
b5:56 [in Coq.Strings.Ascii]
b6:28 [in Coq.Strings.ByteVector]
b6:57 [in Coq.Strings.Ascii]
b7:30 [in Coq.Strings.ByteVector]
b7:58 [in Coq.Strings.Ascii]
b:1 [in Coq.Bool.BoolOrder]
b:1 [in Coq.setoid_ring.Ring]
b:1 [in Coq.ssr.ssrbool]
b:1 [in Coq.ZArith.Zdigits]
b:1 [in Coq.ZArith.Zdiv]
b:1 [in Coq.Bool.Bool]
b:1 [in Coq.Bool.Sumbool]
b:10 [in Coq.Logic.ConstructiveEpsilon]
b:10 [in Coq.Bool.IfProp]
b:10 [in Coq.ZArith.Zpow_facts]
B:10 [in Coq.Logic.JMeq]
b:10 [in Coq.Numbers.Natural.Abstract.NLcm]
b:10 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:10 [in Coq.Numbers.Natural.Abstract.NSqrt]
b:10 [in Coq.Numbers.Natural.Abstract.NBits]
b:10 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:10 [in Coq.ZArith.Zdiv]
b:10 [in Coq.Numbers.Integer.Abstract.ZBits]
b:10 [in Coq.Numbers.Integer.Abstract.ZPow]
B:10 [in Coq.Program.Basics]
b:10 [in Coq.ZArith.Znumtheory]
b:10 [in Coq.ZArith.Zeuclid]
b:10 [in Coq.Reals.Cauchy.QExtra]
b:100 [in Coq.Vectors.VectorSpec]
b:100 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:100 [in Coq.Numbers.Natural.Abstract.NDiv]
b:100 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:100 [in Coq.setoid_ring.Field_theory]
b:100 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:100 [in Coq.Numbers.NatInt.NZDiv]
b:100 [in Coq.Reals.RiemannInt_SF]
b:100 [in Coq.NArith.Ndec]
B:1001 [in Coq.Lists.List]
b:101 [in Coq.ZArith.BinIntDef]
b:101 [in Coq.ZArith.Zdiv]
b:101 [in Coq.Numbers.Integer.Abstract.ZBits]
b:101 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:101 [in Coq.Logic.ClassicalFacts]
b:101 [in Coq.PArith.BinPosDef]
b:101 [in Coq.ZArith.Znumtheory]
B:1011 [in Coq.Lists.List]
B:1017 [in Coq.Lists.List]
b:102 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
B:102 [in Coq.Logic.FunctionalExtensionality]
b:102 [in Coq.setoid_ring.Field_theory]
b:102 [in Coq.Bool.Bool]
b:102 [in Coq.ZArith.Zquot]
b:103 [in Coq.Numbers.Natural.Abstract.NDiv]
B:103 [in Coq.Sorting.PermutSetoid]
b:103 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:103 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:103 [in Coq.ZArith.Zdiv]
b:103 [in Coq.Bool.Bool]
b:103 [in Coq.Numbers.NatInt.NZDiv]
b:103 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:103 [in Coq.NArith.Ndec]
b:104 [in Coq.Sorting.PermutSetoid]
b:104 [in Coq.Reals.RiemannInt]
b:104 [in Coq.Reals.NewtonInt]
b:104 [in Coq.Numbers.Integer.Abstract.ZBits]
b:104 [in Coq.micromega.RMicromega]
b:1049 [in Coq.Lists.List]
b:105 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:105 [in Coq.Lists.List]
b:105 [in Coq.ZArith.Zdiv]
b:105 [in Coq.Arith.PeanoNat]
b:105 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:105 [in Coq.Logic.ClassicalFacts]
b:106 [in Coq.Numbers.Natural.Abstract.NDiv]
b:106 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:106 [in Coq.Numbers.Integer.Abstract.ZBits]
b:107 [in Coq.Vectors.VectorSpec]
B:107 [in Coq.ssr.ssreflect]
b:107 [in Coq.Arith.PeanoNat]
b:107 [in Coq.Reals.Rbasic_fun]
b:107 [in Coq.ZArith.Zquot]
b:107 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:107 [in Coq.PArith.BinPosDef]
b:108 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:108 [in Coq.FSets.FMapFacts]
b:108 [in Coq.Init.Nat]
b:108 [in Coq.ZArith.Zdiv]
b:108 [in Coq.Numbers.Integer.Abstract.ZBits]
b:108 [in Coq.Numbers.NatInt.NZDiv]
B:108 [in Coq.Init.Logic]
b:108 [in Coq.Reals.RiemannInt_SF]
b:108 [in Coq.ZArith.Znumtheory]
b:109 [in Coq.Numbers.Natural.Abstract.NDiv]
b:109 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:109 [in Coq.Reals.RiemannInt]
b:109 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:109 [in Coq.Arith.PeanoNat]
b:109 [in Coq.Reals.Rbasic_fun]
b:109 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:109 [in Coq.Numbers.NatInt.NZMulOrder]
B:11 [in Coq.Logic.Decidable]
b:11 [in Coq.Logic.ConstructiveEpsilon]
b:11 [in Coq.Numbers.Natural.Abstract.NDiv]
b:11 [in Coq.Numbers.Natural.Abstract.NPow]
b:11 [in Coq.Numbers.Natural.Abstract.NDefOps]
b:11 [in Coq.Reals.RiemannInt]
B:11 [in Coq.Program.Subset]
b:11 [in Coq.ssr.ssrbool]
b:11 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:11 [in Coq.setoid_ring.Algebra_syntax]
B:11 [in Coq.Logic.ClassicalChoice]
B:11 [in Coq.Logic.IndefiniteDescription]
B:11 [in Coq.rtauto.Bintree]
B:11 [in Coq.Classes.CRelationClasses]
b:11 [in Coq.Numbers.Cyclic.Int31.Int31]
b:11 [in Coq.ZArith.Zquot]
b:11 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:11 [in Coq.micromega.Refl]
B:110 [in Coq.ssr.ssreflect]
b:110 [in Coq.Reals.NewtonInt]
b:110 [in Coq.ZArith.Zquot]
b:110 [in Coq.PArith.BinPosDef]
b:111 [in Coq.ZArith.Zdiv]
b:111 [in Coq.Arith.PeanoNat]
b:111 [in Coq.Reals.Rbasic_fun]
b:111 [in Coq.Numbers.Integer.Abstract.ZBits]
b:111 [in Coq.Numbers.NatInt.NZDiv]
b:111 [in Coq.Numbers.NatInt.NZMulOrder]
b:111 [in Coq.ZArith.Znumtheory]
b:112 [in Coq.Numbers.Natural.Abstract.NDiv]
b:112 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:112 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:112 [in Coq.Structures.OrderedTypeEx]
b:112 [in Coq.Reals.Abstract.ConstructiveLimits]
b:112 [in Coq.MSets.MSetPositive]
b:112 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:112 [in Coq.Logic.ClassicalFacts]
b:112 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
b:112 [in Coq.Reals.RiemannInt_SF]
b:113 [in Coq.Vectors.VectorSpec]
b:113 [in Coq.ZArith.BinIntDef]
b:113 [in Coq.Reals.Rbasic_fun]
b:113 [in Coq.ZArith.Zquot]
b:113 [in Coq.Numbers.NatInt.NZMulOrder]
b:114 [in Coq.Reals.RiemannInt]
b:114 [in Coq.Arith.PeanoNat]
b:114 [in Coq.Numbers.NatInt.NZDiv]
b:115 [in Coq.Numbers.Natural.Abstract.NDiv]
b:115 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:115 [in Coq.FSets.FSetPositive]
b:115 [in Coq.Reals.Rbasic_fun]
b:115 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:115 [in Coq.ZArith.Znumtheory]
B:115 [in Coq.micromega.Tauto]
b:116 [in Coq.ZArith.BinIntDef]
b:116 [in Coq.Structures.OrderedTypeEx]
b:116 [in Coq.ZArith.Zquot]
b:116 [in Coq.Numbers.NatInt.NZMulOrder]
b:116 [in Coq.Logic.ClassicalFacts]
b:116 [in Coq.Reals.Abstract.ConstructiveMinMax]
b:117 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:117 [in Coq.Reals.MVT]
b:117 [in Coq.ZArith.Zdiv]
b:117 [in Coq.Numbers.NatInt.NZDiv]
b:117 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
b:117 [in Coq.ZArith.Znumtheory]
b:118 [in Coq.Numbers.Natural.Abstract.NDiv]
b:118 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:118 [in Coq.Numbers.NatInt.NZMulOrder]
b:118 [in Coq.PArith.BinPosDef]
b:119 [in Coq.Vectors.VectorSpec]
b:119 [in Coq.ZArith.BinIntDef]
b:119 [in Coq.ZArith.Zdiv]
b:119 [in Coq.ZArith.Zquot]
B:119 [in Coq.Logic.ClassicalFacts]
b:119 [in Coq.ZArith.Znumtheory]
b:12 [in Coq.Reals.Runcountable]
b:12 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:12 [in Coq.Bool.IfProp]
B:12 [in Coq.Classes.RelationPairs]
b:12 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:12 [in Coq.Numbers.Natural.Abstract.NSqrt]
b:12 [in Coq.Numbers.Natural.Abstract.NBits]
b:12 [in Coq.Numbers.NatInt.NZLog]
b:12 [in Coq.ZArith.Zdiv]
b:12 [in Coq.Sorting.Sorted]
B:12 [in Coq.Logic.ClassicalUniqueChoice]
b:12 [in Coq.Reals.NewtonInt]
b:12 [in Coq.ZArith.Zgcd_alt]
b:12 [in Coq.ZArith.Zpow_alt]
b:12 [in Coq.Numbers.Integer.Abstract.ZBits]
b:12 [in Coq.Numbers.Integer.Abstract.ZPow]
B:12 [in Coq.Program.Basics]
b:12 [in Coq.ZArith.Znumtheory]
b:12 [in Coq.QArith.Qpower]
b:12 [in Coq.QArith.QArith_base]
B:12 [in Coq.Logic.FinFun]
b:120 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:120 [in Coq.Numbers.NatInt.NZDiv]
b:120 [in Coq.Numbers.NatInt.NZMulOrder]
b:121 [in Coq.Numbers.Natural.Abstract.NDiv]
b:121 [in Coq.setoid_ring.Field_theory]
b:121 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:121 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:121 [in Coq.ZArith.Znumtheory]
b:122 [in Coq.ZArith.Zdiv]
b:122 [in Coq.ZArith.Zquot]
b:122 [in Coq.Numbers.NatInt.NZMulOrder]
b:122 [in Coq.Logic.ClassicalFacts]
b:122 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
b:123 [in Coq.Sorting.PermutSetoid]
b:123 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:123 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
b:123 [in Coq.Numbers.NatInt.NZDiv]
b:123 [in Coq.Logic.ClassicalFacts]
b:124 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:124 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:124 [in Coq.Numbers.NatInt.NZMulOrder]
b:124 [in Coq.ZArith.Znumtheory]
b:1241 [in Coq.FSets.FMapAVL]
b:1244 [in Coq.FSets.FMapAVL]
b:125 [in Coq.Logic.FunctionalExtensionality]
b:125 [in Coq.ssr.ssrbool]
b:125 [in Coq.ZArith.Zdiv]
b:125 [in Coq.ZArith.Zquot]
b:125 [in Coq.Reals.RiemannInt_SF]
b:126 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:126 [in Coq.Structures.OrderedTypeEx]
B:126 [in Coq.Classes.CMorphisms]
b:126 [in Coq.Numbers.NatInt.NZDiv]
b:126 [in Coq.Numbers.NatInt.NZMulOrder]
b:127 [in Coq.Reals.MVT]
b:127 [in Coq.Logic.FunctionalExtensionality]
b:127 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:127 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:127 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
b:127 [in Coq.ZArith.Znumtheory]
b:128 [in Coq.ssr.ssrbool]
b:128 [in Coq.ZArith.Zdiv]
b:128 [in Coq.ZArith.Zquot]
B:129 [in Coq.Vectors.VectorSpec]
b:129 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:129 [in Coq.Numbers.NatInt.NZDiv]
b:13 [in Coq.Wellfounded.Inverse_Image]
b:13 [in Coq.Reals.Abstract.ConstructiveLUB]
b:13 [in Coq.ZArith.BinInt]
b:13 [in Coq.Reals.Cauchy.ConstructiveRcomplete]
B:13 [in Coq.Logic.FunctionalExtensionality]
b:13 [in Coq.Numbers.Natural.Abstract.NLcm]
B:13 [in Coq.Logic.Hurkens]
b:13 [in Coq.ZArith.Zdigits]
B:13 [in Coq.Sets.Cpo]
b:13 [in Coq.Strings.Ascii]
b:13 [in Coq.ZArith.Zquot]
B:13 [in Coq.Bool.Sumbool]
B:13 [in Coq.Sets.Powerset_facts]
b:13 [in Coq.Numbers.NatInt.NZSqrt]
b:13 [in Coq.Logic.Diaconescu]
B:13 [in Coq.Init.Logic]
b:130 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:130 [in Coq.ZArith.Zdiv]
b:130 [in Coq.Reals.Rbasic_fun]
b:130 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:130 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
b:130 [in Coq.Reals.RiemannInt_SF]
b:131 [in Coq.ZArith.BinIntDef]
b:131 [in Coq.Logic.FunctionalExtensionality]
b:131 [in Coq.Structures.OrderedTypeEx]
B:131 [in Coq.Classes.CMorphisms]
b:131 [in Coq.ZArith.Zquot]
b:131 [in Coq.Logic.ClassicalFacts]
b:131 [in Coq.ZArith.Znumtheory]
b:131 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:131 [in Coq.Relations.Relation_Operators]
b:132 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:132 [in Coq.ZArith.Zdiv]
b:132 [in Coq.Numbers.NatInt.NZDiv]
b:132 [in Coq.Reals.Cauchy.ConstructiveCauchyReals]
b:133 [in Coq.ZArith.BinIntDef]
b:133 [in Coq.ZArith.BinInt]
b:133 [in Coq.Numbers.Natural.Abstract.NBits]
b:133 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:133 [in Coq.Bool.Bool]
b:133 [in Coq.Structures.OrderedTypeEx]
b:133 [in Coq.Reals.Rbasic_fun]
b:133 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:133 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
b:133 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:134 [in Coq.Reals.Ranalysis1]
b:134 [in Coq.Reals.MVT]
b:134 [in Coq.ZArith.Zdiv]
b:134 [in Coq.Bool.Bool]
b:134 [in Coq.ZArith.Znumtheory]
b:134 [in Coq.QArith.QArith_base]
b:135 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:135 [in Coq.Logic.ChoiceFacts]
b:135 [in Coq.Numbers.Natural.Abstract.NBits]
b:135 [in Coq.Bool.Bool]
b:135 [in Coq.Structures.OrderedTypeEx]
b:135 [in Coq.Numbers.NatInt.NZDiv]
b:136 [in Coq.Reals.RiemannInt]
b:136 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:136 [in Coq.ZArith.Zdiv]
b:136 [in Coq.Bool.Bool]
B:136 [in Coq.Classes.CMorphisms]
b:136 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:136 [in Coq.Logic.ClassicalFacts]
b:136 [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
B:137 [in Coq.Vectors.VectorSpec]
b:137 [in Coq.ZArith.BinInt]
B:137 [in Coq.Logic.FunctionalExtensionality]
B:137 [in Coq.Logic.ChoiceFacts]
b:137 [in Coq.Bool.Bool]
b:137 [in Coq.Structures.OrderedTypeEx]
b:138 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:138 [in Coq.ZArith.Zdiv]
B:138 [in Coq.Classes.CMorphisms]
B:139 [in Coq.Logic.ChoiceFacts]
b:139 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:139 [in Coq.ZArith.Zquot]
b:139 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:139 [in Coq.Logic.ClassicalFacts]
B:14 [in Coq.Logic.Decidable]
b:14 [in Coq.Wellfounded.Inverse_Image]
b:14 [in Coq.Logic.ConstructiveEpsilon]
b:14 [in Coq.Numbers.Natural.Abstract.NPow]
B:14 [in Coq.Bool.IfProp]
B:14 [in Coq.Logic.JMeq]
B:14 [in Coq.Classes.RelationPairs]
b:14 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:14 [in Coq.Numbers.Natural.Abstract.NBits]
b:14 [in Coq.ssr.ssrbool]
b:14 [in Coq.micromega.ZifyBool]
b:14 [in Coq.ZArith.Zdiv]
b:14 [in Coq.Wellfounded.Lexicographic_Exponentiation]
b:14 [in Coq.Reals.Abstract.ConstructiveLimits]
B:14 [in Coq.Classes.SetoidDec]
b:14 [in Coq.Numbers.Integer.Abstract.ZBits]
b:14 [in Coq.Bool.Sumbool]
b:14 [in Coq.Logic.Diaconescu]
b:14 [in Coq.Numbers.Integer.Abstract.ZPow]
B:14 [in Coq.Logic.ClassicalFacts]
b:14 [in Coq.ZArith.Znumtheory]
B:14 [in Coq.Bool.DecBool]
b:140 [in Coq.Numbers.Natural.Abstract.NBits]
b:140 [in Coq.ZArith.Zdiv]
b:140 [in Coq.Structures.OrderedTypeEx]
b:141 [in Coq.ZArith.BinInt]
b:141 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:141 [in Coq.Logic.ChoiceFacts]
b:141 [in Coq.Arith.PeanoNat]
b:141 [in Coq.ZArith.Zquot]
b:142 [in Coq.Reals.MVT]
B:142 [in Coq.Logic.FunctionalExtensionality]
b:142 [in Coq.Numbers.Natural.Abstract.NBits]
b:142 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:142 [in Coq.ZArith.Zdiv]
B:142 [in Coq.Logic.ClassicalFacts]
b:143 [in Coq.ZArith.BinInt]
b:143 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:143 [in Coq.Reals.RiemannInt]
b:143 [in Coq.Structures.OrderedTypeEx]
b:143 [in Coq.ZArith.Zquot]
B:143 [in Coq.Lists.ListSet]
B:144 [in Coq.Vectors.VectorSpec]
b:144 [in Coq.Init.Nat]
b:144 [in Coq.Sorting.Permutation]
b:144 [in Coq.ZArith.Zdiv]
b:144 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:144 [in Coq.Relations.Relation_Operators]
B:145 [in Coq.Logic.ChoiceFacts]
b:145 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:145 [in Coq.Arith.PeanoNat]
b:145 [in Coq.ZArith.Zquot]
B:145 [in Coq.Lists.ListSet]
b:145 [in Coq.ZArith.Znumtheory]
b:146 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:146 [in Coq.Numbers.Natural.Abstract.NBits]
b:146 [in Coq.setoid_ring.Field_theory]
b:146 [in Coq.ZArith.Zdiv]
b:146 [in Coq.Structures.OrderedTypeEx]
B:146 [in Coq.Logic.ClassicalFacts]
b:147 [in Coq.Reals.RiemannInt]
B:147 [in Coq.Logic.ChoiceFacts]
b:147 [in Coq.Arith.PeanoNat]
B:147 [in Coq.Lists.ListSet]
b:147 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:148 [in Coq.Numbers.Natural.Abstract.NBits]
b:148 [in Coq.Init.Nat]
b:148 [in Coq.ZArith.Zdiv]
b:148 [in Coq.Reals.RiemannInt_SF]
b:149 [in Coq.ZArith.BinIntDef]
b:149 [in Coq.ZArith.BinInt]
b:149 [in Coq.Reals.MVT]
B:149 [in Coq.Logic.ChoiceFacts]
B:149 [in Coq.Lists.ListSet]
b:15 [in Coq.Numbers.Natural.Abstract.NDiv]
b:15 [in Coq.Reals.Rtrigo_facts]
B:15 [in Coq.Sets.Ensembles]
b:15 [in Coq.ZArith.BinInt]
B:15 [in Coq.Numbers.NaryFunctions]
b:15 [in Coq.Numbers.Natural.Abstract.NLcm]
B:15 [in Coq.MSets.MSetWeakList]
b:15 [in Coq.micromega.ZifyBool]
b:15 [in Coq.QArith.Qfield]
b:15 [in Coq.QArith.Qabs]
b:15 [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
b:15 [in Coq.ZArith.Zgcd_alt]
b:15 [in Coq.ZArith.Zpow_alt]
b:15 [in Coq.ZArith.Zquot]
B:15 [in Coq.Program.Combinators]
b:15 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:15 [in Coq.Program.Basics]
b:15 [in Coq.QArith.Qpower]
b:150 [in Coq.Init.Nat]
b:150 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:150 [in Coq.Logic.Hurkens]
B:150 [in Coq.Classes.CMorphisms]
b:150 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:151 [in Coq.Vectors.VectorSpec]
b:151 [in Coq.ZArith.BinInt]
b:151 [in Coq.ZArith.Zdiv]
b:151 [in Coq.Arith.PeanoNat]
B:152 [in Coq.Logic.ChoiceFacts]
b:152 [in Coq.Numbers.Natural.Abstract.NBits]
b:152 [in Coq.Init.Nat]
b:152 [in Coq.Logic.Hurkens]
b:152 [in Coq.Lists.ListSet]
b:153 [in Coq.ZArith.BinIntDef]
b:153 [in Coq.ZArith.BinInt]
b:153 [in Coq.Init.Nat]
b:153 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:153 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:153 [in Coq.Logic.ClassicalFacts]
b:154 [in Coq.Numbers.Cyclic.Int63.Int63]
B:154 [in Coq.Logic.ChoiceFacts]
b:154 [in Coq.Numbers.Natural.Abstract.NBits]
b:154 [in Coq.ZArith.Zdiv]
b:154 [in Coq.Bool.Bool]
B:154 [in Coq.Lists.ListSet]
b:155 [in Coq.ZArith.BinInt]
b:155 [in Coq.Bool.Bool]
B:156 [in Coq.Logic.ChoiceFacts]
b:156 [in Coq.Init.Nat]
b:156 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:156 [in Coq.Bool.Bool]
b:156 [in Coq.Arith.PeanoNat]
b:156 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:157 [in Coq.Reals.MVT]
b:157 [in Coq.NArith.BinNat]
b:157 [in Coq.ZArith.Zdiv]
b:157 [in Coq.Bool.Bool]
b:157 [in Coq.Logic.ClassicalFacts]
b:157 [in Coq.Reals.RiemannInt_SF]
b:158 [in Coq.Reals.RiemannInt]
B:158 [in Coq.Logic.ChoiceFacts]
b:158 [in Coq.Bool.Bool]
b:158 [in Coq.Arith.PeanoNat]
b:158 [in Coq.Reals.Rtopology]
b:158 [in Coq.ZArith.Znumtheory]
B:159 [in Coq.Vectors.VectorSpec]
b:159 [in Coq.ZArith.BinInt]
b:159 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:159 [in Coq.Bool.Bool]
b:159 [in Coq.MSets.MSetPositive]
b:159 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:16 [in Coq.Logic.Decidable]
b:16 [in Coq.Wellfounded.Inverse_Image]
b:16 [in Coq.Numbers.NatInt.NZPow]
b:16 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:16 [in Coq.Bool.IfProp]
B:16 [in Coq.Classes.RelationPairs]
b:16 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:16 [in Coq.Numbers.Natural.Abstract.NSqrt]
b:16 [in Coq.ssr.ssrbool]
b:16 [in Coq.ZArith.Zdigits]
b:16 [in Coq.ZArith.Zdiv]
B:16 [in Coq.Program.Equality]
B:16 [in Coq.rtauto.Bintree]
B:16 [in Coq.Classes.EquivDec]
b:16 [in Coq.Reals.NewtonInt]
b:16 [in Coq.Numbers.Integer.Abstract.ZPow]
b:16 [in Coq.Reals.R_sqr]
b:16 [in Coq.ZArith.Znumtheory]
b:16 [in Coq.Sets.Powerset]
B:160 [in Coq.Classes.Morphisms]
B:160 [in Coq.Logic.ChoiceFacts]
B:160 [in Coq.Init.Logic]
B:160 [in Coq.Logic.ClassicalFacts]
b:161 [in Coq.ZArith.BinInt]
b:161 [in Coq.Numbers.Natural.Abstract.NBits]
b:161 [in Coq.NArith.BinNat]
b:161 [in Coq.Bool.Bool]
b:161 [in Coq.Arith.PeanoNat]
b:162 [in Coq.Reals.RiemannInt]
B:162 [in Coq.Logic.ChoiceFacts]
b:162 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:162 [in Coq.ZArith.Zdiv]
b:162 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:162 [in Coq.Reals.RiemannInt_SF]
b:163 [in Coq.ZArith.BinInt]
b:163 [in Coq.Numbers.Cyclic.Int31.Int31]
b:163 [in Coq.Logic.ClassicalFacts]
B:164 [in Coq.Logic.ChoiceFacts]
b:164 [in Coq.Numbers.Natural.Abstract.NBits]
b:164 [in Coq.Bool.Bool]
b:164 [in Coq.Arith.PeanoNat]
b:164 [in Coq.Logic.ClassicalFacts]
b:165 [in Coq.ZArith.BinInt]
b:165 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:165 [in Coq.NArith.BinNat]
b:165 [in Coq.ZArith.Zdiv]
b:165 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:166 [in Coq.ZArith.BinIntDef]
b:166 [in Coq.Reals.RiemannInt]
B:166 [in Coq.Logic.ChoiceFacts]
b:166 [in Coq.Sorting.Permutation]
b:166 [in Coq.Bool.Bool]
b:167 [in Coq.ZArith.BinInt]
b:167 [in Coq.Numbers.Natural.Abstract.NBits]
b:167 [in Coq.NArith.BinNat]
b:167 [in Coq.Arith.PeanoNat]
b:168 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:168 [in Coq.ZArith.Zdiv]
b:168 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:168 [in Coq.ZArith.Znumtheory]
B:169 [in Coq.Vectors.VectorSpec]
b:169 [in Coq.Logic.Eqdep_dec]
b:169 [in Coq.ZArith.BinInt]
b:169 [in Coq.NArith.BinNat]
b:169 [in Coq.Bool.Bool]
b:169 [in Coq.Numbers.Cyclic.Int31.Int31]
b:17 [in Coq.Reals.Runcountable]
b:17 [in Coq.Numbers.Natural.Abstract.NPow]
b:17 [in Coq.Bool.IfProp]
b:17 [in Coq.Numbers.Natural.Abstract.NLcm]
b:17 [in Coq.Reals.RiemannInt]
b:17 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:17 [in Coq.Reals.Abstract.ConstructiveAbs]
b:17 [in Coq.Wellfounded.Lexicographic_Exponentiation]
b:17 [in Coq.ZArith.Zgcd_alt]
b:17 [in Coq.ZArith.Zpow_alt]
b:17 [in Coq.ZArith.Zquot]
b:17 [in Coq.Init.Datatypes]
B:17 [in Coq.Init.Logic]
b:170 [in Coq.ZArith.BinIntDef]
B:170 [in Coq.Classes.Morphisms]
b:170 [in Coq.Reals.RiemannInt]
b:170 [in Coq.Numbers.Natural.Abstract.NBits]
b:170 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:171 [in Coq.ZArith.BinInt]
b:171 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:171 [in Coq.NArith.BinNat]
b:171 [in Coq.Reals.Rpower]
b:171 [in Coq.ZArith.Zdiv]
b:171 [in Coq.Numbers.Integer.Abstract.ZBits]
b:171 [in Coq.Reals.RiemannInt_SF]
b:172 [in Coq.Vectors.VectorSpec]
b:172 [in Coq.Bool.Bool]
b:172 [in Coq.Logic.ClassicalFacts]
b:173 [in Coq.FSets.FMapFacts]
b:173 [in Coq.Numbers.Natural.Abstract.NBits]
b:173 [in Coq.NArith.BinNat]
b:173 [in Coq.Numbers.Integer.Abstract.ZBits]
b:173 [in Coq.Reals.RiemannInt_SF]
b:174 [in Coq.ZArith.BinIntDef]
b:174 [in Coq.FSets.FMapFacts]
b:174 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:174 [in Coq.Reals.Rpower]
b:174 [in Coq.ZArith.Zdiv]
b:175 [in Coq.Reals.RiemannInt]
b:175 [in Coq.Bool.Bool]
B:176 [in Coq.PArith.BinPos]
b:176 [in Coq.Reals.MVT]
b:176 [in Coq.Numbers.Natural.Abstract.NBits]
b:176 [in Coq.ZArith.Znumtheory]
B:177 [in Coq.Classes.Morphisms]
b:177 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:177 [in Coq.ZArith.Zdiv]
b:178 [in Coq.ZArith.BinIntDef]
b:178 [in Coq.Numbers.Natural.Abstract.NBits]
b:178 [in Coq.Bool.Bool]
b:178 [in Coq.Numbers.Integer.Abstract.ZBits]
b:179 [in Coq.ZArith.BinInt]
b:179 [in Coq.Reals.RiemannInt]
b:179 [in Coq.setoid_ring.Ring_theory]
b:179 [in Coq.ZArith.Znumtheory]
B:18 [in Coq.Logic.Decidable]
b:18 [in Coq.Logic.ConstructiveEpsilon]
b:18 [in Coq.Reals.Rtrigo_facts]
b:18 [in Coq.Numbers.NatInt.NZPow]
b:18 [in Coq.ZArith.Zpow_facts]
b:18 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:18 [in Coq.ZArith.Wf_Z]
b:18 [in Coq.Numbers.Natural.Abstract.NSqrt]
b:18 [in Coq.ssr.ssrbool]
B:18 [in Coq.Logic.Hurkens]
B:18 [in Coq.Sets.Cpo]
B:18 [in Coq.Classes.CMorphisms]
B:18 [in Coq.Program.Combinators]
b:18 [in Coq.Numbers.NatInt.NZSqrt]
b:18 [in Coq.Numbers.Integer.Abstract.ZPow]
b:18 [in Coq.Reals.R_sqr]
b:180 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:180 [in Coq.ZArith.Zdiv]
b:180 [in Coq.Bool.Bool]
b:180 [in Coq.Numbers.Integer.Abstract.ZBits]
b:180 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:181 [in Coq.ZArith.BinInt]
b:181 [in Coq.ZArith.Znumtheory]
b:182 [in Coq.NArith.BinNat]
b:182 [in Coq.Bool.Bool]
B:182 [in Coq.FSets.FMapPositive]
b:182 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:183 [in Coq.ZArith.BinInt]
b:183 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:183 [in Coq.ZArith.Zdiv]
b:183 [in Coq.FSets.FSetPositive]
b:183 [in Coq.Reals.RiemannInt_SF]
b:183 [in Coq.QArith.QArith_base]
b:184 [in Coq.Reals.RiemannInt]
b:184 [in Coq.NArith.BinNat]
b:184 [in Coq.Numbers.Integer.Abstract.ZBits]
B:184 [in Coq.Init.Logic]
b:184 [in Coq.ZArith.Znumtheory]
b:185 [in Coq.ZArith.BinInt]
b:186 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:186 [in Coq.NArith.BinNat]
b:186 [in Coq.ZArith.Zdiv]
b:186 [in Coq.Numbers.Integer.Abstract.ZBits]
b:186 [in Coq.QArith.QArith_base]
b:187 [in Coq.ZArith.BinInt]
b:187 [in Coq.FSets.FMapFacts]
b:187 [in Coq.ssr.ssrbool]
b:187 [in Coq.Reals.RiemannInt_SF]
b:187 [in Coq.ZArith.Znumtheory]
b:188 [in Coq.FSets.FMapFacts]
b:188 [in Coq.ssr.ssrbool]
b:188 [in Coq.NArith.BinNat]
b:188 [in Coq.Bool.Bool]
B:188 [in Coq.FSets.FMapPositive]
b:188 [in Coq.micromega.ZMicromega]
b:189 [in Coq.ssr.ssrbool]
b:189 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:189 [in Coq.Bool.Bool]
b:189 [in Coq.MSets.MSetRBT]
b:189 [in Coq.Reals.Ranalysis5]
b:189 [in Coq.ZArith.Znumtheory]
b:19 [in Coq.Numbers.Natural.Abstract.NDiv]
b:19 [in Coq.Numbers.Natural.Abstract.NPow]
B:19 [in Coq.Bool.IfProp]
B:19 [in Coq.Classes.Morphisms]
B:19 [in Coq.Logic.ExtensionalityFacts]
b:19 [in Coq.Numbers.Natural.Abstract.NLcm]
b:19 [in Coq.Numbers.NatInt.NZLog]
B:19 [in Coq.Classes.CEquivalence]
B:19 [in Coq.Lists.ListDec]
b:19 [in Coq.Sorting.Sorted]
b:19 [in Coq.Reals.Abstract.ConstructiveLimits]
b:19 [in Coq.FSets.FSetPositive]
b:19 [in Coq.MSets.MSetPositive]
b:19 [in Coq.ZArith.Zquot]
b:19 [in Coq.Init.Datatypes]
b:19 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:19 [in Coq.Reals.Rgeom]
b:19 [in Coq.Reals.RiemannInt_SF]
b:19 [in Coq.Logic.StrictProp]
b:19 [in Coq.Sets.Powerset]
B:19 [in Coq.Classes.Equivalence]
b:190 [in Coq.ssr.ssrbool]
b:190 [in Coq.NArith.BinNat]
b:190 [in Coq.ZArith.Zdiv]
b:190 [in Coq.Bool.Bool]
b:190 [in Coq.Numbers.Integer.Abstract.ZBits]
B:190 [in Coq.Logic.ClassicalFacts]
b:190 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:191 [in Coq.ssr.ssrbool]
B:191 [in Coq.Logic.Hurkens]
B:192 [in Coq.Classes.Morphisms]
b:192 [in Coq.Reals.RiemannInt]
b:192 [in Coq.ssr.ssrbool]
b:192 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:192 [in Coq.Bool.Bool]
b:192 [in Coq.Numbers.Integer.Abstract.ZBits]
b:193 [in Coq.NArith.BinNat]
b:193 [in Coq.ZArith.Zdiv]
B:193 [in Coq.Classes.CMorphisms]
B:193 [in Coq.Init.Logic]
b:193 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:193 [in Coq.micromega.ZMicromega]
b:194 [in Coq.Reals.MVT]
b:194 [in Coq.ssr.ssrbool]
B:195 [in Coq.Logic.ChoiceFacts]
b:195 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:195 [in Coq.ZArith.Zdiv]
b:195 [in Coq.MSets.MSetPositive]
b:195 [in Coq.micromega.ZMicromega]
b:196 [in Coq.ZArith.BinInt]
b:196 [in Coq.ssr.ssrbool]
B:196 [in Coq.Logic.ClassicalFacts]
b:197 [in Coq.Sorting.Permutation]
B:197 [in Coq.Vectors.VectorDef]
b:198 [in Coq.Reals.Ranalysis1]
b:198 [in Coq.ZArith.BinInt]
b:198 [in Coq.ssr.ssrbool]
b:198 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:199 [in Coq.ZArith.Zdiv]
b:199 [in Coq.MSets.MSetPositive]
b:199 [in Coq.Numbers.Integer.Abstract.ZBits]
B:2 [in Coq.Wellfounded.Well_Ordering]
B:2 [in Coq.Logic.ExtensionalFunctionRepresentative]
b:2 [in Coq.Numbers.Natural.Abstract.NDiv]
B:2 [in Coq.Sets.Constructive_sets]
b:2 [in Coq.Numbers.Natural.Abstract.NPow]
b:2 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:2 [in Coq.Logic.SetoidChoice]
B:2 [in Coq.Bool.IfProp]
B:2 [in Coq.Classes.Morphisms]
B:2 [in Coq.Classes.RelationPairs]
B:2 [in Coq.Logic.ExtensionalityFacts]
B:2 [in Coq.Logic.FunctionalExtensionality]
b:2 [in Coq.Numbers.Natural.Abstract.NLcm]
b:2 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:2 [in Coq.Numbers.Natural.Abstract.NBits]
b:2 [in Coq.ssr.ssrbool]
b:2 [in Coq.micromega.ZifyBool]
b:2 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:2 [in Coq.Relations.Relations]
B:2 [in Coq.Logic.ClassicalUniqueChoice]
B:2 [in Coq.Logic.RelationalChoice]
b:2 [in Coq.Numbers.Integer.Abstract.ZBits]
b:2 [in Coq.Strings.Byte]
b:2 [in Coq.Bool.Sumbool]
B:2 [in Coq.Program.Combinators]
b:2 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:2 [in Coq.Numbers.Integer.Abstract.ZPow]
B:2 [in Coq.Logic.PropExtensionalityFacts]
B:2 [in Coq.Program.Basics]
b:2 [in Coq.NArith.Ndiv_def]
b:2 [in Coq.ZArith.Znumtheory]
b:2 [in Coq.Arith.Euclid]
b:2 [in Coq.ZArith.Zeuclid]
b:2 [in Coq.Reals.Cauchy.QExtra]
b:2 [in Coq.Reals.ClassicalConstructiveReals]
B:2 [in Coq.Logic.FinFun]
B:2 [in Coq.Bool.DecBool]
B:20 [in Coq.Logic.Decidable]
b:20 [in Coq.Reals.Runcountable]
b:20 [in Coq.Numbers.NatInt.NZPow]
b:20 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:20 [in Coq.Bool.IfProp]
B:20 [in Coq.Classes.RelationPairs]
B:20 [in Coq.Logic.FunctionalExtensionality]
b:20 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:20 [in Coq.ssr.ssrbool]
b:20 [in Coq.ZArith.Zdiv]
B:20 [in Coq.Program.Equality]
B:20 [in Coq.rtauto.Bintree]
b:20 [in Coq.Wellfounded.Lexicographic_Exponentiation]
b:20 [in Coq.ZArith.Zgcd_alt]
B:20 [in Coq.Logic.ClassicalDescription]
b:20 [in Coq.Numbers.NatInt.NZSqrt]
b:20 [in Coq.Numbers.Integer.Abstract.ZAxioms]
b:20 [in Coq.Numbers.Integer.Abstract.ZPow]
B:20 [in Coq.Init.Logic]
b:20 [in Coq.ZArith.Znumtheory]
B:200 [in Coq.Classes.CMorphisms]
b:200 [in Coq.Logic.ClassicalFacts]
b:200 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:201 [in Coq.ssr.ssrbool]
b:201 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:201 [in Coq.MSets.MSetPositive]
B:201 [in Coq.Logic.ClassicalFacts]
B:202 [in Coq.Logic.ChoiceFacts]
b:202 [in Coq.ZArith.Zdiv]
b:202 [in Coq.Numbers.Integer.Abstract.ZBits]
b:203 [in Coq.Bool.Bool]
b:203 [in Coq.MSets.MSetPositive]
b:203 [in Coq.Reals.RiemannInt_SF]
B:204 [in Coq.Logic.ChoiceFacts]
b:204 [in Coq.ssr.ssrbool]
b:204 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:204 [in Coq.ZArith.Zdiv]
b:205 [in Coq.Bool.Bool]
b:205 [in Coq.Numbers.Integer.Abstract.ZBits]
B:205 [in Coq.Init.Logic]
b:206 [in Coq.Reals.Rfunctions]
b:206 [in Coq.Reals.RiemannInt]
b:206 [in Coq.ssr.ssrbool]
b:206 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:206 [in Coq.Logic.ClassicalFacts]
B:206 [in Coq.Vectors.VectorDef]
b:207 [in Coq.ZArith.Zdiv]
B:207 [in Coq.Classes.CMorphisms]
b:207 [in Coq.MSets.MSetRBT]
b:208 [in Coq.ssr.ssrbool]
b:208 [in Coq.Numbers.Integer.Abstract.ZBits]
b:209 [in Coq.Reals.RiemannInt_SF]
b:21 [in Coq.Numbers.Natural.Abstract.NPow]
B:21 [in Coq.Sets.Ensembles]
b:21 [in Coq.ZArith.Zpow_facts]
b:21 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
b:21 [in Coq.Numbers.Natural.Abstract.NLcm]
B:21 [in Coq.Logic.ChoiceFacts]
b:21 [in Coq.ssr.ssrbool]
b:21 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:21 [in Coq.Numbers.NatInt.NZLog]
b:21 [in Coq.Logic.ClassicalUniqueChoice]
b:21 [in Coq.ZArith.Zquot]
B:21 [in Coq.Program.Combinators]
B:21 [in Coq.Program.Basics]
b:210 [in Coq.Reals.Rfunctions]
b:210 [in Coq.Reals.RiemannInt]
B:210 [in Coq.Logic.ChoiceFacts]
B:210 [in Coq.Logic.Hurkens]
b:211 [in Coq.ssr.ssrbool]
b:211 [in Coq.Numbers.Integer.Abstract.ZBits]
B:211 [in Coq.Logic.ClassicalFacts]
B:212 [in Coq.Logic.ChoiceFacts]
b:212 [in Coq.MSets.MSetRBT]
b:213 [in Coq.Bool.Bool]
B:213 [in Coq.Logic.ClassicalFacts]
b:213 [in Coq.Vectors.VectorDef]
b:214 [in Coq.ssr.ssrbool]
b:214 [in Coq.Numbers.Integer.Abstract.ZBits]
b:215 [in Coq.Numbers.Natural.Abstract.NBits]
B:215 [in Coq.Logic.ClassicalFacts]
B:215 [in Coq.Vectors.VectorDef]
b:216 [in Coq.ssr.ssrbool]
b:216 [in Coq.Numbers.Integer.Abstract.ZBits]
b:217 [in Coq.ZArith.Zdiv]
B:217 [in Coq.Logic.ClassicalFacts]
b:217 [in Coq.Vectors.VectorDef]
b:218 [in Coq.Numbers.Natural.Abstract.NBits]
b:218 [in Coq.ssr.ssrbool]
b:218 [in Coq.Bool.Bool]
b:219 [in Coq.Logic.Hurkens]
b:219 [in Coq.Bool.Bool]
b:219 [in Coq.FSets.FSetPositive]
b:219 [in Coq.Reals.Rtopology]
B:22 [in Coq.Logic.Decidable]
B:22 [in Coq.Sets.Constructive_sets]
b:22 [in Coq.Numbers.NatInt.NZPow]
b:22 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:22 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:22 [in Coq.Numbers.Natural.Abstract.NSqrt]
b:22 [in Coq.ssr.ssrbool]
b:22 [in Coq.ZArith.Zdigits]
b:22 [in Coq.ZArith.Zdiv]
b:22 [in Coq.Sets.Relations_2]
b:22 [in Coq.Numbers.NatInt.NZSqrt]
b:22 [in Coq.Reals.RiemannInt_SF]
b:22 [in Coq.ZArith.Znumtheory]
b:22 [in Coq.QArith.Qpower]
b:22 [in Coq.Reals.Cauchy.QExtra]
b:22 [in Coq.Sets.Powerset]
b:220 [in Coq.ssr.ssrbool]
b:220 [in Coq.Logic.Hurkens]
b:220 [in Coq.ZArith.Zdiv]
b:220 [in Coq.Bool.Bool]
B:220 [in Coq.Init.Logic]
b:220 [in Coq.Vectors.VectorDef]
b:221 [in Coq.Numbers.Natural.Abstract.NBits]
b:221 [in Coq.Bool.Bool]
b:222 [in Coq.ssr.ssrbool]
b:222 [in Coq.ZArith.Zdiv]
b:223 [in Coq.FSets.FSetPositive]
B:224 [in Coq.Logic.ChoiceFacts]
b:224 [in Coq.Numbers.Natural.Abstract.NBits]
b:224 [in Coq.ssr.ssrbool]
b:224 [in Coq.Logic.ClassicalFacts]
b:225 [in Coq.ssr.ssrbool]
b:225 [in Coq.ZArith.Zdiv]
b:225 [in Coq.Bool.Bool]
b:225 [in Coq.FSets.FSetPositive]
b:225 [in Coq.Logic.ClassicalFacts]
b:225 [in Coq.Reals.RiemannInt_SF]
b:226 [in Coq.ssr.ssrbool]
B:226 [in Coq.Vectors.VectorDef]
b:227 [in Coq.Numbers.Natural.Abstract.NBits]
b:227 [in Coq.ssr.ssrbool]
b:227 [in Coq.ZArith.Zdiv]
B:227 [in Coq.Classes.CMorphisms]
b:227 [in Coq.FSets.FSetPositive]
b:227 [in Coq.Reals.Rtopology]
b:228 [in Coq.ssr.ssrbool]
b:229 [in Coq.ssr.ssrbool]
b:229 [in Coq.ZArith.Zdiv]
b:23 [in Coq.Numbers.Natural.Abstract.NPow]
B:23 [in Coq.Sets.Ensembles]
b:23 [in Coq.Numbers.Natural.Abstract.NLcm]
b:23 [in Coq.Numbers.NatInt.NZLog]
b:23 [in Coq.Logic.ClassicalUniqueChoice]
b:23 [in Coq.Sets.Uniset]
b:23 [in Coq.ZArith.Zquot]
b:23 [in Coq.Numbers.NatInt.NZDiv]
b:23 [in Coq.Numbers.Integer.Abstract.ZAxioms]
b:23 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:23 [in Coq.Init.Logic]
b:230 [in Coq.Numbers.Natural.Abstract.NBits]
b:230 [in Coq.Bool.Bool]
b:230 [in Coq.Vectors.VectorDef]
b:231 [in Coq.ssr.ssrbool]
b:231 [in Coq.ZArith.Zdiv]
b:231 [in Coq.Reals.RiemannInt_SF]
b:232 [in Coq.Bool.Bool]
b:233 [in Coq.Numbers.Natural.Abstract.NBits]
b:233 [in Coq.ssr.ssrbool]
B:233 [in Coq.Init.Logic]
B:233 [in Coq.Logic.ClassicalFacts]
b:234 [in Coq.ZArith.BinInt]
B:234 [in Coq.Logic.ChoiceFacts]
b:234 [in Coq.Bool.Bool]
b:234 [in Coq.micromega.ZMicromega]
B:234 [in Coq.Vectors.VectorDef]
b:235 [in Coq.ssr.ssrbool]
B:235 [in Coq.Classes.CMorphisms]
b:235 [in Coq.MSets.MSetRBT]
b:236 [in Coq.Numbers.Natural.Abstract.NBits]
b:236 [in Coq.Init.Logic]
b:237 [in Coq.ZArith.BinInt]
b:237 [in Coq.Reals.RiemannInt]
b:237 [in Coq.ssr.ssrbool]
B:237 [in Coq.Logic.Hurkens]
B:238 [in Coq.FSets.FSetBridge]
b:238 [in Coq.micromega.ZMicromega]
b:239 [in Coq.ssr.ssrbool]
b:239 [in Coq.ZArith.Zdiv]
b:239 [in Coq.Bool.Bool]
b:24 [in Coq.Reals.Runcountable]
b:24 [in Coq.Numbers.Natural.Abstract.NDiv]
b:24 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:24 [in Coq.Numbers.NaryFunctions]
b:24 [in Coq.Reals.RiemannInt]
b:24 [in Coq.Numbers.Natural.Abstract.NSqrt]
b:24 [in Coq.ssr.ssrbool]
B:24 [in Coq.setoid_ring.Algebra_syntax]
b:24 [in Coq.ZArith.Zdigits]
B:24 [in Coq.Program.Equality]
b:24 [in Coq.Reals.NewtonInt]
b:24 [in Coq.Bool.BoolEq]
b:24 [in Coq.Init.Datatypes]
b:24 [in Coq.Numbers.NatInt.NZSqrt]
b:24 [in Coq.ZArith.Znumtheory]
b:24 [in Coq.Reals.Cauchy.QExtra]
b:24 [in Coq.Sets.Powerset]
b:240 [in Coq.ZArith.BinInt]
b:240 [in Coq.Vectors.VectorDef]
b:241 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:241 [in Coq.ssr.ssrbool]
b:241 [in Coq.Bool.Bool]
b:242 [in Coq.Reals.RiemannInt]
b:242 [in Coq.Reals.RiemannInt_SF]
B:242 [in Coq.Vectors.VectorDef]
b:243 [in Coq.ZArith.BinInt]
b:243 [in Coq.ssr.ssrbool]
b:243 [in Coq.Bool.Bool]
b:244 [in Coq.Bool.Bool]
b:244 [in Coq.MSets.MSetRBT]
b:245 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:245 [in Coq.ssr.ssrbool]
b:247 [in Coq.ssr.ssrbool]
b:248 [in Coq.ssr.ssrbool]
b:248 [in Coq.ZArith.Zdiv]
b:249 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
B:25 [in Coq.Logic.Decidable]
b:25 [in Coq.Numbers.NatInt.NZPow]
b:25 [in Coq.Numbers.NaryFunctions]
B:25 [in Coq.Logic.ExtensionalityFacts]
B:25 [in Coq.Logic.FunctionalExtensionality]
b:25 [in Coq.Numbers.Natural.Abstract.NLcm]
b:25 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:25 [in Coq.Numbers.NatInt.NZLog]
b:25 [in Coq.ZArith.Zdiv]
b:25 [in Coq.ZArith.Zquot]
B:25 [in Coq.Sets.Powerset_facts]
B:25 [in Coq.Init.Logic]
b:250 [in Coq.ssr.ssrbool]
B:250 [in Coq.Logic.Hurkens]
b:250 [in Coq.ZArith.Zdiv]
b:250 [in Coq.Reals.RiemannInt_SF]
b:251 [in Coq.ZArith.Zdiv]
b:252 [in Coq.ssr.ssrbool]
b:253 [in Coq.MSets.MSetRBT]
b:253 [in Coq.Numbers.Integer.Abstract.ZBits]
b:254 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:254 [in Coq.ssr.ssrbool]
b:254 [in Coq.Reals.Ranalysis5]
b:256 [in Coq.Numbers.Integer.Abstract.ZBits]
b:256 [in Coq.Reals.RiemannInt_SF]
b:258 [in Coq.Reals.RiemannInt]
b:259 [in Coq.Numbers.Integer.Abstract.ZBits]
b:259 [in Coq.Reals.RiemannInt_SF]
b:26 [in Coq.Sorting.PermutEq]
b:26 [in Coq.Numbers.Natural.Abstract.NDiv]
b:26 [in Coq.Numbers.Natural.Abstract.NPow]
b:26 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:26 [in Coq.ssr.ssrbool]
B:26 [in Coq.Classes.CEquivalence]
b:26 [in Coq.Sorting.Permutation]
b:26 [in Coq.Init.Datatypes]
b:26 [in Coq.Reals.RiemannInt_SF]
b:26 [in Coq.ZArith.Znumtheory]
b:26 [in Coq.Reals.Cauchy.QExtra]
b:26 [in Coq.Sets.Powerset]
B:26 [in Coq.Classes.Equivalence]
B:262 [in Coq.Logic.Hurkens]
B:262 [in Coq.NArith.BinNat]
b:262 [in Coq.Numbers.Integer.Abstract.ZBits]
b:263 [in Coq.MSets.MSetRBT]
B:264 [in Coq.Logic.ChoiceFacts]
B:265 [in Coq.Init.Specif]
b:265 [in Coq.Numbers.Integer.Abstract.ZBits]
b:265 [in Coq.Logic.ClassicalFacts]
b:266 [in Coq.Logic.ClassicalFacts]
b:267 [in Coq.Logic.ChoiceFacts]
b:267 [in Coq.Reals.Ratan]
b:268 [in Coq.Numbers.Integer.Abstract.ZBits]
b:269 [in Coq.Reals.Ratan]
B:27 [in Coq.Logic.Decidable]
b:27 [in Coq.Numbers.Integer.Abstract.ZSgnAbs]
b:27 [in Coq.Numbers.Natural.Abstract.NLcm]
b:27 [in Coq.Reals.RiemannInt]
b:27 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:27 [in Coq.ZArith.Zdiv]
B:27 [in Coq.Program.Equality]
B:27 [in Coq.Sets.Cpo]
b:27 [in Coq.Wellfounded.Lexicographic_Exponentiation]
b:27 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
b:27 [in Coq.ZArith.Zquot]
B:27 [in Coq.Sets.Powerset_facts]
b:27 [in Coq.Numbers.NatInt.NZDiv]
b:27 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:27 [in Coq.Logic.Diaconescu]
B:270 [in Coq.Init.Logic]
b:270 [in Coq.Reals.RiemannInt_SF]
b:271 [in Coq.MSets.MSetRBT]
b:271 [in Coq.Numbers.Integer.Abstract.ZBits]
b:273 [in Coq.Reals.Ratan]
b:274 [in Coq.Numbers.Integer.Abstract.ZBits]
b:275 [in Coq.Reals.Rtopology]
b:276 [in Coq.Reals.Ratan]
b:276 [in Coq.Reals.RiemannInt_SF]
b:279 [in Coq.Numbers.Cyclic.Int63.Int63]
B:279 [in Coq.Init.Logic]
B:28 [in Coq.Sets.Constructive_sets]
b:28 [in Coq.Numbers.NatInt.NZPow]
b:28 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:28 [in Coq.Numbers.NaryFunctions]
b:28 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:28 [in Coq.ssr.ssrbool]
B:28 [in Coq.setoid_ring.Algebra_syntax]
b:28 [in Coq.Reals.NewtonInt]
b:28 [in Coq.Init.Datatypes]
b:28 [in Coq.Reals.Ratan]
b:28 [in Coq.Numbers.Integer.Abstract.ZAxioms]
b:28 [in Coq.Logic.Diaconescu]
B:28 [in Coq.Init.Logic]
b:28 [in Coq.Sets.Powerset]
B:280 [in Coq.FSets.FMapPositive]
b:282 [in Coq.Reals.RiemannInt_SF]
b:282 [in Coq.Lists.SetoidList]
b:284 [in Coq.QArith.QArith_base]
b:285 [in Coq.Numbers.Natural.Abstract.NBits]
B:286 [in Coq.Vectors.VectorDef]
b:287 [in Coq.QArith.QArith_base]
b:288 [in Coq.Numbers.Natural.Abstract.NBits]
b:288 [in Coq.Reals.RiemannInt_SF]
b:289 [in Coq.Numbers.Integer.Abstract.ZBits]
B:29 [in Coq.Logic.Decidable]
b:29 [in Coq.Numbers.Integer.Abstract.ZSgnAbs]
b:29 [in Coq.Numbers.Natural.Abstract.NPow]
b:29 [in Coq.Reals.MVT]
b:29 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:29 [in Coq.Numbers.NatInt.NZLog]
b:29 [in Coq.ZArith.Zdiv]
b:29 [in Coq.ZArith.Zquot]
b:29 [in Coq.Numbers.NatInt.NZSqrt]
b:29 [in Coq.Logic.Diaconescu]
b:29 [in Coq.Sorting.Heap]
B:29 [in Coq.Logic.FinFun]
b:291 [in Coq.Numbers.Natural.Abstract.NBits]
b:292 [in Coq.FSets.FMapWeakList]
b:292 [in Coq.Numbers.Integer.Abstract.ZBits]
b:292 [in Coq.QArith.QArith_base]
b:293 [in Coq.Reals.RiemannInt_SF]
b:294 [in Coq.Numbers.Natural.Abstract.NBits]
b:294 [in Coq.Numbers.Integer.Abstract.ZBits]
b:294 [in Coq.QArith.QArith_base]
b:296 [in Coq.Numbers.Integer.Abstract.ZBits]
b:297 [in Coq.Numbers.Natural.Abstract.NBits]
B:297 [in Coq.Vectors.VectorDef]
b:298 [in Coq.Numbers.Integer.Abstract.ZBits]
b:298 [in Coq.QArith.QArith_base]
b:299 [in Coq.Reals.RiemannInt_SF]
b:3 [in Coq.Init.Byte]
B:3 [in Coq.Numbers.NaryFunctions]
b:3 [in Coq.FSets.FMapFacts]
B:3 [in Coq.Logic.JMeq]
b:3 [in Coq.Numbers.Natural.Abstract.NDefOps]
b:3 [in Coq.Reals.RiemannInt]
b:3 [in Coq.Numbers.Natural.Abstract.NSqrt]
B:3 [in Coq.Sets.Cpo]
b:3 [in Coq.Reals.NewtonInt]
B:3 [in Coq.Classes.CRelationClasses]
b:3 [in Coq.Numbers.Natural.Abstract.NAxioms]
B:3 [in Coq.Sets.Powerset_Classical_facts]
b:3 [in Coq.Logic.Diaconescu]
B:3 [in Coq.Logic.ClassicalFacts]
B:3 [in Coq.Logic.PropFacts]
b:3 [in Coq.Classes.Init]
b:30 [in Coq.Reals.Runcountable]
b:30 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:30 [in Coq.Logic.ExtensionalityFacts]
b:30 [in Coq.Numbers.Natural.Abstract.NLcm]
B:30 [in Coq.Logic.ChoiceFacts]
b:30 [in Coq.ssr.ssrbool]
b:30 [in Coq.Numbers.Cyclic.Int31.Int31]
b:30 [in Coq.Init.Datatypes]
B:30 [in Coq.Sets.Powerset_facts]
b:30 [in Coq.Logic.Diaconescu]
b:30 [in Coq.ZArith.Znumtheory]
b:300 [in Coq.Numbers.Natural.Abstract.NBits]
b:300 [in Coq.Numbers.Integer.Abstract.ZBits]
B:300 [in Coq.Init.Logic]
b:301 [in Coq.Reals.RiemannInt]
b:302 [in Coq.Numbers.Integer.Abstract.ZBits]
b:303 [in Coq.Numbers.Natural.Abstract.NBits]
b:303 [in Coq.QArith.QArith_base]
b:305 [in Coq.Reals.RiemannInt_SF]
b:305 [in Coq.QArith.QArith_base]
b:306 [in Coq.Numbers.Natural.Abstract.NBits]
b:306 [in Coq.Numbers.Integer.Abstract.ZBits]
B:306 [in Coq.Lists.SetoidList]
b:308 [in Coq.Reals.RiemannInt]
b:308 [in Coq.QArith.QArith_base]
B:31 [in Coq.Logic.Decidable]
b:31 [in Coq.Numbers.Natural.Abstract.NPow]
b:31 [in Coq.Numbers.NatInt.NZPow]
b:31 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:31 [in Coq.Numbers.NatInt.NZLog]
b:31 [in Coq.ZArith.Zdiv]
b:31 [in Coq.Bool.Bool]
B:31 [in Coq.Classes.CMorphisms]
b:31 [in Coq.Wellfounded.Lexicographic_Exponentiation]
b:31 [in Coq.ZArith.Zquot]
B:31 [in Coq.Logic.Berardi]
b:31 [in Coq.Reals.Ratan]
b:31 [in Coq.Numbers.NatInt.NZSqrt]
b:31 [in Coq.Numbers.NatInt.NZDiv]
b:31 [in Coq.Numbers.Integer.Abstract.ZAxioms]
b:31 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:31 [in Coq.Logic.Diaconescu]
B:31 [in Coq.Init.Logic]
b:31 [in Coq.Sets.Powerset]
b:311 [in Coq.Reals.RiemannInt]
b:312 [in Coq.Reals.RiemannInt_SF]
b:315 [in Coq.Numbers.Natural.Abstract.NBits]
b:316 [in Coq.Reals.RiemannInt_SF]
b:317 [in Coq.Numbers.Cyclic.Int63.Int63]
b:317 [in Coq.Numbers.Natural.Abstract.NBits]
b:319 [in Coq.Numbers.Natural.Abstract.NBits]
b:32 [in Coq.Reals.Abstract.ConstructiveReals]
b:32 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:32 [in Coq.Numbers.NaryFunctions]
B:32 [in Coq.Logic.FunctionalExtensionality]
b:32 [in Coq.ssr.ssrbool]
b:32 [in Coq.ZArith.Zdiv]
B:32 [in Coq.Lists.ListSet]
b:32 [in Coq.Logic.Diaconescu]
b:32 [in Coq.Reals.RiemannInt_SF]
b:32 [in Coq.Numbers.Natural.Abstract.NGcd]
b:32 [in Coq.ZArith.Znumtheory]
b:321 [in Coq.Numbers.Natural.Abstract.NBits]
b:322 [in Coq.Reals.RIneq]
b:323 [in Coq.Numbers.Natural.Abstract.NBits]
b:324 [in Coq.Reals.RiemannInt_SF]
b:325 [in Coq.Numbers.Natural.Abstract.NBits]
B:326 [in Coq.FSets.FMapPositive]
b:327 [in Coq.Numbers.Natural.Abstract.NBits]
b:329 [in Coq.Numbers.Natural.Abstract.NBits]
B:33 [in Coq.Logic.Decidable]
b:33 [in Coq.Numbers.NatInt.NZPow]
b:33 [in Coq.Numbers.NaryFunctions]
b:33 [in Coq.Numbers.Natural.Abstract.NLcm]
b:33 [in Coq.Numbers.NatInt.NZLog]
b:33 [in Coq.Bool.Bool]
b:33 [in Coq.ZArith.Zgcd_alt]
b:33 [in Coq.ZArith.Zquot]
B:33 [in Coq.Sets.Powerset_facts]
B:33 [in Coq.Logic.FinFun]
b:331 [in Coq.Numbers.Natural.Abstract.NBits]
b:331 [in Coq.Reals.RiemannInt_SF]
b:332 [in Coq.Reals.RiemannInt]
b:333 [in Coq.Numbers.Natural.Abstract.NBits]
B:333 [in Coq.FSets.FMapPositive]
b:335 [in Coq.Reals.Abstract.ConstructiveReals]
b:335 [in Coq.Logic.ChoiceFacts]
b:335 [in Coq.Numbers.Natural.Abstract.NBits]
b:336 [in Coq.Logic.ChoiceFacts]
b:337 [in Coq.Numbers.Cyclic.Int63.Int63]
b:337 [in Coq.Logic.ChoiceFacts]
b:338 [in Coq.Logic.ChoiceFacts]
B:338 [in Coq.Init.Logic]
b:338 [in Coq.Reals.RiemannInt_SF]
b:34 [in Coq.Numbers.Natural.Abstract.NDiv]
b:34 [in Coq.Numbers.Natural.Abstract.NPow]
b:34 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:34 [in Coq.Numbers.Integer.Abstract.ZLcm]
B:34 [in Coq.Classes.CEquivalence]
b:34 [in Coq.Reals.NewtonInt]
b:34 [in Coq.Numbers.Integer.Abstract.ZAxioms]
B:34 [in Coq.Init.Logic]
b:34 [in Coq.btauto.Reflect]
b:34 [in Coq.Sets.Powerset]
B:34 [in Coq.Classes.Equivalence]
b:341 [in Coq.Reals.RiemannInt]
b:341 [in Coq.Numbers.Natural.Abstract.NBits]
B:342 [in Coq.Init.Logic]
b:342 [in Coq.micromega.ZMicromega]
B:343 [in Coq.FSets.FMapFacts]
b:343 [in Coq.Reals.RiemannInt_SF]
b:344 [in Coq.Numbers.Natural.Abstract.NBits]
b:346 [in Coq.Numbers.Integer.Abstract.ZBits]
b:348 [in Coq.Numbers.Natural.Abstract.NBits]
b:348 [in Coq.Numbers.Integer.Abstract.ZBits]
B:35 [in Coq.Logic.Decidable]
B:35 [in Coq.setoid_ring.Ncring_initial]
B:35 [in Coq.Sets.Constructive_sets]
b:35 [in Coq.Numbers.NatInt.NZPow]
B:35 [in Coq.Classes.Morphisms]
b:35 [in Coq.Bool.Bool]
B:35 [in Coq.Program.Equality]
b:35 [in Coq.Numbers.NatInt.NZBits]
b:35 [in Coq.Sets.Relations_2_facts]
b:35 [in Coq.ZArith.Zquot]
B:35 [in Coq.Logic.ClassicalDescription]
b:35 [in Coq.Numbers.NatInt.NZSqrt]
b:35 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:35 [in Coq.ZArith.Znumtheory]
b:350 [in Coq.Numbers.Natural.Abstract.NBits]
B:350 [in Coq.Init.Logic]
b:351 [in Coq.Reals.RiemannInt_SF]
b:352 [in Coq.MSets.MSetRBT]
b:352 [in Coq.Numbers.Integer.Abstract.ZBits]
b:353 [in Coq.FSets.FMapFacts]
b:353 [in Coq.Numbers.Natural.Abstract.NBits]
b:354 [in Coq.Numbers.Integer.Abstract.ZBits]
b:355 [in Coq.Lists.List]
b:355 [in Coq.Numbers.Natural.Abstract.NBits]
b:356 [in Coq.Numbers.Integer.Abstract.ZBits]
b:356 [in Coq.Reals.Ratan]
b:357 [in Coq.FSets.FMapFacts]
b:358 [in Coq.Numbers.Natural.Abstract.NBits]
b:358 [in Coq.Numbers.Integer.Abstract.ZBits]
b:358 [in Coq.Reals.RiemannInt_SF]
b:359 [in Coq.Reals.Ratan]
b:36 [in Coq.Numbers.Natural.Abstract.NDiv]
b:36 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:36 [in Coq.Logic.ExtensionalityFacts]
b:36 [in Coq.Numbers.NatInt.NZLog]
b:36 [in Coq.ZArith.Zgcd_alt]
B:36 [in Coq.Sets.Powerset_facts]
b:36 [in Coq.Numbers.NatInt.NZDiv]
b:36 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:360 [in Coq.Numbers.Integer.Abstract.ZBits]
b:361 [in Coq.FSets.FMapFacts]
b:361 [in Coq.Numbers.Natural.Abstract.NBits]
b:362 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:362 [in Coq.MSets.MSetRBT]
b:362 [in Coq.Numbers.Integer.Abstract.ZBits]
b:363 [in Coq.Numbers.Natural.Abstract.NBits]
b:363 [in Coq.Reals.RiemannInt_SF]
b:364 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:364 [in Coq.Numbers.Integer.Abstract.ZBits]
b:366 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:366 [in Coq.Numbers.Integer.Abstract.ZBits]
b:366 [in Coq.micromega.Tauto]
b:368 [in Coq.Numbers.Integer.Abstract.ZBits]
b:369 [in Coq.Numbers.Natural.Abstract.NBits]
B:37 [in Coq.Logic.Decidable]
b:37 [in Coq.Reals.Runcountable]
b:37 [in Coq.Numbers.Natural.Abstract.NPow]
b:37 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:37 [in Coq.Reals.RiemannInt]
b:37 [in Coq.ssr.ssrbool]
b:37 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:37 [in Coq.Bool.Bool]
B:37 [in Coq.Classes.SetoidDec]
b:37 [in Coq.ZArith.Zquot]
b:37 [in Coq.Numbers.NatInt.NZSqrt]
b:37 [in Coq.Numbers.Integer.Abstract.ZAxioms]
b:37 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:37 [in Coq.Init.Logic]
b:37 [in Coq.ZArith.Znumtheory]
b:371 [in Coq.Reals.RiemannInt_SF]
b:372 [in Coq.Numbers.Natural.Abstract.NBits]
B:376 [in Coq.FSets.FMapWeakList]
B:376 [in Coq.Init.Logic]
b:378 [in Coq.Reals.RiemannInt_SF]
b:379 [in Coq.Numbers.Integer.Abstract.ZBits]
b:38 [in Coq.Numbers.Natural.Abstract.NDiv]
b:38 [in Coq.Numbers.NatInt.NZPow]
b:38 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:38 [in Coq.Logic.ClassicalEpsilon]
B:38 [in Coq.Numbers.NaryFunctions]
B:38 [in Coq.Classes.CEquivalence]
b:38 [in Coq.ZArith.Zdiv]
b:38 [in Coq.Reals.Abstract.ConstructiveLimits]
b:38 [in Coq.Numbers.Cyclic.Int31.Int31]
B:38 [in Coq.Lists.ListSet]
b:38 [in Coq.Numbers.NatInt.NZDiv]
b:38 [in Coq.Reals.R_sqr]
B:38 [in Coq.Logic.FinFun]
B:38 [in Coq.rtauto.Rtauto]
B:38 [in Coq.Classes.Equivalence]
b:380 [in Coq.Reals.RiemannInt]
b:381 [in Coq.Numbers.Integer.Abstract.ZBits]
b:382 [in Coq.micromega.Tauto]
b:383 [in Coq.Numbers.Integer.Abstract.ZBits]
b:385 [in Coq.Numbers.Integer.Abstract.ZBits]
B:386 [in Coq.Lists.List]
b:387 [in Coq.Numbers.Integer.Abstract.ZBits]
b:387 [in Coq.micromega.Tauto]
b:389 [in Coq.Numbers.Integer.Abstract.ZBits]
B:39 [in Coq.Logic.Decidable]
B:39 [in Coq.Sets.Ensembles]
B:39 [in Coq.Logic.FunctionalExtensionality]
b:39 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:39 [in Coq.Numbers.NatInt.NZBits]
b:39 [in Coq.ZArith.Zgcd_alt]
B:39 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
b:39 [in Coq.Numbers.NatInt.NZSqrt]
b:39 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:39 [in Coq.Reals.RiemannInt_SF]
B:390 [in Coq.Lists.List]
B:391 [in Coq.Logic.ChoiceFacts]
b:391 [in Coq.Numbers.Integer.Abstract.ZBits]
B:393 [in Coq.Logic.ChoiceFacts]
b:393 [in Coq.Numbers.Integer.Abstract.ZBits]
b:394 [in Coq.micromega.Tauto]
B:395 [in Coq.Logic.ChoiceFacts]
b:395 [in Coq.Numbers.Integer.Abstract.ZBits]
b:396 [in Coq.micromega.Tauto]
B:397 [in Coq.Logic.ChoiceFacts]
b:397 [in Coq.Numbers.Integer.Abstract.ZBits]
b:399 [in Coq.Numbers.Integer.Abstract.ZBits]
B:4 [in Coq.Logic.Decidable]
b:4 [in Coq.Numbers.Natural.Abstract.NDiv]
B:4 [in Coq.Sets.Ensembles]
b:4 [in Coq.Reals.MVT]
b:4 [in Coq.Arith.Wf_nat]
b:4 [in Coq.Numbers.Natural.Abstract.NLcm]
b:4 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:4 [in Coq.ssr.ssrbool]
b:4 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:4 [in Coq.ZArith.Zgcd_alt]
B:4 [in Coq.Logic.Berardi]
b:4 [in Coq.Bool.Sumbool]
b:4 [in Coq.Numbers.NatInt.NZDiv]
b:4 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:4 [in Coq.Numbers.Integer.Abstract.ZPow]
b:4 [in Coq.NArith.Ndiv_def]
b:4 [in Coq.ZArith.Zeuclid]
b:40 [in Coq.Numbers.Natural.Abstract.NDiv]
b:40 [in Coq.Numbers.NaryFunctions]
b:40 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:40 [in Coq.ssr.ssrbool]
b:40 [in Coq.Numbers.NatInt.NZLog]
b:40 [in Coq.ZArith.Zquot]
B:40 [in Coq.Init.Logic]
b:40 [in Coq.Reals.R_sqr]
b:40 [in Coq.Reals.Cauchy.QExtra]
B:403 [in Coq.Lists.List]
b:405 [in Coq.Numbers.Integer.Abstract.ZBits]
b:408 [in Coq.FSets.FMapFacts]
b:409 [in Coq.Numbers.Integer.Abstract.ZBits]
B:41 [in Coq.Logic.Decidable]
b:41 [in Coq.Numbers.Natural.Abstract.NPow]
b:41 [in Coq.Numbers.NatInt.NZPow]
B:41 [in Coq.Classes.RelationPairs]
b:41 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:41 [in Coq.Program.Equality]
B:41 [in Coq.Init.Datatypes]
b:41 [in Coq.Numbers.NatInt.NZSqrt]
b:41 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:410 [in Coq.Lists.List]
b:410 [in Coq.FSets.FMapFacts]
b:410 [in Coq.Numbers.Cyclic.Int63.Int63]
B:411 [in Coq.Logic.ChoiceFacts]
B:413 [in Coq.Logic.ChoiceFacts]
b:413 [in Coq.Numbers.Integer.Abstract.ZBits]
B:415 [in Coq.Logic.ChoiceFacts]
B:416 [in Coq.Lists.List]
B:416 [in Coq.Init.Logic]
B:417 [in Coq.Logic.ChoiceFacts]
b:417 [in Coq.Numbers.Integer.Abstract.ZBits]
b:419 [in Coq.Reals.RiemannInt]
b:419 [in Coq.Numbers.Integer.Abstract.ZBits]
b:42 [in Coq.Numbers.Natural.Abstract.NDiv]
B:42 [in Coq.Sets.Ensembles]
b:42 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:42 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:42 [in Coq.ssr.ssrbool]
b:42 [in Coq.Numbers.NatInt.NZLog]
B:42 [in Coq.Classes.CEquivalence]
B:42 [in Coq.Classes.EquivDec]
b:42 [in Coq.ZArith.Zgcd_alt]
b:42 [in Coq.ZArith.Znumtheory]
b:42 [in Coq.Reals.Cauchy.QExtra]
b:42 [in Coq.NArith.Ndec]
B:42 [in Coq.Logic.FinFun]
B:42 [in Coq.rtauto.Rtauto]
B:42 [in Coq.Classes.Equivalence]
b:421 [in Coq.Logic.ChoiceFacts]
B:422 [in Coq.Lists.List]
b:422 [in Coq.Numbers.Integer.Abstract.ZBits]
B:422 [in Coq.Init.Logic]
b:422 [in Coq.micromega.Tauto]
b:423 [in Coq.Logic.ChoiceFacts]
b:424 [in Coq.Numbers.Integer.Abstract.ZBits]
b:425 [in Coq.Reals.RiemannInt]
b:427 [in Coq.Numbers.Integer.Abstract.ZBits]
B:428 [in Coq.Lists.List]
B:43 [in Coq.Logic.Decidable]
b:43 [in Coq.Numbers.NatInt.NZPow]
b:43 [in Coq.Numbers.Integer.Abstract.ZGcd]
b:43 [in Coq.Reals.MVT]
b:43 [in Coq.ZArith.Zdiv]
b:43 [in Coq.Numbers.NatInt.NZBits]
b:43 [in Coq.ZArith.Zquot]
b:43 [in Coq.Numbers.NatInt.NZSqrt]
b:43 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:43 [in Coq.Init.Logic]
b:430 [in Coq.Reals.RiemannInt]
b:430 [in Coq.Numbers.Integer.Abstract.ZBits]
b:432 [in Coq.Numbers.Integer.Abstract.ZBits]
B:434 [in Coq.Lists.List]
b:434 [in Coq.Numbers.Integer.Abstract.ZBits]
b:437 [in Coq.Reals.Ranalysis1]
b:437 [in Coq.Reals.RiemannInt]
b:437 [in Coq.Numbers.Integer.Abstract.ZBits]
b:44 [in Coq.Numbers.Natural.Abstract.NDiv]
B:44 [in Coq.Sets.Ensembles]
b:44 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:44 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:44 [in Coq.ssr.ssrbool]
B:44 [in Coq.MSets.MSetList]
b:44 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:44 [in Coq.ZArith.Zdigits]
B:44 [in Coq.Classes.CMorphisms]
b:44 [in Coq.Reals.Ratan]
b:44 [in Coq.Reals.RiemannInt_SF]
b:44 [in Coq.NArith.Ndec]
b:443 [in Coq.Reals.Ranalysis1]
b:444 [in Coq.Numbers.Cyclic.Int63.Int63]
b:444 [in Coq.Reals.RiemannInt]
B:444 [in Coq.FSets.FMapList]
b:45 [in Coq.Numbers.Natural.Abstract.NPow]
b:45 [in Coq.Numbers.NatInt.NZLog]
B:45 [in Coq.Sets.Powerset_facts]
b:45 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:45 [in Coq.ZArith.Znumtheory]
b:451 [in Coq.Reals.Ranalysis1]
b:452 [in Coq.Reals.RiemannInt]
b:456 [in Coq.Reals.RiemannInt]
b:459 [in Coq.FSets.FMapFacts]
b:46 [in Coq.Reals.Runcountable]
b:46 [in Coq.Numbers.Natural.Abstract.NDiv]
b:46 [in Coq.Numbers.NatInt.NZPow]
B:46 [in Coq.Logic.FunctionalExtensionality]
b:46 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:46 [in Coq.ssr.ssrbool]
b:46 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:46 [in Coq.Classes.CEquivalence]
b:46 [in Coq.Bool.Bool]
b:46 [in Coq.ZArith.Zquot]
B:46 [in Coq.Init.Datatypes]
b:46 [in Coq.Numbers.NatInt.NZDiv]
B:46 [in Coq.Init.Logic]
b:46 [in Coq.Numbers.Natural.Abstract.NGcd]
b:46 [in Coq.NArith.Ndec]
B:46 [in Coq.Structures.OrdersFacts]
B:46 [in Coq.Classes.Equivalence]
b:460 [in Coq.Reals.RiemannInt]
b:462 [in Coq.Reals.RIneq]
b:464 [in Coq.FSets.FMapFacts]
b:464 [in Coq.Reals.RiemannInt]
b:47 [in Coq.Numbers.NatInt.NZLog]
b:47 [in Coq.Bool.Bool]
b:47 [in Coq.Numbers.NatInt.NZBits]
b:47 [in Coq.ZArith.Zgcd_alt]
b:47 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
b:47 [in Coq.Reals.Ratan]
b:47 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:47 [in Coq.Reals.RiemannInt_SF]
B:47 [in Coq.Logic.FinFun]
b:47 [in Coq.Structures.OrdersFacts]
B:47 [in Coq.rtauto.Rtauto]
B:471 [in Coq.Lists.List]
b:472 [in Coq.Reals.RIneq]
B:477 [in Coq.Lists.List]
b:48 [in Coq.Numbers.Natural.Abstract.NDiv]
b:48 [in Coq.Numbers.Natural.Abstract.NPow]
b:48 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:48 [in Coq.ssr.ssrbool]
b:48 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:48 [in Coq.Logic.Hurkens]
b:48 [in Coq.Bool.Bool]
B:48 [in Coq.Program.Equality]
b:48 [in Coq.Vectors.Fin]
b:48 [in Coq.Sorting.CPermutation]
B:48 [in Coq.Sets.Powerset_facts]
b:48 [in Coq.Numbers.NatInt.NZDiv]
b:48 [in Coq.ZArith.Znumtheory]
b:48 [in Coq.Reals.Abstract.ConstructiveMinMax]
b:49 [in Coq.Numbers.NatInt.NZPow]
B:49 [in Coq.Sets.Ensembles]
B:49 [in Coq.Logic.JMeq]
b:49 [in Coq.ZArith.Zeven]
b:49 [in Coq.ZArith.Zdiv]
B:49 [in Coq.Classes.CMorphisms]
b:49 [in Coq.Strings.Ascii]
b:49 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
b:49 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:49 [in Coq.Init.Logic]
b:49 [in Coq.NArith.Ndec]
B:492 [in Coq.Lists.List]
b:493 [in Coq.FSets.FMapFacts]
b:496 [in Coq.FSets.FMapFacts]
b:499 [in Coq.Reals.RiemannInt]
b:5 [in Coq.Init.Byte]
b:5 [in Coq.Bool.BoolOrder]
b:5 [in Coq.Numbers.Natural.Abstract.NDiv]
b:5 [in Coq.Numbers.NatInt.NZPow]
b:5 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:5 [in Coq.Numbers.Natural.Abstract.NBits]
b:5 [in Coq.ssr.ssrbool]
b:5 [in Coq.Bool.Bool]
B:5 [in Coq.Classes.CRelationClasses]
b:5 [in Coq.Numbers.Integer.Abstract.ZBits]
B:5 [in Coq.Program.Combinators]
b:5 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:5 [in Coq.Reals.Cauchy.QExtra]
b:50 [in Coq.Numbers.Natural.Abstract.NDiv]
B:50 [in Coq.Numbers.NaryFunctions]
b:50 [in Coq.Lists.List]
b:50 [in Coq.Numbers.Integer.Abstract.ZLcm]
B:50 [in Coq.Logic.ChoiceFacts]
b:50 [in Coq.ssr.ssrbool]
b:50 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:50 [in Coq.Bool.Bool]
b:50 [in Coq.ZArith.Zgcd_alt]
b:50 [in Coq.ZArith.Zquot]
b:50 [in Coq.Logic.Berardi]
B:50 [in Coq.Init.Datatypes]
b:50 [in Coq.Numbers.NatInt.NZSqrt]
b:50 [in Coq.Numbers.NatInt.NZDiv]
b:501 [in Coq.FSets.FMapFacts]
b:504 [in Coq.FSets.FMapFacts]
B:505 [in Coq.Init.Specif]
b:506 [in Coq.Reals.RiemannInt]
b:51 [in Coq.Numbers.Natural.Abstract.NPow]
b:51 [in Coq.ZArith.Zeven]
b:51 [in Coq.Bool.Bool]
b:51 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
b:51 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:51 [in Coq.Vectors.VectorDef]
b:51 [in Coq.NArith.Ndec]
b:513 [in Coq.Reals.RiemannInt]
b:52 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:52 [in Coq.Reals.R_sqrt]
b:52 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:52 [in Coq.ssr.ssrbool]
b:52 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:52 [in Coq.Bool.Bool]
B:52 [in Coq.Classes.EquivDec]
b:52 [in Coq.Reals.NewtonInt]
b:52 [in Coq.Sorting.CPermutation]
b:52 [in Coq.Numbers.NatInt.NZDiv]
B:52 [in Coq.Init.Logic]
b:52 [in Coq.Reals.RiemannInt_SF]
b:52 [in Coq.Sorting.Heap]
b:528 [in Coq.Reals.RiemannInt]
b:53 [in Coq.Reals.Ranalysis2]
b:53 [in Coq.Numbers.Natural.Abstract.NDiv]
b:53 [in Coq.Numbers.NatInt.NZPow]
B:53 [in Coq.Sets.Ensembles]
B:53 [in Coq.Logic.JMeq]
B:53 [in Coq.Logic.FunctionalExtensionality]
b:53 [in Coq.ZArith.Zeven]
b:53 [in Coq.ZArith.Zdiv]
b:53 [in Coq.ZArith.Zgcd_alt]
b:53 [in Coq.Numbers.Cyclic.Int63.Cyclic63]
b:53 [in Coq.Lists.ListSet]
b:53 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:534 [in Coq.Reals.RiemannInt]
b:54 [in Coq.Reals.Runcountable]
b:54 [in Coq.Numbers.Natural.Abstract.NPow]
b:54 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:54 [in Coq.Lists.List]
b:54 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:54 [in Coq.ssr.ssrbool]
b:54 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:54 [in Coq.Logic.Hurkens]
b:54 [in Coq.Bool.Bool]
b:54 [in Coq.micromega.QMicromega]
b:54 [in Coq.ZArith.Zquot]
B:54 [in Coq.Init.Datatypes]
b:54 [in Coq.Numbers.NatInt.NZDiv]
B:54 [in Coq.Init.Logic]
b:54 [in Coq.ZArith.Znumtheory]
b:54 [in Coq.NArith.Ndec]
b:543 [in Coq.Reals.RiemannInt]
b:546 [in Coq.Reals.RiemannInt]
b:549 [in Coq.Reals.RiemannInt]
b:55 [in Coq.Numbers.Natural.Abstract.NDiv]
B:55 [in Coq.Sets.Ensembles]
b:55 [in Coq.Reals.RiemannInt]
b:55 [in Coq.Numbers.NatInt.NZLog]
b:55 [in Coq.ZArith.Zeven]
b:55 [in Coq.ZArith.Zgcd_alt]
b:55 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:55 [in Coq.Reals.RiemannInt_SF]
b:555 [in Coq.Reals.RiemannInt]
b:557 [in Coq.micromega.Tauto]
b:559 [in Coq.Reals.RiemannInt]
b:56 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:56 [in Coq.Reals.R_sqrt]
B:56 [in Coq.Logic.FunctionalExtensionality]
b:56 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:56 [in Coq.Numbers.Cyclic.Int63.Int63]
b:56 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:56 [in Coq.Lists.ListSet]
b:56 [in Coq.Numbers.NatInt.NZDiv]
b:562 [in Coq.micromega.Tauto]
b:57 [in Coq.Reals.Ranalysis2]
b:57 [in Coq.Numbers.Natural.Abstract.NDiv]
b:57 [in Coq.Numbers.Natural.Abstract.NPow]
b:57 [in Coq.Numbers.NatInt.NZPow]
b:57 [in Coq.ZArith.Zeven]
b:57 [in Coq.ZArith.Zdiv]
b:57 [in Coq.Bool.Bool]
B:57 [in Coq.Classes.CMorphisms]
b:57 [in Coq.Numbers.NatInt.NZSqrt]
b:57 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:57 [in Coq.NArith.BinNatDef]
B:57 [in Coq.Init.Logic]
b:57 [in Coq.Reals.Cauchy.QExtra]
b:57 [in Coq.NArith.Ndec]
b:571 [in Coq.Reals.RiemannInt]
b:578 [in Coq.Reals.RiemannInt]
B:58 [in Coq.Sets.Ensembles]
b:58 [in Coq.Lists.List]
B:58 [in Coq.Logic.JMeq]
b:58 [in Coq.Numbers.Cyclic.Int63.Int63]
b:58 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:58 [in Coq.Bool.Bool]
b:58 [in Coq.Sorting.CPermutation]
b:58 [in Coq.ZArith.Zquot]
B:58 [in Coq.Sets.Powerset_facts]
b:58 [in Coq.Numbers.NatInt.NZDiv]
B:58 [in Coq.Logic.FinFun]
b:580 [in Coq.PArith.BinPos]
b:582 [in Coq.PArith.BinPos]
b:585 [in Coq.PArith.BinPos]
b:587 [in Coq.PArith.BinPos]
b:589 [in Coq.PArith.BinPos]
b:59 [in Coq.Numbers.Natural.Abstract.NDiv]
b:59 [in Coq.Reals.Rfunctions]
b:59 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:59 [in Coq.Numbers.NaryFunctions]
b:59 [in Coq.Reals.R_sqrt]
b:59 [in Coq.Numbers.Integer.Abstract.ZLcm]
B:59 [in Coq.ssr.ssrbool]
b:59 [in Coq.MSets.MSetAVL]
b:59 [in Coq.ZArith.Zeven]
b:59 [in Coq.Reals.Raxioms]
b:59 [in Coq.Lists.ListSet]
b:59 [in Coq.Numbers.NatInt.NZSqrt]
b:59 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:59 [in Coq.Logic.ClassicalFacts]
b:59 [in Coq.Vectors.VectorDef]
b:591 [in Coq.PArith.BinPos]
b:594 [in Coq.PArith.BinPos]
b:597 [in Coq.PArith.BinPos]
B:6 [in Coq.Logic.Decidable]
b:6 [in Coq.Bool.BoolOrder]
b:6 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:6 [in Coq.Bool.IfProp]
b:6 [in Coq.Arith.Wf_nat]
b:6 [in Coq.Logic.ExtensionalityFacts]
b:6 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:6 [in Coq.Numbers.Cyclic.Int63.Int63]
b:6 [in Coq.Numbers.Natural.Abstract.NSqrt]
B:6 [in Coq.Program.Subset]
b:6 [in Coq.ssr.ssrbool]
b:6 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:6 [in Coq.Reals.Machin]
b:6 [in Coq.ZArith.Zdiv]
b:6 [in Coq.Bool.Bool]
b:6 [in Coq.Numbers.Cyclic.Int31.Int31]
b:6 [in Coq.Numbers.NatInt.NZSqrt]
B:6 [in Coq.Logic.Diaconescu]
b:6 [in Coq.Numbers.Integer.Abstract.ZPow]
b:6 [in Coq.ZArith.Znumtheory]
B:6 [in Coq.Logic.PropFacts]
b:6 [in Coq.ZArith.Zeuclid]
b:60 [in Coq.Reals.Runcountable]
b:60 [in Coq.Numbers.Natural.Abstract.NPow]
b:60 [in Coq.Numbers.NatInt.NZPow]
b:60 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:60 [in Coq.ZArith.Zquot]
B:60 [in Coq.Init.Datatypes]
b:60 [in Coq.Numbers.NatInt.NZDiv]
B:60 [in Coq.micromega.RMicromega]
B:60 [in Coq.Init.Logic]
b:60 [in Coq.Logic.ClassicalFacts]
b:60 [in Coq.ZArith.Znumtheory]
b:60 [in Coq.NArith.Ndec]
b:600 [in Coq.PArith.BinPos]
b:601 [in Coq.Reals.RIneq]
b:603 [in Coq.Reals.RIneq]
b:606 [in Coq.Reals.RIneq]
b:61 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:61 [in Coq.Reals.MVT]
b:61 [in Coq.setoid_ring.Field_theory]
b:61 [in Coq.ZArith.Zeven]
b:61 [in Coq.ZArith.Zdiv]
b:61 [in Coq.Reals.NewtonInt]
b:61 [in Coq.Numbers.NatInt.NZSqrt]
b:61 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:61 [in Coq.Logic.ClassicalFacts]
b:61 [in Coq.Reals.Cauchy.QExtra]
b:62 [in Coq.Numbers.Natural.Abstract.NDiv]
b:62 [in Coq.Reals.R_sqrt]
b:62 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:62 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:62 [in Coq.Numbers.NatInt.NZLog]
b:62 [in Coq.MSets.MSetAVL]
b:62 [in Coq.Arith.PeanoNat]
b:62 [in Coq.ZArith.Zquot]
b:62 [in Coq.Lists.ListSet]
b:62 [in Coq.Numbers.NatInt.NZDiv]
b:62 [in Coq.Logic.ClassicalFacts]
b:63 [in Coq.Numbers.Natural.Abstract.NPow]
b:63 [in Coq.Numbers.NatInt.NZPow]
b:63 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:63 [in Coq.ssr.ssrbool]
B:63 [in Coq.Init.Datatypes]
b:63 [in Coq.Numbers.NatInt.NZSqrt]
b:63 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:63 [in Coq.Init.Logic]
b:63 [in Coq.Logic.ClassicalFacts]
b:63 [in Coq.Reals.RiemannInt_SF]
b:63 [in Coq.ZArith.Znumtheory]
b:63 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:63 [in Coq.NArith.Ndec]
b:64 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:64 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:64 [in Coq.Reals.RiemannInt]
b:64 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:64 [in Coq.Vectors.Fin]
b:64 [in Coq.Numbers.NatInt.NZDiv]
b:646 [in Coq.micromega.Tauto]
b:65 [in Coq.Numbers.Natural.Abstract.NDiv]
B:65 [in Coq.Sorting.PermutSetoid]
b:65 [in Coq.Numbers.Natural.Abstract.NPow]
b:65 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:65 [in Coq.Reals.R_sqrt]
b:65 [in Coq.setoid_ring.Field_theory]
b:65 [in Coq.Arith.PeanoNat]
b:65 [in Coq.ZArith.Zquot]
b:65 [in Coq.Lists.ListSet]
b:65 [in Coq.Numbers.NatInt.NZSqrt]
B:65 [in Coq.Init.Logic]
b:65 [in Coq.NArith.Ndec]
B:650 [in Coq.MSets.MSetRBT]
B:653 [in Coq.MSets.MSetRBT]
B:656 [in Coq.MSets.MSetRBT]
B:658 [in Coq.Init.Specif]
b:66 [in Coq.Sorting.PermutSetoid]
b:66 [in Coq.Numbers.NatInt.NZPow]
b:66 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:66 [in Coq.Numbers.NatInt.NZLog]
b:66 [in Coq.Bool.Bool]
b:66 [in Coq.Reals.RiemannInt_SF]
b:66 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:67 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:67 [in Coq.ssr.ssrbool]
b:67 [in Coq.Vectors.Fin]
b:67 [in Coq.ZArith.Zquot]
B:67 [in Coq.Init.Datatypes]
b:67 [in Coq.Numbers.NatInt.NZDiv]
b:67 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:67 [in Coq.Reals.R_sqr]
b:67 [in Coq.ZArith.Znumtheory]
b:67 [in Coq.NArith.Ndec]
b:68 [in Coq.Reals.Abstract.ConstructiveLUB]
b:68 [in Coq.Numbers.Natural.Abstract.NPow]
b:68 [in Coq.Reals.MVT]
b:68 [in Coq.Reals.R_sqrt]
b:68 [in Coq.Init.Specif]
b:68 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:68 [in Coq.Numbers.NatInt.NZLog]
B:68 [in Coq.Classes.CMorphisms]
b:68 [in Coq.NArith.BinNatDef]
B:68 [in Coq.Init.Logic]
B:680 [in Coq.Init.Specif]
B:684 [in Coq.Init.Specif]
b:688 [in Coq.MSets.MSetRBT]
b:69 [in Coq.Numbers.NatInt.NZPow]
b:69 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:69 [in Coq.Numbers.NaryFunctions]
b:69 [in Coq.Reals.NewtonInt]
b:69 [in Coq.ZArith.Zquot]
b:69 [in Coq.Numbers.NatInt.NZDiv]
b:69 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:69 [in Coq.Reals.RiemannInt_SF]
b:69 [in Coq.NArith.Ndec]
b:7 [in Coq.Init.Byte]
b:7 [in Coq.Bool.BoolOrder]
b:7 [in Coq.Reals.Runcountable]
b:7 [in Coq.Bool.IfProp]
B:7 [in Coq.Numbers.NaryFunctions]
b:7 [in Coq.ZArith.Zpow_facts]
B:7 [in Coq.Logic.FunctionalExtensionality]
b:7 [in Coq.Numbers.Natural.Abstract.NLcm]
b:7 [in Coq.Numbers.Natural.Abstract.NBits]
b:7 [in Coq.ssr.ssrbool]
B:7 [in Coq.Logic.Hurkens]
B:7 [in Coq.Numbers.Cyclic.Abstract.DoubleType]
b:7 [in Coq.Bool.Bool]
b:7 [in Coq.Sorting.Sorted]
b:7 [in Coq.Reals.NewtonInt]
b:7 [in Coq.Numbers.Cyclic.Int31.Int31]
b:7 [in Coq.Strings.Ascii]
b:7 [in Coq.ZArith.Zquot]
b:7 [in Coq.Numbers.Integer.Abstract.ZBits]
B:7 [in Coq.Sets.Powerset_facts]
b:7 [in Coq.Numbers.NatInt.NZDiv]
B:7 [in Coq.Init.Logic]
b:7 [in Coq.Reals.Cauchy.PosExtra]
B:7 [in Coq.Logic.FinFun]
b:70 [in Coq.setoid_ring.Field_theory]
b:70 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:70 [in Coq.Numbers.NatInt.NZLog]
b:70 [in Coq.Vectors.Fin]
b:70 [in Coq.Lists.ListSet]
b:70 [in Coq.Numbers.NatInt.NZSqrt]
B:70 [in Coq.Init.Logic]
B:701 [in Coq.Lists.List]
b:71 [in Coq.Numbers.Natural.Abstract.NDiv]
b:71 [in Coq.Numbers.Natural.Abstract.NPow]
b:71 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:71 [in Coq.Vectors.Fin]
b:71 [in Coq.ZArith.Zquot]
b:71 [in Coq.Numbers.NatInt.NZDiv]
b:71 [in Coq.ZArith.Znumtheory]
b:71 [in Coq.NArith.Ndec]
b:71 [in Coq.Sorting.Heap]
b:72 [in Coq.Numbers.NatInt.NZPow]
b:72 [in Coq.Reals.R_sqrt]
b:72 [in Coq.setoid_ring.Field_theory]
b:72 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:72 [in Coq.Numbers.NatInt.NZLog]
b:72 [in Coq.Numbers.NatInt.NZSqrt]
b:72 [in Coq.NArith.BinNatDef]
b:73 [in Coq.Numbers.Natural.Abstract.NPow]
b:73 [in Coq.Bool.Bool]
b:73 [in Coq.Vectors.Fin]
b:73 [in Coq.ZArith.Zquot]
B:73 [in Coq.Init.Datatypes]
b:73 [in Coq.Reals.Ratan]
b:73 [in Coq.Numbers.NatInt.NZDiv]
b:73 [in Coq.NArith.Ndec]
b:74 [in Coq.Numbers.Natural.Abstract.NDiv]
b:74 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:74 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:74 [in Coq.Bool.Bool]
b:74 [in Coq.NArith.BinNatDef]
b:74 [in Coq.Logic.ClassicalFacts]
b:74 [in Coq.Reals.RiemannInt_SF]
b:74 [in Coq.ZArith.Znumtheory]
b:75 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:75 [in Coq.Sorting.PermutSetoid]
b:75 [in Coq.Numbers.NatInt.NZPow]
B:75 [in Coq.Classes.Morphisms]
b:75 [in Coq.ZArith.Zdiv]
b:75 [in Coq.Bool.Bool]
b:75 [in Coq.Lists.ListSet]
b:75 [in Coq.NArith.Ndec]
B:75 [in Coq.Logic.FinFun]
b:76 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:76 [in Coq.Numbers.NaryFunctions]
B:76 [in Coq.Logic.FunctionalExtensionality]
b:76 [in Coq.Init.Wf]
b:76 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:76 [in Coq.Numbers.NatInt.NZLog]
b:76 [in Coq.Bool.Bool]
b:76 [in Coq.Structures.OrderedTypeEx]
b:76 [in Coq.ZArith.Zquot]
b:76 [in Coq.Numbers.NatInt.NZSqrt]
b:76 [in Coq.Numbers.NatInt.NZDiv]
b:76 [in Coq.NArith.BinNatDef]
b:77 [in Coq.Numbers.Natural.Abstract.NDiv]
b:77 [in Coq.Numbers.NatInt.NZPow]
b:77 [in Coq.Reals.RiemannInt]
b:77 [in Coq.setoid_ring.Field_theory]
b:77 [in Coq.ZArith.Zdiv]
b:77 [in Coq.Bool.Bool]
b:77 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:77 [in Coq.Reals.RiemannInt_SF]
b:77 [in Coq.NArith.Ndec]
b:78 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:78 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:78 [in Coq.Numbers.NaryFunctions]
b:78 [in Coq.Lists.List]
b:78 [in Coq.Numbers.Natural.Abstract.NBits]
b:78 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:78 [in Coq.Numbers.NatInt.NZLog]
b:78 [in Coq.Bool.Bool]
b:78 [in Coq.Structures.OrderedTypeEx]
B:78 [in Coq.Sorting.CPermutation]
b:78 [in Coq.Lists.ListSet]
b:78 [in Coq.Numbers.NatInt.NZSqrt]
b:79 [in Coq.Lists.Streams]
b:79 [in Coq.setoid_ring.Field_theory]
b:79 [in Coq.ZArith.Zdiv]
b:79 [in Coq.Bool.Bool]
b:79 [in Coq.ZArith.Zquot]
B:79 [in Coq.Init.Datatypes]
b:79 [in Coq.Numbers.NatInt.NZDiv]
b:79 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:79 [in Coq.NArith.Ndec]
b:8 [in Coq.Init.Byte]
b:8 [in Coq.Numbers.Natural.Abstract.NPow]
b:8 [in Coq.Numbers.NatInt.NZPow]
B:8 [in Coq.Classes.RelationPairs]
b:8 [in Coq.Numbers.Natural.Abstract.NDefOps]
b:8 [in Coq.Numbers.Integer.Abstract.ZLcm]
b:8 [in Coq.Numbers.Natural.Abstract.NSqrt]
b:8 [in Coq.ssr.ssrbool]
b:8 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:8 [in Coq.Numbers.NatInt.NZLog]
B:8 [in Coq.Relations.Relations]
b:8 [in Coq.Bool.Bool]
B:8 [in Coq.Sets.Cpo]
B:8 [in Coq.Logic.Berardi]
B:8 [in Coq.Program.Combinators]
b:8 [in Coq.Numbers.Integer.Abstract.ZPow]
B:8 [in Coq.Program.Basics]
b:8 [in Coq.NArith.Ndiv_def]
b:8 [in Coq.ZArith.Znumtheory]
b:8 [in Coq.ZArith.Zeuclid]
b:8 [in Coq.Reals.Cauchy.QExtra]
B:8 [in Coq.Bool.DecBool]
b:80 [in Coq.Numbers.Natural.Abstract.NDiv]
b:80 [in Coq.Numbers.NatInt.NZPow]
B:80 [in Coq.MSets.MSetProperties]
b:80 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:80 [in Coq.Numbers.Natural.Abstract.NBits]
b:80 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:80 [in Coq.Numbers.NatInt.NZLog]
b:80 [in Coq.Structures.OrderedTypeEx]
b:80 [in Coq.Numbers.NatInt.NZSqrt]
b:80 [in Coq.NArith.BinNatDef]
b:80 [in Coq.Reals.RiemannInt_SF]
B:80 [in Coq.FSets.FSetProperties]
b:81 [in Coq.Reals.RiemannInt]
b:81 [in Coq.Sorting.Permutation]
b:81 [in Coq.ZArith.Zdiv]
B:81 [in Coq.Sorting.CPermutation]
b:81 [in Coq.Lists.ListSet]
b:81 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:81 [in Coq.micromega.RMicromega]
b:81 [in Coq.NArith.Ndec]
b:82 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:82 [in Coq.Reals.Abstract.ConstructiveLUB]
B:82 [in Coq.Sorting.PermutSetoid]
B:82 [in Coq.micromega.RingMicromega]
b:82 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:82 [in Coq.Structures.OrderedTypeEx]
B:82 [in Coq.Classes.CMorphisms]
b:82 [in Coq.ZArith.Zquot]
b:82 [in Coq.Numbers.NatInt.NZSqrt]
b:82 [in Coq.Logic.ClassicalFacts]
b:83 [in Coq.Lists.Streams]
b:83 [in Coq.Numbers.Natural.Abstract.NDiv]
b:83 [in Coq.Sorting.PermutSetoid]
b:83 [in Coq.Numbers.NatInt.NZPow]
b:83 [in Coq.setoid_ring.Field_theory]
b:83 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:83 [in Coq.Numbers.NatInt.NZLog]
b:83 [in Coq.ZArith.Zdiv]
b:83 [in Coq.NArith.Ndec]
b:84 [in Coq.Reals.Abstract.ConstructiveLUB]
b:84 [in Coq.FSets.FMapFacts]
b:84 [in Coq.ZArith.Zquot]
b:84 [in Coq.Lists.ListSet]
b:84 [in Coq.Numbers.NatInt.NZSqrt]
b:84 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:84 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:85 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:85 [in Coq.Logic.ChoiceFacts]
b:85 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:85 [in Coq.ZArith.Zdiv]
B:85 [in Coq.Init.Datatypes]
b:85 [in Coq.Numbers.NatInt.NZDiv]
b:85 [in Coq.Reals.RiemannInt_SF]
b:85 [in Coq.NArith.Ndec]
b:86 [in Coq.Lists.Streams]
b:86 [in Coq.Numbers.Natural.Abstract.NDiv]
B:86 [in Coq.Sorting.PermutSetoid]
b:86 [in Coq.Numbers.NatInt.NZPow]
b:86 [in Coq.Reals.RiemannInt]
B:86 [in Coq.Classes.CMorphisms]
b:86 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:866 [in Coq.Lists.List]
b:87 [in Coq.Sorting.PermutSetoid]
B:87 [in Coq.micromega.RingMicromega]
b:87 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:87 [in Coq.Numbers.NatInt.NZLog]
B:87 [in Coq.Sorting.CPermutation]
b:87 [in Coq.ZArith.Zquot]
b:87 [in Coq.Reals.RiemannInt_SF]
b:87 [in Coq.Reals.Cauchy.QExtra]
b:87 [in Coq.NArith.Ndec]
b:88 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:88 [in Coq.Logic.FunctionalExtensionality]
b:88 [in Coq.Reals.NewtonInt]
B:88 [in Coq.Init.Datatypes]
b:88 [in Coq.Numbers.NatInt.NZDiv]
b:88 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:89 [in Coq.Numbers.Natural.Abstract.NDiv]
B:89 [in Coq.Sorting.PermutSetoid]
b:89 [in Coq.MSets.MSetProperties]
b:89 [in Coq.setoid_ring.Field_theory]
b:89 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:89 [in Coq.Numbers.NatInt.NZLog]
b:89 [in Coq.ZArith.Zdiv]
b:89 [in Coq.Reals.Abstract.ConstructiveSum]
b:89 [in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:89 [in Coq.FSets.FSetProperties]
b:89 [in Coq.NArith.Ndec]
B:9 [in Coq.Logic.Decidable]
b:9 [in Coq.Init.Byte]
B:9 [in Coq.Bool.IfProp]
b:9 [in Coq.ssr.ssrbool]
b:9 [in Coq.Reals.Machin]
b:9 [in Coq.Bool.Bool]
b:9 [in Coq.Strings.Ascii]
b:9 [in Coq.ZArith.Zquot]
B:9 [in Coq.Sets.Powerset_facts]
b:9 [in Coq.Numbers.NatInt.NZSqrt]
b:9 [in Coq.Numbers.NatInt.NZDiv]
b:90 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:90 [in Coq.Sorting.PermutSetoid]
b:90 [in Coq.Reals.RiemannInt]
B:90 [in Coq.ssr.ssreflect]
b:90 [in Coq.Bool.Bool]
b:90 [in Coq.Numbers.Cyclic.Int31.Int31]
b:90 [in Coq.ZArith.Zquot]
b:90 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:91 [in Coq.ZArith.BinIntDef]
b:91 [in Coq.Floats.SpecFloat]
b:91 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
b:91 [in Coq.Init.Specif]
b:91 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:91 [in Coq.Structures.OrderedTypeEx]
b:91 [in Coq.Numbers.NatInt.NZDiv]
b:91 [in Coq.micromega.ZifyInst]
b:91 [in Coq.NArith.Ndec]
b:92 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:92 [in Coq.MSets.MSetProperties]
b:92 [in Coq.Numbers.NatInt.NZLog]
b:92 [in Coq.ZArith.Zdiv]
b:92 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:92 [in Coq.FSets.FSetProperties]
B:93 [in Coq.Logic.FunctionalExtensionality]
b:93 [in Coq.setoid_ring.Field_theory]
b:93 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:93 [in Coq.ZArith.Zquot]
b:937 [in Coq.Lists.List]
b:94 [in Coq.Numbers.Natural.Abstract.NDiv]
b:94 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:94 [in Coq.Numbers.NatInt.NZLog]
B:94 [in Coq.ssr.ssreflect]
b:94 [in Coq.Structures.OrderedTypeEx]
b:94 [in Coq.Reals.NewtonInt]
b:94 [in Coq.Numbers.NatInt.NZDiv]
b:94 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:94 [in Coq.Reals.Abstract.ConstructiveMinMax]
b:94 [in Coq.NArith.Ndec]
B:946 [in Coq.Lists.List]
b:95 [in Coq.MSets.MSetProperties]
B:95 [in Coq.Numbers.NaryFunctions]
b:95 [in Coq.FSets.FMapFacts]
b:95 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:95 [in Coq.ZArith.Zdiv]
b:95 [in Coq.Bool.Bool]
b:95 [in Coq.micromega.RMicromega]
B:95 [in Coq.Logic.ClassicalFacts]
b:95 [in Coq.FSets.FSetProperties]
b:96 [in Coq.Bool.Bool]
b:96 [in Coq.Reals.Rbasic_fun]
b:96 [in Coq.ZArith.Zquot]
b:96 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:97 [in Coq.Numbers.Natural.Abstract.NDiv]
B:97 [in Coq.Sorting.PermutSetoid]
b:97 [in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:97 [in Coq.Numbers.NaryFunctions]
b:97 [in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
b:97 [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:97 [in Coq.ZArith.Zdiv]
b:97 [in Coq.Bool.Bool]
b:97 [in Coq.Structures.OrderedTypeEx]
b:97 [in Coq.Numbers.NatInt.NZDiv]
b:97 [in Coq.ZArith.Znumtheory]
b:97 [in Coq.NArith.Ndec]
b:98 [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:98 [in Coq.Sorting.PermutSetoid]
B:98 [in Coq.ssr.ssreflect]
b:98 [in Coq.Bool.Bool]
b:98 [in Coq.Reals.NewtonInt]
B:98 [in Coq.Sorting.CPermutation]
b:98 [in Coq.Numbers.Integer.Abstract.ZBits]
B:98 [in Coq.Logic.ClassicalFacts]
b:98 [in Coq.Reals.RiemannInt_SF]
b:99 [in Coq.ZArith.Zdiv]
b:99 [in Coq.Bool.Bool]
b:99 [in Coq.ZArith.Zquot]
b:99 [in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:994 [in Coq.Lists.List]
| 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 | (70451 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 | (1003 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 | (45703 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 | (771 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 | (1516 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 | (579 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 | (11670 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 | (1018 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 | (622 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 | (304 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 | (472 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 | (482 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 | (844 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 | (1187 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 | (4117 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 | (163 entries) |