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 | (72746 entries) |

Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1016 entries) |

Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (47311 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 | (787 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 | (1547 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 | (584 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 | (11763 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (959 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (627 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (308 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (475 entries) |

Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (492 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 | (903 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 | (1448 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 | (4360 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (166 entries) |

## Y

Y [definition, in Coq.Logic.WKL]Y [definition, in Coq.Logic.WeakFan]

yn:12 [binder, in Coq.Reals.Abstract.ConstructiveLimits]

yn:3 [binder, in Coq.Reals.Abstract.ConstructiveLimits]

yp:19 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

yp:23 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

yq:20 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

yq:24 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

yr [definition, in Coq.Reals.Rgeom]

ys:270 [binder, in Coq.MSets.MSetList]

yt [definition, in Coq.Reals.Rgeom]

Y_approx [lemma, in Coq.Logic.WKL]

Y_unique [lemma, in Coq.Logic.WKL]

Y_approx [lemma, in Coq.Logic.WeakFan]

Y_unique [lemma, in Coq.Logic.WeakFan]

y'':186 [binder, in Coq.Logic.EqdepFacts]

y'':188 [binder, in Coq.Logic.EqdepFacts]

y':101 [binder, in Coq.Relations.Relation_Operators]

y':111 [binder, in Coq.Relations.Relation_Operators]

y':114 [binder, in Coq.Relations.Relation_Operators]

y':127 [binder, in Coq.Relations.Relation_Operators]

y':185 [binder, in Coq.Logic.EqdepFacts]

y':187 [binder, in Coq.Logic.EqdepFacts]

y':259 [binder, in Coq.Logic.ChoiceFacts]

y':262 [binder, in Coq.Logic.ChoiceFacts]

y':35 [binder, in Coq.Logic.Eqdep_dec]

y':36 [binder, in Coq.Relations.Relation_Definitions]

y':37 [binder, in Coq.Relations.Relation_Definitions]

y':377 [binder, in Coq.Logic.ChoiceFacts]

y':383 [binder, in Coq.Logic.ChoiceFacts]

y':386 [binder, in Coq.Logic.ChoiceFacts]

y':389 [binder, in Coq.Logic.ChoiceFacts]

y':4 [binder, in Coq.Logic.Eqdep_dec]

y':48 [binder, in Coq.Logic.Decidable]

y':58 [binder, in Coq.Logic.Eqdep_dec]

y':58 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y':60 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y':61 [binder, in Coq.Init.Wf]

y':68 [binder, in Coq.Init.Wf]

y':7 [binder, in Coq.Wellfounded.Union]

y':74 [binder, in Coq.Init.Wf]

y':78 [binder, in Coq.Logic.ChoiceFacts]

y':8 [binder, in Coq.Wellfounded.Union]

y':9 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y':98 [binder, in Coq.Relations.Relation_Operators]

y0:12 [binder, in Coq.Reals.Rgeom]

y0:2 [binder, in Coq.Reals.Rgeom]

y0:22 [binder, in Coq.Reals.Rgeom]

y0:26 [binder, in Coq.Wellfounded.Lexicographic_Product]

y0:27 [binder, in Coq.Wellfounded.Lexicographic_Product]

y0:309 [binder, in Coq.Reals.Rtopology]

y0:312 [binder, in Coq.Reals.Rtopology]

y0:338 [binder, in Coq.Reals.Rtopology]

y0:339 [binder, in Coq.Reals.Rtopology]

y0:341 [binder, in Coq.Reals.Rtopology]

y0:342 [binder, in Coq.Reals.Rtopology]

y0:6 [binder, in Coq.Reals.Rgeom]

y0:654 [binder, in Coq.Lists.List]

y0:8 [binder, in Coq.Reals.Rgeom]

y1:10 [binder, in Coq.Reals.Rgeom]

y1:1120 [binder, in Coq.FSets.FMapAVL]

y1:1174 [binder, in Coq.FSets.FMapAVL]

y1:1179 [binder, in Coq.FSets.FMapAVL]

y1:14 [binder, in Coq.Reals.Rgeom]

y1:15 [binder, in Coq.micromega.OrderedRing]

y1:179 [binder, in Coq.Init.Logic]

y1:199 [binder, in Coq.Init.Logic]

y1:20 [binder, in Coq.micromega.OrderedRing]

y1:208 [binder, in Coq.Init.Logic]

y1:220 [binder, in Coq.Init.Logic]

y1:220 [binder, in Coq.setoid_ring.Ncring]

y1:235 [binder, in Coq.Init.Logic]

y1:24 [binder, in Coq.Reals.Rgeom]

y1:28 [binder, in Coq.micromega.OrderedRing]

y1:295 [binder, in Coq.Init.Logic]

y1:327 [binder, in Coq.Init.Logic]

y1:33 [binder, in Coq.micromega.OrderedRing]

y1:34 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y1:35 [binder, in Coq.Reals.Rgeom]

y1:389 [binder, in Coq.Lists.List]

y1:4 [binder, in Coq.Reals.Rgeom]

y1:50 [binder, in Coq.Reals.Rgeom]

y1:54 [binder, in Coq.Lists.List]

y1:55 [binder, in Coq.Reals.Rgeom]

y1:56 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y1:560 [binder, in Coq.MSets.MSetAVL]

y1:577 [binder, in Coq.MSets.MSetAVL]

y1:58 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y1:60 [binder, in Coq.Reals.Rgeom]

y1:67 [binder, in Coq.Reals.Rgeom]

y1:95 [binder, in Coq.Init.Datatypes]

y2:1121 [binder, in Coq.FSets.FMapAVL]

y2:1175 [binder, in Coq.FSets.FMapAVL]

y2:1180 [binder, in Coq.FSets.FMapAVL]

y2:16 [binder, in Coq.micromega.OrderedRing]

y2:16 [binder, in Coq.Reals.Rgeom]

y2:180 [binder, in Coq.Init.Logic]

y2:201 [binder, in Coq.Init.Logic]

y2:21 [binder, in Coq.micromega.OrderedRing]

y2:210 [binder, in Coq.Init.Logic]

y2:221 [binder, in Coq.setoid_ring.Ncring]

y2:222 [binder, in Coq.Init.Logic]

y2:237 [binder, in Coq.Init.Logic]

y2:26 [binder, in Coq.Reals.Rgeom]

y2:29 [binder, in Coq.micromega.OrderedRing]

y2:296 [binder, in Coq.Init.Logic]

y2:328 [binder, in Coq.Init.Logic]

y2:34 [binder, in Coq.micromega.OrderedRing]

y2:36 [binder, in Coq.Reals.Rgeom]

y2:390 [binder, in Coq.Lists.List]

y2:52 [binder, in Coq.Reals.Rgeom]

y2:55 [binder, in Coq.Lists.List]

y2:561 [binder, in Coq.MSets.MSetAVL]

y2:57 [binder, in Coq.Reals.Rgeom]

y2:578 [binder, in Coq.MSets.MSetAVL]

y2:62 [binder, in Coq.Reals.Rgeom]

y2:69 [binder, in Coq.Reals.Rgeom]

y2:96 [binder, in Coq.Init.Datatypes]

y3:212 [binder, in Coq.Init.Logic]

y3:224 [binder, in Coq.Init.Logic]

y3:239 [binder, in Coq.Init.Logic]

y3:297 [binder, in Coq.Init.Logic]

y4:226 [binder, in Coq.Init.Logic]

y4:241 [binder, in Coq.Init.Logic]

y5:243 [binder, in Coq.Init.Logic]

y:1 [binder, in Coq.Init.Tauto]

y:1 [binder, in Coq.Arith.Cantor]

y:10 [binder, in Coq.Structures.DecidableTypeEx]

Y:10 [binder, in Coq.Sets.Finite_sets_facts]

y:10 [binder, in Coq.PArith.BinPos]

y:10 [binder, in Coq.ZArith.BinInt]

y:10 [binder, in Coq.funind.Recdef]

y:10 [binder, in Coq.Sets.Partial_Order]

y:10 [binder, in Coq.Sets.Relations_1_facts]

y:10 [binder, in Coq.ZArith.Zbool]

y:10 [binder, in Coq.micromega.ZifyComparison]

y:10 [binder, in Coq.Structures.GenericMinMax]

y:10 [binder, in Coq.Reals.PSeries_reg]

y:10 [binder, in Coq.Reals.Ranalysis5]

y:10 [binder, in Coq.omega.PreOmega]

y:10 [binder, in Coq.Sets.Relations_1]

y:10 [binder, in Coq.Relations.Relation_Definitions]

y:10 [binder, in Coq.Reals.ROrderedType]

y:10 [binder, in Coq.Floats.FloatAxioms]

y:10 [binder, in Coq.Sorting.Heap]

y:10 [binder, in Coq.QArith.QArith_base]

y:10 [binder, in Coq.Structures.OrdersFacts]

y:100 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:100 [binder, in Coq.QArith.Qcanon]

y:100 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:100 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:100 [binder, in Coq.Structures.EqualitiesFacts]

y:100 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:100 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:100 [binder, in Coq.Relations.Relation_Operators]

y:101 [binder, in Coq.Program.Wf]

y:101 [binder, in Coq.Logic.Eqdep_dec]

y:101 [binder, in Coq.Structures.OrderedTypeEx]

y:101 [binder, in Coq.Reals.Rbasic_fun]

y:101 [binder, in Coq.setoid_ring.Ring_theory]

y:101 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:101 [binder, in Coq.Structures.OrdersFacts]

y:102 [binder, in Coq.Program.Wf]

y:102 [binder, in Coq.FSets.FSetBridge]

y:102 [binder, in Coq.Reals.Ranalysis4]

y:102 [binder, in Coq.Init.Nat]

y:102 [binder, in Coq.Sorting.Permutation]

y:102 [binder, in Coq.Structures.OrderedType]

y:102 [binder, in Coq.Reals.Ranalysis5]

y:102 [binder, in Coq.Structures.EqualitiesFacts]

y:102 [binder, in Coq.setoid_ring.Ncring]

y:102 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:102 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:103 [binder, in Coq.QArith.Qcanon]

y:103 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]

y:103 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:103 [binder, in Coq.Logic.ChoiceFacts]

y:103 [binder, in Coq.Reals.Rpower]

y:103 [binder, in Coq.Reals.Rtopology]

y:103 [binder, in Coq.Reals.Rbasic_fun]

y:103 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:103 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:103 [binder, in Coq.Structures.OrdersFacts]

y:103 [binder, in Coq.Reals.Cos_plus]

y:1036 [binder, in Coq.FSets.FMapAVL]

y:104 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:104 [binder, in Coq.FSets.FMapFacts]

y:104 [binder, in Coq.Reals.Rpower]

y:104 [binder, in Coq.Arith.PeanoNat]

y:104 [binder, in Coq.setoid_ring.Ring_theory]

y:104 [binder, in Coq.micromega.ZifyInst]

y:104 [binder, in Coq.Reals.ClassicalDedekindReals]

y:104 [binder, in Coq.Logic.FinFun]

y:1045 [binder, in Coq.FSets.FMapAVL]

y:105 [binder, in Coq.Program.Wf]

y:105 [binder, in Coq.QArith.Qcanon]

y:105 [binder, in Coq.Init.Nat]

y:105 [binder, in Coq.Reals.PSeries_reg]

y:105 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:1050 [binder, in Coq.FSets.FMapAVL]

y:1056 [binder, in Coq.FSets.FMapAVL]

y:1059 [binder, in Coq.FSets.FMapAVL]

y:106 [binder, in Coq.Program.Wf]

y:106 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:106 [binder, in Coq.Logic.ChoiceFacts]

y:106 [binder, in Coq.Reals.Ranalysis5]

y:106 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:106 [binder, in Coq.setoid_ring.Ncring]

y:106 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:106 [binder, in Coq.Structures.OrdersFacts]

y:1060 [binder, in Coq.Lists.List]

y:1062 [binder, in Coq.Init.Specif]

y:1066 [binder, in Coq.FSets.FMapAVL]

y:107 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:107 [binder, in Coq.Program.Wf]

y:107 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:107 [binder, in Coq.QArith.Qcanon]

y:107 [binder, in Coq.Lists.List]

y:107 [binder, in Coq.Structures.OrderedType]

y:107 [binder, in Coq.Reals.PSeries_reg]

y:107 [binder, in Coq.Init.Logic]

y:107 [binder, in Coq.micromega.ZifyInst]

y:1070 [binder, in Coq.FSets.FMapAVL]

y:1071 [binder, in Coq.Lists.List]

y:1075 [binder, in Coq.FSets.FMapAVL]

y:1077 [binder, in Coq.Lists.List]

y:108 [binder, in Coq.Program.Wf]

y:108 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:1080 [binder, in Coq.FSets.FMapAVL]

y:1082 [binder, in Coq.Init.Specif]

y:1084 [binder, in Coq.Lists.List]

y:1087 [binder, in Coq.FSets.FMapAVL]

y:1088 [binder, in Coq.Init.Specif]

y:109 [binder, in Coq.Program.Wf]

y:109 [binder, in Coq.QArith.Qcanon]

y:109 [binder, in Coq.Reals.Rfunctions]

y:109 [binder, in Coq.Reals.Rtopology]

y:109 [binder, in Coq.Reals.PSeries_reg]

y:109 [binder, in Coq.Lists.SetoidList]

y:109 [binder, in Coq.Structures.OrdersFacts]

y:1093 [binder, in Coq.FSets.FMapAVL]

y:11 [binder, in Coq.Structures.Orders]

y:11 [binder, in Coq.Relations.Operators_Properties]

y:11 [binder, in Coq.Structures.OrdersLists]

y:11 [binder, in Coq.Sets.Relations_3]

y:11 [binder, in Coq.FSets.FSetDecide]

y:11 [binder, in Coq.Arith.Bool_nat]

y:11 [binder, in Coq.Reals.Exp_prop]

y:11 [binder, in Coq.MSets.MSetDecide]

y:11 [binder, in Coq.Relations.Relations]

y:11 [binder, in Coq.QArith.Qreals]

y:11 [binder, in Coq.Lists.SetoidPermutation]

y:11 [binder, in Coq.Structures.OrderedTypeEx]

y:11 [binder, in Coq.Reals.Raxioms]

y:11 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]

y:11 [binder, in Coq.Bool.BoolEq]

y:11 [binder, in Coq.Classes.SetoidDec]

y:11 [binder, in Coq.Strings.Byte]

y:11 [binder, in Coq.Logic.HLevels]

y:11 [binder, in Coq.Sets.Relations_2]

Y:11 [binder, in Coq.Sets.Classical_sets]

y:11 [binder, in Coq.Structures.OrdersTac]

y:11 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:110 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:110 [binder, in Coq.Program.Wf]

y:110 [binder, in Coq.Logic.Eqdep_dec]

y:110 [binder, in Coq.Logic.ChoiceFacts]

y:110 [binder, in Coq.setoid_ring.Field_theory]

y:110 [binder, in Coq.Structures.OrderedType]

y:110 [binder, in Coq.Reals.Ranalysis5]

y:110 [binder, in Coq.setoid_ring.Ring_theory]

y:110 [binder, in Coq.setoid_ring.Ncring]

y:110 [binder, in Coq.Relations.Relation_Operators]

y:1101 [binder, in Coq.Init.Specif]

y:111 [binder, in Coq.Program.Wf]

y:111 [binder, in Coq.QArith.Qcanon]

y:111 [binder, in Coq.FSets.FMapFacts]

y:111 [binder, in Coq.Lists.ListSet]

y:111 [binder, in Coq.Reals.PSeries_reg]

y:111 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:111 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:1110 [binder, in Coq.FSets.FMapAVL]

y:1112 [binder, in Coq.Lists.List]

y:1113 [binder, in Coq.FSets.FMapAVL]

y:1116 [binder, in Coq.Lists.List]

y:1116 [binder, in Coq.FSets.FMapAVL]

y:112 [binder, in Coq.Program.Wf]

y:112 [binder, in Coq.Logic.Eqdep_dec]

y:112 [binder, in Coq.FSets.FSetDecide]

y:112 [binder, in Coq.MSets.MSetDecide]

y:112 [binder, in Coq.Reals.PSeries_reg]

y:112 [binder, in Coq.Structures.OrdersFacts]

y:1124 [binder, in Coq.FSets.FMapAVL]

y:1127 [binder, in Coq.Lists.List]

y:1129 [binder, in Coq.FSets.FMapAVL]

y:113 [binder, in Coq.Program.Wf]

y:113 [binder, in Coq.QArith.Qcanon]

y:113 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:113 [binder, in Coq.Reals.Rtrigo1]

y:113 [binder, in Coq.Structures.GenericMinMax]

y:113 [binder, in Coq.Reals.Ratan]

y:113 [binder, in Coq.setoid_ring.Ring_theory]

y:113 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:113 [binder, in Coq.Relations.Relation_Operators]

y:1132 [binder, in Coq.FSets.FMapAVL]

y:1136 [binder, in Coq.FSets.FMapAVL]

y:1138 [binder, in Coq.Lists.List]

y:114 [binder, in Coq.Program.Wf]

y:114 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]

y:114 [binder, in Coq.Lists.List]

y:114 [binder, in Coq.MSets.MSetGenTree]

y:114 [binder, in Coq.Lists.ListSet]

y:114 [binder, in Coq.Reals.PSeries_reg]

y:114 [binder, in Coq.setoid_ring.Ncring]

y:114 [binder, in Coq.Lists.SetoidList]

y:1142 [binder, in Coq.Lists.List]

y:1142 [binder, in Coq.FSets.FMapAVL]

y:1149 [binder, in Coq.Lists.List]

y:115 [binder, in Coq.Program.Wf]

y:115 [binder, in Coq.QArith.Qcanon]

y:115 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:115 [binder, in Coq.Reals.Rtrigo1]

y:115 [binder, in Coq.Reals.Rtopology]

y:115 [binder, in Coq.Structures.OrdersFacts]

y:1151 [binder, in Coq.FSets.FMapAVL]

y:1152 [binder, in Coq.Lists.List]

y:1154 [binder, in Coq.FSets.FMapAVL]

y:1155 [binder, in Coq.Lists.List]

y:1157 [binder, in Coq.FSets.FMapAVL]

y:116 [binder, in Coq.Program.Wf]

y:116 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]

y:116 [binder, in Coq.Logic.ChoiceFacts]

y:116 [binder, in Coq.Reals.Rtopology]

y:116 [binder, in Coq.Structures.OrderedType]

y:116 [binder, in Coq.Reals.PSeries_reg]

y:116 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:116 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:1161 [binder, in Coq.Lists.List]

y:1164 [binder, in Coq.Lists.List]

y:1168 [binder, in Coq.FSets.FMapAVL]

y:117 [binder, in Coq.Program.Wf]

y:117 [binder, in Coq.Reals.Rtrigo1]

y:117 [binder, in Coq.Logic.EqdepFacts]

y:117 [binder, in Coq.Logic.Hurkens]

y:117 [binder, in Coq.Reals.Rtopology]

y:117 [binder, in Coq.MSets.MSetGenTree]

y:117 [binder, in Coq.Lists.ListSet]

y:117 [binder, in Coq.setoid_ring.Ring_theory]

y:117 [binder, in Coq.Structures.OrdersFacts]

y:1171 [binder, in Coq.FSets.FMapAVL]

y:1178 [binder, in Coq.FSets.FMapAVL]

y:118 [binder, in Coq.Program.Wf]

y:118 [binder, in Coq.setoid_ring.InitialRing]

y:118 [binder, in Coq.Reals.Rtopology]

y:118 [binder, in Coq.Reals.Ratan]

y:118 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:119 [binder, in Coq.Program.Wf]

y:119 [binder, in Coq.Reals.Rtrigo1]

y:119 [binder, in Coq.Floats.SpecFloat]

y:119 [binder, in Coq.Reals.RiemannInt]

y:119 [binder, in Coq.Logic.Hurkens]

y:119 [binder, in Coq.ssr.ssrfun]

y:119 [binder, in Coq.Structures.OrderedTypeEx]

y:119 [binder, in Coq.Reals.Rtopology]

y:119 [binder, in Coq.Structures.OrderedType]

y:119 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:1194 [binder, in Coq.FSets.FMapAVL]

y:12 [binder, in Coq.Program.Wf]

y:12 [binder, in Coq.Structures.DecidableTypeEx]

y:12 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:12 [binder, in Coq.Wellfounded.Inverse_Image]

y:12 [binder, in Coq.Logic.Eqdep_dec]

y:12 [binder, in Coq.Structures.OrdersEx]

y:12 [binder, in Coq.Reals.ArithProp]

y:12 [binder, in Coq.Logic.JMeq]

y:12 [binder, in Coq.Structures.OrdersAlt]

y:12 [binder, in Coq.Logic.ChoiceFacts]

y:12 [binder, in Coq.Reals.Machin]

y:12 [binder, in Coq.ZArith.Zwf]

y:12 [binder, in Coq.Sets.Cpo]

y:12 [binder, in Coq.funind.Recdef]

y:12 [binder, in Coq.Structures.OrderedTypeAlt]

y:12 [binder, in Coq.micromega.ZifySint63]

y:12 [binder, in Coq.ZArith.Zbool]

y:12 [binder, in Coq.micromega.ZifyUint63]

y:12 [binder, in Coq.Sets.Permut]

y:12 [binder, in Coq.Reals.Ranalysis5]

y:12 [binder, in Coq.Sets.Relations_2]

y:12 [binder, in Coq.omega.PreOmega]

y:12 [binder, in Coq.Reals.Rlogic]

y:12 [binder, in Coq.Reals.ROrderedType]

y:12 [binder, in Coq.Reals.Cos_rel]

Y:12 [binder, in Coq.Sets.Infinite_sets]

y:12 [binder, in Coq.Reals.ClassicalConstructiveReals]

y:12 [binder, in Coq.Relations.Relation_Operators]

y:12 [binder, in Coq.Bool.DecBool]

y:12 [binder, in Coq.Structures.OrdersFacts]

y:12 [binder, in Coq.Sets.Powerset]

y:120 [binder, in Coq.Program.Wf]

y:120 [binder, in Coq.MSets.MSetList]

y:120 [binder, in Coq.Reals.Rtopology]

y:120 [binder, in Coq.Lists.ListSet]

y:120 [binder, in Coq.Reals.Ratan]

y:120 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:120 [binder, in Coq.Structures.OrdersFacts]

y:121 [binder, in Coq.Program.Wf]

y:121 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:121 [binder, in Coq.Reals.Rtrigo1]

y:121 [binder, in Coq.Reals.Ranalysis5]

y:121 [binder, in Coq.setoid_ring.Ring_theory]

y:121 [binder, in Coq.Init.Logic]

y:122 [binder, in Coq.Program.Wf]

y:122 [binder, in Coq.Logic.EqdepFacts]

y:122 [binder, in Coq.PArith.BinPos]

y:122 [binder, in Coq.Reals.MVT]

y:122 [binder, in Coq.FSets.FMapFacts]

y:122 [binder, in Coq.Reals.RiemannInt]

y:122 [binder, in Coq.Logic.ChoiceFacts]

y:122 [binder, in Coq.Structures.OrderedTypeEx]

y:122 [binder, in Coq.Classes.CRelationClasses]

y:122 [binder, in Coq.Structures.OrderedType]

y:122 [binder, in Coq.Reals.Ratan]

y:122 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:122 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:122 [binder, in Coq.Structures.OrdersFacts]

y:123 [binder, in Coq.QArith.Qcanon]

y:123 [binder, in Coq.Logic.Eqdep_dec]

y:123 [binder, in Coq.Reals.Rtrigo1]

y:123 [binder, in Coq.Logic.ChoiceFacts]

y:124 [binder, in Coq.Reals.PSeries_reg]

y:124 [binder, in Coq.Reals.Ratan]

y:124 [binder, in Coq.Structures.OrdersFacts]

y:125 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:125 [binder, in Coq.Reals.Abstract.ConstructiveLUB]

y:125 [binder, in Coq.Reals.Rtrigo1]

y:125 [binder, in Coq.Reals.MVT]

y:125 [binder, in Coq.FSets.FMapFacts]

y:125 [binder, in Coq.Reals.RiemannInt]

y:125 [binder, in Coq.Reals.PSeries_reg]

y:125 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:125 [binder, in Coq.Relations.Relation_Operators]

y:126 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:126 [binder, in Coq.Logic.EqdepFacts]

y:126 [binder, in Coq.Classes.CRelationClasses]

y:126 [binder, in Coq.Relations.Relation_Operators]

y:126 [binder, in Coq.Structures.OrdersFacts]

y:127 [binder, in Coq.QArith.Qcanon]

y:127 [binder, in Coq.Reals.Rtrigo1]

y:127 [binder, in Coq.Logic.ChoiceFacts]

y:127 [binder, in Coq.Reals.Rbasic_fun]

y:128 [binder, in Coq.Program.Wf]

y:128 [binder, in Coq.Lists.ListSet]

y:128 [binder, in Coq.Structures.OrdersFacts]

y:129 [binder, in Coq.Program.Wf]

y:129 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:129 [binder, in Coq.Reals.Abstract.ConstructiveLUB]

y:129 [binder, in Coq.Reals.Rtrigo1]

y:129 [binder, in Coq.setoid_ring.InitialRing]

y:129 [binder, in Coq.ssr.ssrfun]

y:129 [binder, in Coq.Reals.Rbasic_fun]

y:1292 [binder, in Coq.FSets.FMapAVL]

y:13 [binder, in Coq.Program.Wf]

y:13 [binder, in Coq.Relations.Operators_Properties]

y:13 [binder, in Coq.ZArith.BinIntDef]

y:13 [binder, in Coq.FSets.FSetDecide]

y:13 [binder, in Coq.Logic.EqdepFacts]

y:13 [binder, in Coq.Arith.Bool_nat]

y:13 [binder, in Coq.Reals.MVT]

y:13 [binder, in Coq.ZArith.Zpow_facts]

y:13 [binder, in Coq.Arith.Wf_nat]

y:13 [binder, in Coq.MSets.MSetDecide]

y:13 [binder, in Coq.Program.Subset]

y:13 [binder, in Coq.Init.Wf]

y:13 [binder, in Coq.setoid_ring.Cring]

y:13 [binder, in Coq.QArith.Qreals]

y:13 [binder, in Coq.QArith.Qfield]

y:13 [binder, in Coq.QArith.Qabs]

y:13 [binder, in Coq.Lists.ListDec]

y:13 [binder, in Coq.Classes.EquivDec]

y:13 [binder, in Coq.Reals.Raxioms]

y:13 [binder, in Coq.Structures.Equalities]

y:13 [binder, in Coq.Bool.BoolEq]

y:13 [binder, in Coq.Structures.GenericMinMax]

y:13 [binder, in Coq.Logic.ProofIrrelevanceFacts]

y:13 [binder, in Coq.Numbers.Cyclic.Int63.Ring63]

y:13 [binder, in Coq.Structures.OrdersTac]

y:13 [binder, in Coq.Reals.R_sqr]

y:13 [binder, in Coq.QArith.Qround]

y:13 [binder, in Coq.Relations.Relation_Operators]

y:13 [binder, in Coq.Sorting.Heap]

y:13 [binder, in Coq.Lists.SetoidList]

y:13 [binder, in Coq.Numbers.Cyclic.Int31.Ring31]

y:130 [binder, in Coq.QArith.Qcanon]

y:130 [binder, in Coq.Logic.Eqdep_dec]

y:130 [binder, in Coq.FSets.FMapFacts]

y:130 [binder, in Coq.Reals.RiemannInt]

y:130 [binder, in Coq.Logic.Hurkens]

y:130 [binder, in Coq.Classes.CRelationClasses]

y:130 [binder, in Coq.Reals.Rtopology]

y:130 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:130 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:130 [binder, in Coq.Structures.OrdersFacts]

y:131 [binder, in Coq.Reals.Rtrigo1]

y:131 [binder, in Coq.FSets.FSetDecide]

y:131 [binder, in Coq.MSets.MSetEqProperties]

y:131 [binder, in Coq.Reals.RiemannInt]

y:131 [binder, in Coq.MSets.MSetDecide]

y:131 [binder, in Coq.MSets.MSetList]

y:131 [binder, in Coq.ssr.ssreflect]

y:131 [binder, in Coq.FSets.FSetEqProperties]

y:131 [binder, in Coq.Lists.ListSet]

y:132 [binder, in Coq.Program.Wf]

y:132 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:132 [binder, in Coq.Reals.MVT]

y:132 [binder, in Coq.Reals.RiemannInt]

y:132 [binder, in Coq.Logic.Hurkens]

y:132 [binder, in Coq.ssr.ssreflect]

y:132 [binder, in Coq.Reals.Rpower]

y:132 [binder, in Coq.Reals.Rtopology]

y:133 [binder, in Coq.Program.Wf]

y:133 [binder, in Coq.QArith.Qcanon]

y:133 [binder, in Coq.Reals.Rtrigo1]

y:133 [binder, in Coq.Arith.Wf_nat]

y:133 [binder, in Coq.Reals.RiemannInt]

y:133 [binder, in Coq.ssr.ssreflect]

y:133 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:1337 [binder, in Coq.FSets.FMapAVL]

y:134 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:134 [binder, in Coq.FSets.FMapFacts]

y:134 [binder, in Coq.FSets.FSetInterface]

y:134 [binder, in Coq.ssr.ssreflect]

y:134 [binder, in Coq.Lists.ListSet]

y:134 [binder, in Coq.Relations.Relation_Operators]

y:1342 [binder, in Coq.FSets.FMapAVL]

y:135 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:135 [binder, in Coq.Reals.Rtrigo1]

y:135 [binder, in Coq.Reals.Rsqrt_def]

y:135 [binder, in Coq.MSets.MSetList]

y:135 [binder, in Coq.Reals.Rtopology]

y:135 [binder, in Coq.FSets.FSetCompat]

y:135 [binder, in Coq.Structures.OrdersFacts]

y:1351 [binder, in Coq.FSets.FMapAVL]

y:1354 [binder, in Coq.FSets.FMapAVL]

y:136 [binder, in Coq.Sorting.PermutSetoid]

y:136 [binder, in Coq.Reals.Rbasic_fun]

y:136 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:136 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:137 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:137 [binder, in Coq.Reals.Rtrigo1]

y:137 [binder, in Coq.Reals.Rsqrt_def]

y:137 [binder, in Coq.Reals.Rtopology]

y:137 [binder, in Coq.FSets.FMapWeakList]

y:137 [binder, in Coq.Reals.Ratan]

y:137 [binder, in Coq.Relations.Relation_Operators]

y:137 [binder, in Coq.Structures.OrdersFacts]

y:138 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:138 [binder, in Coq.Logic.EqdepFacts]

y:138 [binder, in Coq.Arith.Wf_nat]

y:138 [binder, in Coq.FSets.FMapFacts]

y:138 [binder, in Coq.Reals.Ratan]

y:138 [binder, in Coq.Init.Logic]

y:139 [binder, in Coq.Logic.Eqdep_dec]

y:139 [binder, in Coq.Reals.Rtrigo1]

y:139 [binder, in Coq.Reals.MVT]

y:139 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:139 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:139 [binder, in Coq.Structures.OrdersFacts]

y:1396 [binder, in Coq.FSets.FMapAVL]

y:14 [binder, in Coq.Structures.Orders]

y:14 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:14 [binder, in Coq.nsatz.NsatzTactic]

y:14 [binder, in Coq.Logic.Eqdep_dec]

y:14 [binder, in Coq.FSets.FSetBridge]

y:14 [binder, in Coq.Reals.Rfunctions]

y:14 [binder, in Coq.Reals.MVT]

y:14 [binder, in Coq.Strings.String]

y:14 [binder, in Coq.Reals.Exp_prop]

y:14 [binder, in Coq.Structures.OrdersAlt]

y:14 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]

y:14 [binder, in Coq.setoid_ring.Integral_domain]

y:14 [binder, in Coq.Logic.ClassicalChoice]

y:14 [binder, in Coq.Reals.Abstract.ConstructiveAbs]

y:14 [binder, in Coq.Logic.IndefiniteDescription]

y:14 [binder, in Coq.omega.OmegaLemmas]

y:14 [binder, in Coq.Structures.OrderedTypeEx]

y:14 [binder, in Coq.Sets.Relations_1_facts]

y:14 [binder, in Coq.Structures.OrderedTypeAlt]

y:14 [binder, in Coq.Sets.Relations_2_facts]

y:14 [binder, in Coq.micromega.ZifySint63]

y:14 [binder, in Coq.Structures.OrderedType]

y:14 [binder, in Coq.Classes.SetoidClass]

y:14 [binder, in Coq.micromega.ZifyUint63]

y:14 [binder, in Coq.Reals.Ranalysis5]

y:14 [binder, in Coq.Setoids.Setoid]

y:14 [binder, in Coq.omega.PreOmega]

y:14 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:14 [binder, in Coq.Sets.Classical_sets]

y:14 [binder, in Coq.Reals.Rlogic]

y:14 [binder, in Coq.Sets.Relations_1]

y:14 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:14 [binder, in Coq.micromega.ZCoeff]

y:14 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:140 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:140 [binder, in Coq.ssr.ssrfun]

y:140 [binder, in Coq.Init.Datatypes]

y:1406 [binder, in Coq.FSets.FMapAVL]

y:141 [binder, in Coq.Logic.Eqdep_dec]

y:141 [binder, in Coq.Sorting.PermutSetoid]

y:141 [binder, in Coq.Reals.Rtrigo1]

y:141 [binder, in Coq.Reals.Rsqrt_def]

y:141 [binder, in Coq.Reals.RiemannInt]

y:141 [binder, in Coq.ssr.ssrfun]

y:141 [binder, in Coq.Reals.Rtopology]

y:141 [binder, in Coq.FSets.FMapWeakList]

y:141 [binder, in Coq.FSets.FSetCompat]

y:141 [binder, in Coq.Structures.OrdersFacts]

y:1410 [binder, in Coq.FSets.FMapAVL]

y:1415 [binder, in Coq.FSets.FMapAVL]

y:142 [binder, in Coq.FSets.FMapFacts]

y:142 [binder, in Coq.Reals.Rtopology]

y:142 [binder, in Coq.Init.Logic]

y:142 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:142 [binder, in Coq.QArith.QArith_base]

y:1420 [binder, in Coq.FSets.FMapAVL]

y:1423 [binder, in Coq.FSets.FMapAVL]

y:1427 [binder, in Coq.FSets.FMapAVL]

y:143 [binder, in Coq.Reals.Rtrigo1]

y:143 [binder, in Coq.Logic.EqdepFacts]

y:143 [binder, in Coq.FSets.FSetPositive]

y:143 [binder, in Coq.Reals.Rtopology]

y:143 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:143 [binder, in Coq.Structures.OrdersFacts]

y:144 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:144 [binder, in Coq.QArith.Qcanon]

y:145 [binder, in Coq.Reals.Rtrigo1]

y:145 [binder, in Coq.FSets.FMapFullAVL]

y:145 [binder, in Coq.Structures.OrderedTypeEx]

y:145 [binder, in Coq.Init.Datatypes]

y:145 [binder, in Coq.setoid_ring.Ring_theory]

y:145 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:145 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:145 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:145 [binder, in Coq.Structures.OrdersFacts]

y:1452 [binder, in Coq.FSets.FMapAVL]

y:146 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:146 [binder, in Coq.QArith.Qcanon]

y:146 [binder, in Coq.FSets.FMapFacts]

y:146 [binder, in Coq.Reals.Rtopology]

y:146 [binder, in Coq.FSets.FMapWeakList]

y:146 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:146 [binder, in Coq.Init.Logic]

y:147 [binder, in Coq.Reals.Rtrigo1]

y:147 [binder, in Coq.Logic.EqdepFacts]

y:147 [binder, in Coq.Reals.Rtopology]

y:147 [binder, in Coq.QArith.QArith_base]

y:147 [binder, in Coq.FSets.FSetCompat]

y:147 [binder, in Coq.Structures.OrdersFacts]

y:148 [binder, in Coq.QArith.Qcanon]

y:148 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:148 [binder, in Coq.MSets.MSetGenTree]

y:148 [binder, in Coq.Reals.Ratan]

y:148 [binder, in Coq.setoid_ring.Ring_theory]

y:148 [binder, in Coq.FSets.FMapList]

y:148 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:148 [binder, in Coq.Relations.Relation_Operators]

y:1487 [binder, in Coq.FSets.FMapAVL]

y:149 [binder, in Coq.Reals.Rtrigo1]

y:149 [binder, in Coq.Reals.Ratan]

y:149 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:149 [binder, in Coq.Reals.SeqProp]

y:149 [binder, in Coq.Structures.OrdersFacts]

y:15 [binder, in Coq.Relations.Operators_Properties]

y:15 [binder, in Coq.Wellfounded.Well_Ordering]

y:15 [binder, in Coq.Structures.OrdersEx]

y:15 [binder, in Coq.QArith.Qcabs]

y:15 [binder, in Coq.Arith.Bool_nat]

y:15 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]

y:15 [binder, in Coq.Program.Subset]

y:15 [binder, in Coq.QArith.Qreals]

y:15 [binder, in Coq.Logic.ClassicalUniqueChoice]

y:15 [binder, in Coq.Reals.Raxioms]

y:15 [binder, in Coq.ZArith.Zbool]

y:15 [binder, in Coq.Bool.BoolEq]

y:15 [binder, in Coq.Reals.PSeries_reg]

y:15 [binder, in Coq.Sets.Powerset_facts]

y:15 [binder, in Coq.Numbers.Cyclic.Int63.Ring63]

y:15 [binder, in Coq.Structures.OrdersTac]

y:15 [binder, in Coq.Reals.R_sqr]

y:15 [binder, in Coq.micromega.ZifyInst]

y:15 [binder, in Coq.QArith.Qround]

y:15 [binder, in Coq.Numbers.Cyclic.Int31.Ring31]

y:15 [binder, in Coq.Structures.OrdersFacts]

y:150 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:150 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:150 [binder, in Coq.Sorting.PermutSetoid]

y:150 [binder, in Coq.FSets.FMapFacts]

y:150 [binder, in Coq.Reals.Rtopology]

y:150 [binder, in Coq.Init.Datatypes]

y:150 [binder, in Coq.Init.Logic]

y:150 [binder, in Coq.setoid_ring.Ncring]

y:150 [binder, in Coq.Lists.SetoidList]

y:151 [binder, in Coq.Reals.Rtrigo1]

y:151 [binder, in Coq.FSets.FMapWeakList]

y:151 [binder, in Coq.Reals.Ratan]

y:151 [binder, in Coq.setoid_ring.Ring_theory]

y:151 [binder, in Coq.Relations.Relation_Operators]

y:151 [binder, in Coq.QArith.QArith_base]

y:152 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:152 [binder, in Coq.setoid_ring.InitialRing]

y:152 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:152 [binder, in Coq.FSets.FMapList]

y:152 [binder, in Coq.Structures.OrdersFacts]

y:153 [binder, in Coq.Reals.Rtrigo1]

y:153 [binder, in Coq.MSets.MSetGenTree]

y:153 [binder, in Coq.Reals.Ratan]

y:154 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:154 [binder, in Coq.FSets.FMapFacts]

y:154 [binder, in Coq.QArith.QArith_base]

y:155 [binder, in Coq.Reals.Rtrigo1]

y:155 [binder, in Coq.FSets.FMapFullAVL]

y:155 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:155 [binder, in Coq.Structures.OrdersFacts]

y:156 [binder, in Coq.Logic.Eqdep_dec]

y:156 [binder, in Coq.Logic.EqdepFacts]

y:156 [binder, in Coq.Lists.ListSet]

y:156 [binder, in Coq.Relations.Relation_Operators]

y:156 [binder, in Coq.Lists.SetoidList]

y:157 [binder, in Coq.Reals.Rtrigo1]

y:157 [binder, in Coq.FSets.FMapFacts]

y:157 [binder, in Coq.Reals.Ratan]

y:157 [binder, in Coq.setoid_ring.Ring_theory]

y:157 [binder, in Coq.FSets.FMapList]

y:157 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:157 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:157 [binder, in Coq.Structures.OrdersFacts]

y:158 [binder, in Coq.Logic.EqdepFacts]

y:158 [binder, in Coq.MSets.MSetGenTree]

y:158 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:159 [binder, in Coq.Logic.Eqdep_dec]

y:159 [binder, in Coq.FSets.FMapFullAVL]

y:159 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:159 [binder, in Coq.Structures.OrdersFacts]

y:16 [binder, in Coq.Structures.Orders]

y:16 [binder, in Coq.Program.Wf]

y:16 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:16 [binder, in Coq.QArith.Qcanon]

y:16 [binder, in Coq.nsatz.NsatzTactic]

y:16 [binder, in Coq.Logic.Eqdep_dec]

y:16 [binder, in Coq.Reals.Abstract.ConstructiveLUB]

y:16 [binder, in Coq.Classes.RelationClasses]

y:16 [binder, in Coq.Reals.Binomial]

y:16 [binder, in Coq.Structures.OrdersAlt]

y:16 [binder, in Coq.Program.Subset]

y:16 [binder, in Coq.Reals.Rpower]

y:16 [binder, in Coq.omega.OmegaLemmas]

y:16 [binder, in Coq.ZArith.Int]

y:16 [binder, in Coq.Strings.Ascii]

y:16 [binder, in Coq.Sets.Permut]

y:16 [binder, in Coq.omega.PreOmega]

y:16 [binder, in Coq.Reals.RiemannInt_SF]

y:16 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:16 [binder, in Coq.micromega.ZCoeff]

y:16 [binder, in Coq.QArith.Qreduction]

y:16 [binder, in Coq.Floats.FloatAxioms]

Y:16 [binder, in Coq.Sets.Infinite_sets]

y:16 [binder, in Coq.Reals.ClassicalConstructiveReals]

y:16 [binder, in Coq.Sorting.Heap]

y:16 [binder, in Coq.Logic.FinFun]

y:160 [binder, in Coq.FSets.FSetBridge]

y:160 [binder, in Coq.Logic.EqdepFacts]

y:160 [binder, in Coq.FSets.FMapFacts]

y:160 [binder, in Coq.setoid_ring.Ring_theory]

y:161 [binder, in Coq.omega.OmegaLemmas]

y:161 [binder, in Coq.MSets.MSetRBT]

y:161 [binder, in Coq.Structures.OrdersFacts]

y:162 [binder, in Coq.FSets.FMapAVL]

y:163 [binder, in Coq.Logic.Eqdep_dec]

y:163 [binder, in Coq.Logic.EqdepFacts]

y:163 [binder, in Coq.FSets.FMapFacts]

y:163 [binder, in Coq.MSets.MSetGenTree]

y:163 [binder, in Coq.setoid_ring.Ring_theory]

y:164 [binder, in Coq.Reals.Rfunctions]

y:164 [binder, in Coq.Reals.MVT]

y:164 [binder, in Coq.FSets.FMapFullAVL]

y:164 [binder, in Coq.Reals.Ratan]

y:164 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:164 [binder, in Coq.QArith.QArith_base]

y:165 [binder, in Coq.Reals.MVT]

y:165 [binder, in Coq.FSets.FSetInterface]

y:165 [binder, in Coq.omega.OmegaLemmas]

y:165 [binder, in Coq.Reals.Ratan]

y:166 [binder, in Coq.Reals.MVT]

y:166 [binder, in Coq.FSets.FMapFacts]

y:166 [binder, in Coq.Reals.Rpower]

y:166 [binder, in Coq.FSets.FMapAVL]

y:166 [binder, in Coq.Reals.PSeries_reg]

y:166 [binder, in Coq.QArith.QArith_base]

y:167 [binder, in Coq.FSets.FSetBridge]

y:167 [binder, in Coq.Reals.Rfunctions]

y:167 [binder, in Coq.Reals.MVT]

y:167 [binder, in Coq.ssr.ssrfun]

y:167 [binder, in Coq.Reals.Ratan]

y:167 [binder, in Coq.Reals.Ranalysis5]

y:167 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:168 [binder, in Coq.Reals.MVT]

y:168 [binder, in Coq.Reals.PSeries_reg]

y:168 [binder, in Coq.setoid_ring.Ring_theory]

y:169 [binder, in Coq.Reals.MVT]

y:169 [binder, in Coq.FSets.FMapFacts]

y:169 [binder, in Coq.FSets.FMapFullAVL]

y:169 [binder, in Coq.omega.OmegaLemmas]

y:169 [binder, in Coq.Reals.PSeries_reg]

y:169 [binder, in Coq.Reals.Ratan]

y:169 [binder, in Coq.QArith.QArith_base]

y:17 [binder, in Coq.Program.Wf]

y:17 [binder, in Coq.Relations.Operators_Properties]

y:17 [binder, in Coq.Structures.OrdersLists]

y:17 [binder, in Coq.Sets.Relations_3]

y:17 [binder, in Coq.QArith.Qcabs]

y:17 [binder, in Coq.Arith.Bool_nat]

y:17 [binder, in Coq.ZArith.BinInt]

y:17 [binder, in Coq.Reals.Abstract.ConstructivePower]

y:17 [binder, in Coq.Logic.JMeq]

y:17 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]

y:17 [binder, in Coq.Logic.ChoiceFacts]

y:17 [binder, in Coq.Init.Wf]

y:17 [binder, in Coq.QArith.Qreals]

y:17 [binder, in Coq.Sets.Cpo]

y:17 [binder, in Coq.Structures.OrderedTypeEx]

y:17 [binder, in Coq.Structures.OrderedTypeAlt]

y:17 [binder, in Coq.ZArith.Zbool]

y:17 [binder, in Coq.Structures.Equalities]

y:17 [binder, in Coq.Structures.OrderedType]

y:17 [binder, in Coq.Sets.Powerset_facts]

y:17 [binder, in Coq.Numbers.Cyclic.Int63.Ring63]

y:17 [binder, in Coq.Sets.Relations_2]

y:17 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:17 [binder, in Coq.Logic.Diaconescu]

y:17 [binder, in Coq.Sets.Classical_sets]

y:17 [binder, in Coq.Reals.RiemannInt_SF]

y:17 [binder, in Coq.micromega.ZifyInst]

y:17 [binder, in Coq.Reals.Cos_rel]

Y:17 [binder, in Coq.Sets.Infinite_sets]

y:17 [binder, in Coq.Numbers.Cyclic.Int31.Ring31]

y:17 [binder, in Coq.Structures.OrdersFacts]

y:170 [binder, in Coq.Reals.MVT]

y:170 [binder, in Coq.MSets.MSetGenTree]

y:170 [binder, in Coq.Reals.PSeries_reg]

y:170 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:170 [binder, in Coq.ZArith.Znumtheory]

y:171 [binder, in Coq.Reals.MVT]

y:171 [binder, in Coq.FSets.FMapAVL]

y:172 [binder, in Coq.FSets.FMapFullAVL]

y:172 [binder, in Coq.QArith.QArith_base]

y:173 [binder, in Coq.setoid_ring.Field_theory]

y:174 [binder, in Coq.FSets.FSetBridge]

y:174 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:174 [binder, in Coq.QArith.QArith_base]

y:175 [binder, in Coq.MSets.MSetGenTree]

y:175 [binder, in Coq.Reals.PSeries_reg]

y:176 [binder, in Coq.FSets.FMapFullAVL]

y:176 [binder, in Coq.ssr.ssrfun]

y:176 [binder, in Coq.setoid_ring.Ncring]

y:176 [binder, in Coq.QArith.QArith_base]

y:177 [binder, in Coq.FSets.FSetBridge]

y:177 [binder, in Coq.ssr.ssrfun]

y:177 [binder, in Coq.Reals.Rpower]

y:177 [binder, in Coq.Reals.PSeries_reg]

y:177 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:178 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:178 [binder, in Coq.QArith.QArith_base]

y:179 [binder, in Coq.Vectors.VectorSpec]

y:179 [binder, in Coq.FSets.FMapAVL]

y:179 [binder, in Coq.Vectors.Fin]

y:179 [binder, in Coq.setoid_ring.Ncring]

y:18 [binder, in Coq.Structures.Orders]

y:18 [binder, in Coq.QArith.Qcanon]

y:18 [binder, in Coq.nsatz.NsatzTactic]

y:18 [binder, in Coq.FSets.FSetBridge]

y:18 [binder, in Coq.Logic.EqdepFacts]

y:18 [binder, in Coq.Strings.String]

y:18 [binder, in Coq.Reals.R_sqrt]

y:18 [binder, in Coq.Structures.OrdersAlt]

y:18 [binder, in Coq.QArith.Qabs]

y:18 [binder, in Coq.Reals.Rdefinitions]

y:18 [binder, in Coq.Reals.Rpower]

y:18 [binder, in Coq.omega.OmegaLemmas]

y:18 [binder, in Coq.Sets.Partial_Order]

y:18 [binder, in Coq.Structures.GenericMinMax]

y:18 [binder, in Coq.Sets.Relations_2]

y:18 [binder, in Coq.ssr.ssrunder]

y:18 [binder, in Coq.Classes.DecidableClass]

y:18 [binder, in Coq.ZArith.Znumtheory]

Y:18 [binder, in Coq.Sets.Infinite_sets]

y:18 [binder, in Coq.Relations.Relation_Operators]

y:18 [binder, in Coq.Bool.DecBool]

y:18 [binder, in Coq.Lists.SetoidList]

y:180 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:180 [binder, in Coq.FSets.FSetBridge]

y:180 [binder, in Coq.FSets.FSetInterface]

y:180 [binder, in Coq.Structures.OrderedType]

y:181 [binder, in Coq.Sorting.Permutation]

y:182 [binder, in Coq.setoid_ring.Ncring]

y:184 [binder, in Coq.Logic.EqdepFacts]

y:184 [binder, in Coq.micromega.RingMicromega]

y:184 [binder, in Coq.FSets.FMapAVL]

y:184 [binder, in Coq.Structures.OrderedType]

y:185 [binder, in Coq.FSets.FMapFacts]

y:185 [binder, in Coq.FSets.FSetInterface]

y:185 [binder, in Coq.Init.Logic]

y:186 [binder, in Coq.FSets.FSetBridge]

y:186 [binder, in Coq.micromega.RingMicromega]

y:186 [binder, in Coq.omega.OmegaLemmas]

y:186 [binder, in Coq.Structures.GenericMinMax]

y:186 [binder, in Coq.Reals.Ranalysis5]

y:186 [binder, in Coq.setoid_ring.Ring_theory]

y:186 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:187 [binder, in Coq.Reals.Rtopology]

y:187 [binder, in Coq.setoid_ring.Ncring]

y:188 [binder, in Coq.micromega.RingMicromega]

y:189 [binder, in Coq.FSets.FSetBridge]

y:189 [binder, in Coq.FSets.FMapAVL]

y:189 [binder, in Coq.Reals.Rtopology]

y:189 [binder, in Coq.Structures.GenericMinMax]

y:189 [binder, in Coq.Reals.PSeries_reg]

y:189 [binder, in Coq.QArith.QArith_base]

y:19 [binder, in Coq.Relations.Operators_Properties]

y:19 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:19 [binder, in Coq.Logic.Eqdep_dec]

y:19 [binder, in Coq.Sets.Constructive_sets]

y:19 [binder, in Coq.QArith.Qcabs]

y:19 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]

y:19 [binder, in Coq.FSets.FMapFacts]

y:19 [binder, in Coq.Wellfounded.Lexicographic_Product]

y:19 [binder, in Coq.ZArith.Int]

y:19 [binder, in Coq.micromega.QMicromega]

y:19 [binder, in Coq.Structures.OrderedTypeAlt]

y:19 [binder, in Coq.Classes.CRelationClasses]

y:19 [binder, in Coq.micromega.ZifySint63]

y:19 [binder, in Coq.Reals.Rbasic_fun]

y:19 [binder, in Coq.Classes.SetoidClass]

y:19 [binder, in Coq.Bool.BoolEq]

y:19 [binder, in Coq.Logic.ProofIrrelevanceFacts]

y:19 [binder, in Coq.Reals.RList]

y:19 [binder, in Coq.Logic.Diaconescu]

Y:19 [binder, in Coq.Sets.Classical_sets]

y:19 [binder, in Coq.Program.Basics]

y:19 [binder, in Coq.micromega.ZifyInst]

y:19 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:19 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:19 [binder, in Coq.micromega.ZMicromega]

y:19 [binder, in Coq.Floats.FloatAxioms]

y:19 [binder, in Coq.Relations.Relation_Operators]

y:19 [binder, in Coq.Numbers.Cyclic.Int31.Ring31]

y:19 [binder, in Coq.Structures.OrdersFacts]

y:190 [binder, in Coq.micromega.RingMicromega]

y:190 [binder, in Coq.omega.OmegaLemmas]

y:191 [binder, in Coq.Reals.Rpower]

y:191 [binder, in Coq.Reals.Rtopology]

y:191 [binder, in Coq.Reals.Ranalysis5]

y:191 [binder, in Coq.Init.Logic]

y:191 [binder, in Coq.QArith.QArith_base]

y:191 [binder, in Coq.Lists.SetoidList]

y:191 [binder, in Coq.FSets.FSetCompat]

y:192 [binder, in Coq.FSets.FSetBridge]

y:192 [binder, in Coq.Reals.PSeries_reg]

y:193 [binder, in Coq.ssr.ssrfun]

y:193 [binder, in Coq.Reals.Rtopology]

y:194 [binder, in Coq.Reals.Rpower]

y:194 [binder, in Coq.Bool.Bool]

y:194 [binder, in Coq.omega.OmegaLemmas]

y:194 [binder, in Coq.Structures.GenericMinMax]

y:194 [binder, in Coq.Reals.Ranalysis5]

y:196 [binder, in Coq.FSets.FSetBridge]

y:196 [binder, in Coq.FSets.FMapAVL]

y:197 [binder, in Coq.MSets.MSetList]

y:197 [binder, in Coq.Reals.Rpower]

y:197 [binder, in Coq.Reals.Ranalysis5]

y:197 [binder, in Coq.FSets.FSetCompat]

y:198 [binder, in Coq.FSets.FSetBridge]

y:198 [binder, in Coq.FSets.FMapPositive]

y:199 [binder, in Coq.FSets.FMapAVL]

y:199 [binder, in Coq.omega.OmegaLemmas]

y:199 [binder, in Coq.Structures.GenericMinMax]

y:199 [binder, in Coq.Reals.Ranalysis5]

y:199 [binder, in Coq.QArith.QArith_base]

y:2 [binder, in Coq.Reals.Rderiv]

y:2 [binder, in Coq.micromega.Ztac]

y:2 [binder, in Coq.Structures.DecidableTypeEx]

y:2 [binder, in Coq.Reals.Rminmax]

y:2 [binder, in Coq.Structures.OrdersEx]

y:2 [binder, in Coq.PArith.BinPos]

y:2 [binder, in Coq.ZArith.BinInt]

y:2 [binder, in Coq.ZArith.Zmax]

y:2 [binder, in Coq.Numbers.NatInt.NZBase]

y:2 [binder, in Coq.ZArith.Zmin]

y:2 [binder, in Coq.FSets.FMapFacts]

y:2 [binder, in Coq.Reals.Rsqrt_def]

y:2 [binder, in Coq.MSets.MSetFacts]

y:2 [binder, in Coq.QArith.Qfield]

y:2 [binder, in Coq.NArith.BinNat]

y:2 [binder, in Coq.Reals.Raxioms]

y:2 [binder, in Coq.micromega.ZifyNat]

y:2 [binder, in Coq.ZArith.Zbool]

y:2 [binder, in Coq.Reals.Rbasic_fun]

y:2 [binder, in Coq.NArith.NArith]

y:2 [binder, in Coq.micromega.Fourier_util]

y:2 [binder, in Coq.Numbers.Cyclic.Int63.Ring63]

y:2 [binder, in Coq.Unicode.Utf8_core]

y:2 [binder, in Coq.omega.PreOmega]

y:2 [binder, in Coq.Numbers.Integer.Binary.ZBinary]

y:2 [binder, in Coq.micromega.ZifyN]

y:2 [binder, in Coq.FSets.FSetFacts]

y:2 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:2 [binder, in Coq.Numbers.Cyclic.Int31.Ring31]

y:2 [binder, in Coq.Structures.OrdersFacts]

y:2 [binder, in Coq.Reals.Cos_plus]

y:20 [binder, in Coq.Structures.Orders]

y:20 [binder, in Coq.Program.Wf]

y:20 [binder, in Coq.QArith.Qcanon]

y:20 [binder, in Coq.Structures.OrdersLists]

y:20 [binder, in Coq.Structures.OrdersEx]

y:20 [binder, in Coq.Reals.R_sqrt]

y:20 [binder, in Coq.Reals.Exp_prop]

y:20 [binder, in Coq.Structures.OrdersAlt]

y:20 [binder, in Coq.Reals.Rsqrt_def]

y:20 [binder, in Coq.QArith.Qreals]

y:20 [binder, in Coq.Reals.Abstract.ConstructiveAbs]

y:20 [binder, in Coq.omega.OmegaLemmas]

y:20 [binder, in Coq.Structures.OrderedTypeEx]

y:20 [binder, in Coq.Structures.Equalities]

y:20 [binder, in Coq.Strings.Ascii]

y:20 [binder, in Coq.micromega.ZifyUint63]

y:20 [binder, in Coq.Lists.ListSet]

y:20 [binder, in Coq.Sets.Permut]

y:20 [binder, in Coq.Sets.Powerset_facts]

y:20 [binder, in Coq.Sets.Powerset_Classical_facts]

y:20 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:20 [binder, in Coq.Sets.Multiset]

y:20 [binder, in Coq.Classes.DecidableClass]

y:20 [binder, in Coq.Sets.Image]

y:20 [binder, in Coq.Sorting.Heap]

y:20 [binder, in Coq.FSets.FSetCompat]

y:200 [binder, in Coq.ssr.ssrfun]

y:200 [binder, in Coq.Reals.Rpower]

y:201 [binder, in Coq.FSets.FMapFullAVL]

y:201 [binder, in Coq.Bool.Bool]

y:201 [binder, in Coq.Reals.Ranalysis5]

y:201 [binder, in Coq.Lists.SetoidList]

y:202 [binder, in Coq.QArith.QArith_base]

y:203 [binder, in Coq.Reals.Rfunctions]

y:203 [binder, in Coq.Reals.Rtopology]

y:203 [binder, in Coq.Reals.PSeries_reg]

y:203 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:203 [binder, in Coq.FSets.FSetCompat]

y:204 [binder, in Coq.Logic.EqdepFacts]

y:204 [binder, in Coq.MSets.MSetList]

y:204 [binder, in Coq.Reals.Ranalysis5]

y:204 [binder, in Coq.micromega.ZMicromega]

y:204 [binder, in Coq.Lists.SetoidList]

y:205 [binder, in Coq.Reals.Rfunctions]

y:205 [binder, in Coq.FSets.FMapWeakList]

y:205 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:206 [binder, in Coq.Logic.ChoiceFacts]

y:206 [binder, in Coq.omega.OmegaLemmas]

y:206 [binder, in Coq.Structures.GenericMinMax]

y:206 [binder, in Coq.Reals.PSeries_reg]

y:207 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:207 [binder, in Coq.Reals.Rfunctions]

y:207 [binder, in Coq.ssr.ssrfun]

y:207 [binder, in Coq.MSets.MSetPositive]

y:207 [binder, in Coq.Reals.Ranalysis5]

y:207 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:207 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:208 [binder, in Coq.Logic.ChoiceFacts]

y:208 [binder, in Coq.Reals.Rpower]

y:208 [binder, in Coq.MSets.MSetRBT]

y:208 [binder, in Coq.Reals.Rtopology]

y:208 [binder, in Coq.Reals.PSeries_reg]

y:208 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:209 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:209 [binder, in Coq.Reals.Rfunctions]

y:209 [binder, in Coq.FSets.FMapWeakList]

y:209 [binder, in Coq.Reals.Ranalysis5]

y:209 [binder, in Coq.setoid_ring.Ring_theory]

y:209 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:209 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:21 [binder, in Coq.Program.Wf]

y:21 [binder, in Coq.Relations.Operators_Properties]

y:21 [binder, in Coq.Logic.Eqdep_dec]

y:21 [binder, in Coq.Sets.Constructive_sets]

y:21 [binder, in Coq.Classes.RelationClasses]

y:21 [binder, in Coq.Arith.Wf_nat]

y:21 [binder, in Coq.Logic.JMeq]

y:21 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]

y:21 [binder, in Coq.QArith.Qabs]

y:21 [binder, in Coq.Reals.Rdefinitions]

y:21 [binder, in Coq.micromega.QMicromega]

y:21 [binder, in Coq.Sets.Partial_Order]

y:21 [binder, in Coq.Structures.OrderedTypeAlt]

y:21 [binder, in Coq.micromega.ZifySint63]

y:21 [binder, in Coq.Structures.OrderedType]

y:21 [binder, in Coq.Reals.Rbasic_fun]

y:21 [binder, in Coq.Classes.SetoidDec]

y:21 [binder, in Coq.Strings.Byte]

y:21 [binder, in Coq.Lists.ListSet]

y:21 [binder, in Coq.Reals.RList]

y:21 [binder, in Coq.Logic.Diaconescu]

Y:21 [binder, in Coq.Sets.Classical_sets]

y:21 [binder, in Coq.Structures.OrdersTac]

y:21 [binder, in Coq.micromega.ZifyInst]

y:21 [binder, in Coq.micromega.ZMicromega]

y:21 [binder, in Coq.micromega.ZCoeff]

y:21 [binder, in Coq.Structures.OrdersFacts]

y:210 [binder, in Coq.Reals.Rpower]

y:210 [binder, in Coq.MSets.MSetPositive]

y:210 [binder, in Coq.Reals.Rtopology]

y:210 [binder, in Coq.Reals.PSeries_reg]

y:211 [binder, in Coq.Structures.GenericMinMax]

y:211 [binder, in Coq.Reals.PSeries_reg]

y:211 [binder, in Coq.Reals.Ranalysis5]

y:211 [binder, in Coq.setoid_ring.Ring_theory]

y:211 [binder, in Coq.FSets.FMapList]

y:211 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:211 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:212 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:212 [binder, in Coq.Reals.Rfunctions]

y:212 [binder, in Coq.MSets.MSetPositive]

y:212 [binder, in Coq.Reals.Rtopology]

y:212 [binder, in Coq.setoid_ring.Ncring]

y:213 [binder, in Coq.ssr.ssrfun]

y:213 [binder, in Coq.MSets.MSetRBT]

y:213 [binder, in Coq.Reals.PSeries_reg]

y:213 [binder, in Coq.Reals.Ranalysis5]

y:213 [binder, in Coq.setoid_ring.Ring_theory]

y:213 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:214 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:214 [binder, in Coq.Reals.Ranalysis1]

y:214 [binder, in Coq.Logic.ChoiceFacts]

y:214 [binder, in Coq.Reals.Rtopology]

y:214 [binder, in Coq.FSets.FMapWeakList]

y:214 [binder, in Coq.setoid_ring.Ncring]

y:215 [binder, in Coq.Reals.Ranalysis1]

y:215 [binder, in Coq.ssr.ssrfun]

y:215 [binder, in Coq.Reals.Rtopology]

y:215 [binder, in Coq.Reals.Ranalysis5]

y:215 [binder, in Coq.setoid_ring.Ring_theory]

y:215 [binder, in Coq.FSets.FMapList]

y:215 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:215 [binder, in Coq.Lists.SetoidList]

y:216 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:216 [binder, in Coq.Reals.Ranalysis1]

y:216 [binder, in Coq.Logic.ChoiceFacts]

y:216 [binder, in Coq.Reals.Rtopology]

y:216 [binder, in Coq.Structures.GenericMinMax]

y:216 [binder, in Coq.setoid_ring.Ncring]

y:217 [binder, in Coq.Reals.Ranalysis1]

y:217 [binder, in Coq.ssr.ssrfun]

y:217 [binder, in Coq.Reals.Ranalysis5]

y:217 [binder, in Coq.setoid_ring.Ring_theory]

y:218 [binder, in Coq.Reals.Ranalysis1]

y:218 [binder, in Coq.Logic.ChoiceFacts]

y:218 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:218 [binder, in Coq.Lists.SetoidList]

y:219 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:219 [binder, in Coq.Reals.Ranalysis1]

y:219 [binder, in Coq.ssr.ssrfun]

y:219 [binder, in Coq.FSets.FMapWeakList]

y:219 [binder, in Coq.Structures.GenericMinMax]

y:219 [binder, in Coq.Reals.Ranalysis5]

y:22 [binder, in Coq.Structures.Orders]

y:22 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:22 [binder, in Coq.QArith.Qcanon]

y:22 [binder, in Coq.QArith.Qcabs]

y:22 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]

y:22 [binder, in Coq.FSets.FMapFacts]

y:22 [binder, in Coq.Structures.OrdersAlt]

y:22 [binder, in Coq.Logic.Hurkens]

y:22 [binder, in Coq.Arith.Cantor]

y:22 [binder, in Coq.Sets.Cpo]

y:22 [binder, in Coq.Structures.OrderedTypeEx]

y:22 [binder, in Coq.ZArith.Int]

y:22 [binder, in Coq.Structures.Equalities]

y:22 [binder, in Coq.Structures.GenericMinMax]

y:22 [binder, in Coq.Reals.Rlimit]

y:22 [binder, in Coq.micromega.ZifyUint63]

y:22 [binder, in Coq.Sets.Powerset_facts]

Y:22 [binder, in Coq.Sets.Powerset_Classical_facts]

y:22 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:22 [binder, in Coq.Classes.DecidableClass]

y:22 [binder, in Coq.Reals.R_sqr]

y:22 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:22 [binder, in Coq.Floats.FloatAxioms]

y:22 [binder, in Coq.Reals.Cos_rel]

Y:22 [binder, in Coq.Sets.Infinite_sets]

y:220 [binder, in Coq.setoid_ring.Ring_theory]

y:220 [binder, in Coq.FSets.FMapList]

y:221 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:221 [binder, in Coq.Reals.Ranalysis1]

y:221 [binder, in Coq.Logic.ChoiceFacts]

y:221 [binder, in Coq.Reals.Ranalysis5]

y:221 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:222 [binder, in Coq.Structures.GenericMinMax]

y:223 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:223 [binder, in Coq.Reals.Ranalysis1]

y:223 [binder, in Coq.Reals.Ranalysis5]

y:224 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:224 [binder, in Coq.setoid_ring.Ncring]

y:224 [binder, in Coq.Lists.SetoidList]

y:225 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:225 [binder, in Coq.Reals.Ranalysis1]

y:225 [binder, in Coq.ssr.ssrfun]

y:225 [binder, in Coq.Structures.GenericMinMax]

y:226 [binder, in Coq.Logic.ChoiceFacts]

y:226 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:227 [binder, in Coq.Reals.Ranalysis1]

y:227 [binder, in Coq.ssr.ssrfun]

y:227 [binder, in Coq.Reals.Ranalysis5]

y:227 [binder, in Coq.setoid_ring.Ncring]

y:227 [binder, in Coq.Lists.SetoidList]

y:228 [binder, in Coq.Reals.Ranalysis1]

y:228 [binder, in Coq.Logic.ChoiceFacts]

y:228 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:229 [binder, in Coq.Reals.Ranalysis1]

y:229 [binder, in Coq.ssr.ssrfun]

y:23 [binder, in Coq.Relations.Operators_Properties]

y:23 [binder, in Coq.Logic.Eqdep_dec]

y:23 [binder, in Coq.Structures.OrdersLists]

y:23 [binder, in Coq.ZArith.BinIntDef]

y:23 [binder, in Coq.Reals.Rtrigo_reg]

Y:23 [binder, in Coq.Sets.Finite_sets_facts]

y:23 [binder, in Coq.Logic.EqdepFacts]

y:23 [binder, in Coq.Reals.R_sqrt]

y:23 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:23 [binder, in Coq.Reals.Abstract.ConstructivePower]

y:23 [binder, in Coq.Wellfounded.Lexicographic_Product]

y:23 [binder, in Coq.Init.Wf]

y:23 [binder, in Coq.QArith.Qreals]

y:23 [binder, in Coq.QArith.Qabs]

y:23 [binder, in Coq.Reals.Abstract.ConstructiveAbs]

y:23 [binder, in Coq.omega.OmegaLemmas]

y:23 [binder, in Coq.Classes.CMorphisms]

y:23 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y:23 [binder, in Coq.micromega.QMicromega]

y:23 [binder, in Coq.Structures.OrderedTypeAlt]

y:23 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]

y:23 [binder, in Coq.Reals.Rbasic_fun]

y:23 [binder, in Coq.Bool.BoolEq]

y:23 [binder, in Coq.Lists.ListSet]

y:23 [binder, in Coq.Sets.Multiset]

y:23 [binder, in Coq.Logic.Diaconescu]

y:23 [binder, in Coq.micromega.ZifyInst]

y:23 [binder, in Coq.QArith.Qpower]

y:23 [binder, in Coq.micromega.ZCoeff]

y:23 [binder, in Coq.Structures.OrdersFacts]

y:230 [binder, in Coq.Reals.Ranalysis1]

y:230 [binder, in Coq.Logic.ChoiceFacts]

y:230 [binder, in Coq.Lists.SetoidList]

y:231 [binder, in Coq.Reals.Ranalysis1]

y:231 [binder, in Coq.ssr.ssrfun]

y:231 [binder, in Coq.Reals.Ranalysis5]

y:231 [binder, in Coq.micromega.ZMicromega]

y:232 [binder, in Coq.Logic.ChoiceFacts]

y:233 [binder, in Coq.ssr.ssrfun]

y:234 [binder, in Coq.MSets.MSetProperties]

y:234 [binder, in Coq.ssr.ssrfun]

y:234 [binder, in Coq.Reals.Ranalysis5]

y:234 [binder, in Coq.FSets.FSetProperties]

y:235 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:235 [binder, in Coq.Logic.EqdepFacts]

y:235 [binder, in Coq.FSets.FSetPositive]

y:235 [binder, in Coq.setoid_ring.Ring_theory]

y:236 [binder, in Coq.MSets.MSetProperties]

y:236 [binder, in Coq.Lists.List]

y:236 [binder, in Coq.Logic.ChoiceFacts]

y:236 [binder, in Coq.FSets.FMapFullAVL]

y:236 [binder, in Coq.MSets.MSetRBT]

y:236 [binder, in Coq.FSets.FSetProperties]

y:237 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:237 [binder, in Coq.Logic.EqdepFacts]

y:237 [binder, in Coq.Reals.Ranalysis5]

y:237 [binder, in Coq.setoid_ring.Ring_theory]

y:237 [binder, in Coq.QArith.QArith_base]

y:237 [binder, in Coq.Lists.SetoidList]

y:238 [binder, in Coq.Logic.ChoiceFacts]

y:239 [binder, in Coq.FSets.FSetPositive]

y:239 [binder, in Coq.QArith.QArith_base]

y:24 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:24 [binder, in Coq.QArith.Qcabs]

y:24 [binder, in Coq.Structures.OrdersAlt]

y:24 [binder, in Coq.Reals.Rsqrt_def]

y:24 [binder, in Coq.Arith.Cantor]

y:24 [binder, in Coq.Structures.OrderedTypeEx]

y:24 [binder, in Coq.Classes.EquivDec]

y:24 [binder, in Coq.Structures.Equalities]

y:24 [binder, in Coq.Structures.GenericMinMax]

y:24 [binder, in Coq.micromega.ZifyUint63]

y:24 [binder, in Coq.Sets.Permut]

y:24 [binder, in Coq.Logic.ClassicalDescription]

y:24 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:24 [binder, in Coq.Reals.RList]

y:24 [binder, in Coq.Classes.DecidableClass]

y:24 [binder, in Coq.Sets.Image]

y:24 [binder, in Coq.Structures.OrdersTac]

y:24 [binder, in Coq.Reals.R_sqr]

y:24 [binder, in Coq.micromega.ZMicromega]

y:240 [binder, in Coq.Logic.ChoiceFacts]

y:240 [binder, in Coq.Reals.Ranalysis5]

y:240 [binder, in Coq.ZArith.Znat]

y:240 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:241 [binder, in Coq.ssr.ssrfun]

y:242 [binder, in Coq.MSets.MSetProperties]

y:242 [binder, in Coq.Logic.ChoiceFacts]

y:242 [binder, in Coq.FSets.FSetPositive]

y:242 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:242 [binder, in Coq.FSets.FSetProperties]

y:243 [binder, in Coq.ssr.ssrfun]

y:243 [binder, in Coq.Structures.GenericMinMax]

y:243 [binder, in Coq.QArith.QArith_base]

y:244 [binder, in Coq.MSets.MSetProperties]

y:244 [binder, in Coq.Logic.ChoiceFacts]

y:244 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:244 [binder, in Coq.FSets.FSetProperties]

y:245 [binder, in Coq.Logic.ChoiceFacts]

y:245 [binder, in Coq.ssr.ssrfun]

y:245 [binder, in Coq.FSets.FSetPositive]

y:245 [binder, in Coq.MSets.MSetRBT]

y:245 [binder, in Coq.MSets.MSetGenTree]

y:245 [binder, in Coq.Structures.GenericMinMax]

y:245 [binder, in Coq.QArith.QArith_base]

y:246 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:247 [binder, in Coq.Logic.ChoiceFacts]

y:247 [binder, in Coq.ssr.ssrfun]

y:247 [binder, in Coq.FSets.FSetPositive]

y:247 [binder, in Coq.QArith.QArith_base]

y:248 [binder, in Coq.Logic.ChoiceFacts]

y:248 [binder, in Coq.Reals.Rtopology]

y:249 [binder, in Coq.Logic.EqdepFacts]

y:249 [binder, in Coq.ssr.ssrfun]

y:249 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:249 [binder, in Coq.QArith.QArith_base]

y:25 [binder, in Coq.Program.Wf]

y:25 [binder, in Coq.Relations.Operators_Properties]

y:25 [binder, in Coq.Reals.Rtrigo_reg]

y:25 [binder, in Coq.Reals.MVT]

y:25 [binder, in Coq.Reals.R_sqrt]

y:25 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:25 [binder, in Coq.Arith.Wf_nat]

y:25 [binder, in Coq.Logic.JMeq]

y:25 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]

y:25 [binder, in Coq.Logic.ChoiceFacts]

y:25 [binder, in Coq.Wellfounded.Lexicographic_Product]

y:25 [binder, in Coq.QArith.Qabs]

y:25 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y:25 [binder, in Coq.micromega.QMicromega]

y:25 [binder, in Coq.Structures.OrderedTypeAlt]

y:25 [binder, in Coq.micromega.ZifySint63]

y:25 [binder, in Coq.Structures.OrderedType]

y:25 [binder, in Coq.Reals.Rbasic_fun]

y:25 [binder, in Coq.Reals.Rlimit]

y:25 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:25 [binder, in Coq.micromega.ZCoeff]

y:25 [binder, in Coq.QArith.Qreduction]

y:25 [binder, in Coq.Reals.Cos_rel]

y:25 [binder, in Coq.Structures.OrdersFacts]

y:250 [binder, in Coq.Logic.ChoiceFacts]

y:250 [binder, in Coq.ssr.ssrfun]

y:250 [binder, in Coq.Reals.Ranalysis5]

y:251 [binder, in Coq.FSets.FSetPositive]

y:251 [binder, in Coq.Reals.Rtopology]

y:252 [binder, in Coq.Logic.ChoiceFacts]

y:252 [binder, in Coq.MSets.MSetGenTree]

y:253 [binder, in Coq.Lists.List]

y:253 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:253 [binder, in Coq.QArith.QArith_base]

y:253 [binder, in Coq.Lists.SetoidList]

y:254 [binder, in Coq.MSets.MSetProperties]

y:254 [binder, in Coq.FSets.FSetInterface]

y:254 [binder, in Coq.FSets.FSetPositive]

y:254 [binder, in Coq.MSets.MSetRBT]

y:254 [binder, in Coq.setoid_ring.Ring_theory]

y:254 [binder, in Coq.FSets.FSetProperties]

y:254 [binder, in Coq.Lists.SetoidList]

y:255 [binder, in Coq.Reals.RIneq]

y:255 [binder, in Coq.Init.Logic]

y:255 [binder, in Coq.Lists.SetoidList]

y:256 [binder, in Coq.Lists.List]

y:256 [binder, in Coq.Logic.ChoiceFacts]

y:256 [binder, in Coq.Reals.Rtopology]

y:256 [binder, in Coq.Lists.SetoidList]

y:257 [binder, in Coq.Logic.EqdepFacts]

y:257 [binder, in Coq.MSets.MSetProperties]

y:257 [binder, in Coq.Sorting.Permutation]

y:257 [binder, in Coq.FSets.FSetPositive]

y:257 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:257 [binder, in Coq.FSets.FSetProperties]

y:258 [binder, in Coq.Logic.ChoiceFacts]

y:258 [binder, in Coq.FSets.FSetInterface]

y:258 [binder, in Coq.Reals.Ratan]

y:258 [binder, in Coq.setoid_ring.Ring_theory]

y:259 [binder, in Coq.Lists.List]

y:259 [binder, in Coq.FSets.FMapFacts]

y:259 [binder, in Coq.FSets.FSetPositive]

y:259 [binder, in Coq.Reals.Rtopology]

y:259 [binder, in Coq.Init.Logic]

y:259 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:26 [binder, in Coq.Structures.Orders]

y:26 [binder, in Coq.Program.Wf]

y:26 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:26 [binder, in Coq.setoid_ring.Ncring_initial]

y:26 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:26 [binder, in Coq.Structures.OrdersEx]

y:26 [binder, in Coq.QArith.Qcabs]

y:26 [binder, in Coq.Classes.RelationClasses]

y:26 [binder, in Coq.Reals.MVT]

y:26 [binder, in Coq.Arith.Cantor]

y:26 [binder, in Coq.Reals.Rdefinitions]

y:26 [binder, in Coq.Sets.Cpo]

y:26 [binder, in Coq.Arith.PeanoNat]

y:26 [binder, in Coq.omega.OmegaLemmas]

y:26 [binder, in Coq.Structures.OrderedTypeEx]

y:26 [binder, in Coq.Structures.Equalities]

y:26 [binder, in Coq.Bool.BoolEq]

y:26 [binder, in Coq.Classes.SetoidDec]

y:26 [binder, in Coq.Structures.GenericMinMax]

y:26 [binder, in Coq.micromega.ZifyUint63]

y:26 [binder, in Coq.Reals.PSeries_reg]

y:26 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:26 [binder, in Coq.Classes.DecidableClass]

y:26 [binder, in Coq.Reals.R_sqr]

y:26 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:26 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:26 [binder, in Coq.Relations.Relation_Operators]

y:260 [binder, in Coq.Logic.ClassicalFacts]

y:261 [binder, in Coq.Logic.ChoiceFacts]

y:261 [binder, in Coq.FSets.FSetPositive]

y:261 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:262 [binder, in Coq.MSets.MSetRBT]

y:263 [binder, in Coq.Init.Logic]

y:263 [binder, in Coq.QArith.QArith_base]

y:264 [binder, in Coq.MSets.MSetList]

y:264 [binder, in Coq.Reals.Rtopology]

y:264 [binder, in Coq.setoid_ring.Ring_theory]

y:264 [binder, in Coq.Lists.SetoidList]

y:265 [binder, in Coq.Logic.EqdepFacts]

y:265 [binder, in Coq.setoid_ring.Ncring_tac]

y:265 [binder, in Coq.ssr.ssrfun]

y:266 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:266 [binder, in Coq.QArith.QArith_base]

y:267 [binder, in Coq.MSets.MSetList]

y:267 [binder, in Coq.Reals.Rtopology]

y:267 [binder, in Coq.setoid_ring.Ring_theory]

y:267 [binder, in Coq.Init.Logic]

y:268 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:268 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:269 [binder, in Coq.QArith.QArith_base]

y:27 [binder, in Coq.Relations.Operators_Properties]

y:27 [binder, in Coq.Sets.Constructive_sets]

y:27 [binder, in Coq.Reals.R_sqrt]

y:27 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:27 [binder, in Coq.Structures.OrdersAlt]

y:27 [binder, in Coq.ZArith.Wf_Z]

y:27 [binder, in Coq.setoid_ring.InitialRing]

y:27 [binder, in Coq.QArith.Qabs]

y:27 [binder, in Coq.Structures.OrderedTypeAlt]

y:27 [binder, in Coq.Classes.CRelationClasses]

y:27 [binder, in Coq.micromega.ZifySint63]

y:27 [binder, in Coq.Reals.Rbasic_fun]

y:27 [binder, in Coq.Logic.HLevels]

y:27 [binder, in Coq.Lists.ListSet]

y:27 [binder, in Coq.Sets.Permut]

y:27 [binder, in Coq.Reals.RList]

y:27 [binder, in Coq.Sets.Image]

y:27 [binder, in Coq.Structures.OrdersTac]

y:27 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:27 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:27 [binder, in Coq.micromega.ZCoeff]

y:27 [binder, in Coq.Floats.FloatAxioms]

y:27 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:27 [binder, in Coq.Structures.OrdersFacts]

y:270 [binder, in Coq.setoid_ring.Field_theory]

y:270 [binder, in Coq.ssr.ssrfun]

y:270 [binder, in Coq.MSets.MSetRBT]

y:270 [binder, in Coq.setoid_ring.Ring_theory]

y:270 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:271 [binder, in Coq.Logic.ChoiceFacts]

y:271 [binder, in Coq.Sorting.Permutation]

y:271 [binder, in Coq.Init.Logic]

y:272 [binder, in Coq.Logic.EqdepFacts]

y:272 [binder, in Coq.QArith.QArith_base]

y:273 [binder, in Coq.Logic.ChoiceFacts]

y:273 [binder, in Coq.setoid_ring.Field_theory]

y:273 [binder, in Coq.ssr.ssrfun]

y:273 [binder, in Coq.MSets.MSetGenTree]

y:273 [binder, in Coq.setoid_ring.Ring_theory]

y:274 [binder, in Coq.QArith.QArith_base]

y:274 [binder, in Coq.Lists.SetoidList]

y:275 [binder, in Coq.MSets.MSetRBT]

y:275 [binder, in Coq.Init.Logic]

y:276 [binder, in Coq.setoid_ring.Field_theory]

y:276 [binder, in Coq.setoid_ring.Ring_theory]

y:276 [binder, in Coq.micromega.ZMicromega]

y:276 [binder, in Coq.QArith.QArith_base]

y:278 [binder, in Coq.ssr.ssrfun]

y:278 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:278 [binder, in Coq.QArith.QArith_base]

y:279 [binder, in Coq.MSets.MSetPositive]

y:279 [binder, in Coq.setoid_ring.Ring_theory]

y:28 [binder, in Coq.setoid_ring.Ncring_initial]

y:28 [binder, in Coq.ZArith.BinIntDef]

y:28 [binder, in Coq.Reals.Rfunctions]

y:28 [binder, in Coq.Lists.List]

y:28 [binder, in Coq.Reals.Rsqrt_def]

y:28 [binder, in Coq.Wellfounded.Lexicographic_Product]

y:28 [binder, in Coq.Arith.PeanoNat]

y:28 [binder, in Coq.Structures.Equalities]

y:28 [binder, in Coq.Reals.Rtopology]

y:28 [binder, in Coq.Structures.OrderedType]

y:28 [binder, in Coq.Bool.BoolEq]

y:28 [binder, in Coq.Structures.GenericMinMax]

y:28 [binder, in Coq.Reals.Rlimit]

y:28 [binder, in Coq.micromega.ZifyUint63]

y:28 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:28 [binder, in Coq.Classes.DecidableClass]

y:28 [binder, in Coq.Reals.R_sqr]

y:28 [binder, in Coq.ZArith.Znumtheory]

y:28 [binder, in Coq.Relations.Relation_Definitions]

y:28 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

Y:28 [binder, in Coq.Sets.Infinite_sets]

y:280 [binder, in Coq.Lists.List]

y:280 [binder, in Coq.Strings.Byte]

y:280 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:280 [binder, in Coq.QArith.QArith_base]

y:281 [binder, in Coq.Logic.ChoiceFacts]

y:281 [binder, in Coq.ssr.ssrfun]

y:282 [binder, in Coq.Reals.Ranalysis1]

y:282 [binder, in Coq.setoid_ring.Field_theory]

y:282 [binder, in Coq.Reals.Ratan]

y:282 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:282 [binder, in Coq.QArith.QArith_base]

y:283 [binder, in Coq.Reals.Ranalysis1]

y:283 [binder, in Coq.Lists.List]

y:283 [binder, in Coq.Logic.ChoiceFacts]

y:284 [binder, in Coq.Reals.Ranalysis1]

y:284 [binder, in Coq.QArith.QArith_base]

y:285 [binder, in Coq.Reals.Ranalysis1]

y:285 [binder, in Coq.MSets.MSetPositive]

y:286 [binder, in Coq.Reals.Ranalysis1]

y:286 [binder, in Coq.MSets.MSetRBT]

y:286 [binder, in Coq.Reals.Ranalysis5]

y:286 [binder, in Coq.setoid_ring.Ring_theory]

y:286 [binder, in Coq.micromega.ZMicromega]

y:287 [binder, in Coq.Reals.Ranalysis1]

y:288 [binder, in Coq.Reals.Ranalysis1]

y:288 [binder, in Coq.Reals.Rtopology]

y:288 [binder, in Coq.Reals.Ranalysis5]

y:288 [binder, in Coq.Init.Logic]

y:289 [binder, in Coq.Reals.Ranalysis1]

y:289 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:29 [binder, in Coq.Structures.Orders]

y:29 [binder, in Coq.Relations.Operators_Properties]

y:29 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:29 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:29 [binder, in Coq.Reals.Ranalysis4]

y:29 [binder, in Coq.micromega.RingMicromega]

y:29 [binder, in Coq.Reals.Rfunctions]

y:29 [binder, in Coq.Sets.Ensembles]

y:29 [binder, in Coq.Reals.R_sqrt]

y:29 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:29 [binder, in Coq.Arith.Wf_nat]

y:29 [binder, in Coq.Logic.JMeq]

y:29 [binder, in Coq.Wellfounded.Lexicographic_Product]

y:29 [binder, in Coq.Init.Wf]

y:29 [binder, in Coq.setoid_ring.InitialRing]

y:29 [binder, in Coq.Reals.Rdefinitions]

y:29 [binder, in Coq.Reals.Rpower]

y:29 [binder, in Coq.Program.Equality]

y:29 [binder, in Coq.omega.OmegaLemmas]

y:29 [binder, in Coq.Structures.OrderedTypeEx]

y:29 [binder, in Coq.micromega.QMicromega]

y:29 [binder, in Coq.Sets.Relations_2_facts]

y:29 [binder, in Coq.ZArith.ZArith_dec]

y:29 [binder, in Coq.Logic.ClassicalDescription]

y:29 [binder, in Coq.Sets.Image]

y:29 [binder, in Coq.Reals.Rgeom]

y:29 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:29 [binder, in Coq.Structures.OrdersFacts]

y:290 [binder, in Coq.Reals.Ranalysis1]

y:290 [binder, in Coq.Lists.List]

y:290 [binder, in Coq.Strings.Byte]

y:290 [binder, in Coq.Reals.Ranalysis5]

y:291 [binder, in Coq.Reals.Ranalysis1]

y:291 [binder, in Coq.Logic.ChoiceFacts]

y:291 [binder, in Coq.MSets.MSetPositive]

y:291 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:293 [binder, in Coq.MSets.MSetInterface]

y:293 [binder, in Coq.Logic.ChoiceFacts]

y:293 [binder, in Coq.Reals.Ranalysis5]

y:293 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:294 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:294 [binder, in Coq.Lists.List]

y:294 [binder, in Coq.Reals.Rtopology]

y:295 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:296 [binder, in Coq.MSets.MSetInterface]

y:296 [binder, in Coq.MSets.MSetPositive]

y:296 [binder, in Coq.Reals.Ranalysis5]

y:296 [binder, in Coq.QArith.QArith_base]

y:297 [binder, in Coq.MSets.MSetRBT]

y:297 [binder, in Coq.FSets.FMapPositive]

y:298 [binder, in Coq.Reals.Rtopology]

y:298 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:299 [binder, in Coq.Reals.Ranalysis5]

y:3 [binder, in Coq.Sorting.PermutEq]

y:3 [binder, in Coq.Logic.Eqdep_dec]

y:3 [binder, in Coq.Structures.OrdersLists]

y:3 [binder, in Coq.Arith.Bool_nat]

y:3 [binder, in Coq.QArith.Qreals]

y:3 [binder, in Coq.ZArith.Zwf]

y:3 [binder, in Coq.Lists.ListDec]

y:3 [binder, in Coq.Reals.Rpower]

y:3 [binder, in Coq.Structures.GenericMinMax]

y:3 [binder, in Coq.Lists.ListSet]

y:3 [binder, in Coq.Reals.PSeries_reg]

y:3 [binder, in Coq.micromega.RMicromega]

y:3 [binder, in Coq.Reals.R_sqr]

y:3 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:3 [binder, in Coq.Program.Utils]

y:30 [binder, in Coq.Logic.EqdepFacts]

y:30 [binder, in Coq.Reals.Rfunctions]

y:30 [binder, in Coq.Structures.OrdersAlt]

y:30 [binder, in Coq.QArith.Qabs]

y:30 [binder, in Coq.Arith.PeanoNat]

y:30 [binder, in Coq.Classes.CMorphisms]

y:30 [binder, in Coq.Classes.EquivDec]

y:30 [binder, in Coq.Sets.Uniset]

y:30 [binder, in Coq.Structures.OrderedTypeAlt]

y:30 [binder, in Coq.Reals.Rbasic_fun]

y:30 [binder, in Coq.Structures.GenericMinMax]

y:30 [binder, in Coq.micromega.ZifyUint63]

y:30 [binder, in Coq.Sets.Multiset]

y:30 [binder, in Coq.Classes.DecidableClass]

y:30 [binder, in Coq.Structures.OrdersTac]

y:30 [binder, in Coq.Reals.R_sqr]

y:30 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:30 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:30 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:30 [binder, in Coq.Floats.FloatAxioms]

y:300 [binder, in Coq.MSets.MSetInterface]

y:300 [binder, in Coq.QArith.QArith_base]

y:302 [binder, in Coq.Reals.Ranalysis1]

y:302 [binder, in Coq.MSets.MSetInterface]

y:302 [binder, in Coq.Lists.List]

y:302 [binder, in Coq.Reals.Ranalysis5]

y:302 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:303 [binder, in Coq.Reals.Ranalysis1]

y:304 [binder, in Coq.Reals.Ranalysis1]

y:304 [binder, in Coq.FSets.FSetBridge]

y:304 [binder, in Coq.Reals.Rtopology]

y:304 [binder, in Coq.QArith.QArith_base]

y:305 [binder, in Coq.Reals.Ranalysis5]

y:305 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:307 [binder, in Coq.MSets.MSetRBT]

y:307 [binder, in Coq.MSets.MSetPositive]

y:307 [binder, in Coq.QArith.QArith_base]

y:308 [binder, in Coq.MSets.MSetInterface]

y:308 [binder, in Coq.Logic.ChoiceFacts]

y:308 [binder, in Coq.Init.Logic]

y:309 [binder, in Coq.Reals.Ranalysis1]

y:31 [binder, in Coq.Program.Wf]

y:31 [binder, in Coq.Relations.Operators_Properties]

y:31 [binder, in Coq.setoid_ring.Ncring_initial]

y:31 [binder, in Coq.Reals.Ranalysis4]

y:31 [binder, in Coq.Reals.Rfunctions]

y:31 [binder, in Coq.Reals.R_sqrt]

y:31 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:31 [binder, in Coq.ZArith.Wf_Z]

y:31 [binder, in Coq.Reals.Rdefinitions]

y:31 [binder, in Coq.Sets.Cpo]

y:31 [binder, in Coq.Structures.OrderedTypeEx]

y:31 [binder, in Coq.micromega.QMicromega]

y:31 [binder, in Coq.Structures.Equalities]

y:31 [binder, in Coq.Structures.OrderedType]

y:31 [binder, in Coq.ZArith.ZArith_dec]

y:31 [binder, in Coq.Classes.SetoidDec]

y:31 [binder, in Coq.Reals.Rlimit]

y:31 [binder, in Coq.Numbers.NatInt.NZOrder]

y:31 [binder, in Coq.Logic.HLevels]

y:31 [binder, in Coq.Sets.Permut]

y:31 [binder, in Coq.Logic.ClassicalDescription]

y:31 [binder, in Coq.Sets.Image]

y:310 [binder, in Coq.Reals.Ranalysis1]

y:310 [binder, in Coq.Logic.ChoiceFacts]

y:310 [binder, in Coq.QArith.QArith_base]

y:311 [binder, in Coq.Reals.Ranalysis1]

y:311 [binder, in Coq.Arith.PeanoNat]

y:311 [binder, in Coq.Reals.Ratan]

y:312 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:313 [binder, in Coq.MSets.MSetRBT]

y:313 [binder, in Coq.MSets.MSetPositive]

y:313 [binder, in Coq.QArith.QArith_base]

y:314 [binder, in Coq.MSets.MSetInterface]

y:316 [binder, in Coq.MSets.MSetRBT]

y:316 [binder, in Coq.QArith.QArith_base]

y:317 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:319 [binder, in Coq.MSets.MSetPositive]

y:319 [binder, in Coq.Init.Logic]

y:32 [binder, in Coq.Structures.Orders]

y:32 [binder, in Coq.Program.Wf]

y:32 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:32 [binder, in Coq.Sets.Constructive_sets]

y:32 [binder, in Coq.micromega.RingMicromega]

y:32 [binder, in Coq.Reals.Rfunctions]

y:32 [binder, in Coq.Structures.OrdersAlt]

y:32 [binder, in Coq.Reals.Rsqrt_def]

y:32 [binder, in Coq.Classes.CEquivalence]

y:32 [binder, in Coq.Program.Equality]

y:32 [binder, in Coq.Arith.PeanoNat]

y:32 [binder, in Coq.omega.OmegaLemmas]

y:32 [binder, in Coq.Classes.CRelationClasses]

y:32 [binder, in Coq.Structures.GenericMinMax]

y:32 [binder, in Coq.Sets.Multiset]

y:32 [binder, in Coq.Classes.DecidableClass]

y:32 [binder, in Coq.NArith.BinNatDef]

y:32 [binder, in Coq.Reals.Rgeom]

y:32 [binder, in Coq.PArith.BinPosDef]

y:32 [binder, in Coq.Reals.R_sqr]

y:32 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:32 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

Y:32 [binder, in Coq.Sets.Infinite_sets]

y:32 [binder, in Coq.Relations.Relation_Operators]

y:32 [binder, in Coq.QArith.QArith_base]

y:32 [binder, in Coq.Structures.OrdersFacts]

y:32 [binder, in Coq.Classes.Equivalence]

y:320 [binder, in Coq.QArith.QArith_base]

y:322 [binder, in Coq.Reals.Rtopology]

y:322 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:323 [binder, in Coq.QArith.QArith_base]

y:324 [binder, in Coq.MSets.MSetRBT]

y:325 [binder, in Coq.Logic.ChoiceFacts]

y:326 [binder, in Coq.ssr.ssrbool]

y:326 [binder, in Coq.QArith.QArith_base]

y:327 [binder, in Coq.Logic.ChoiceFacts]

y:329 [binder, in Coq.QArith.QArith_base]

y:33 [binder, in Coq.Relations.Operators_Properties]

y:33 [binder, in Coq.setoid_ring.Ncring_initial]

y:33 [binder, in Coq.Reals.Ranalysis1]

y:33 [binder, in Coq.ZArith.BinIntDef]

y:33 [binder, in Coq.Reals.Ranalysis4]

y:33 [binder, in Coq.Reals.Rfunctions]

y:33 [binder, in Coq.Sets.Ensembles]

y:33 [binder, in Coq.Reals.R_sqrt]

y:33 [binder, in Coq.Arith.Wf_nat]

y:33 [binder, in Coq.Classes.Morphisms]

y:33 [binder, in Coq.Logic.JMeq]

y:33 [binder, in Coq.setoid_ring.InitialRing]

y:33 [binder, in Coq.Reals.Rpower]

y:33 [binder, in Coq.Sets.Cpo]

y:33 [binder, in Coq.Structures.OrderedTypeEx]

y:33 [binder, in Coq.micromega.QMicromega]

y:33 [binder, in Coq.Sets.Uniset]

y:33 [binder, in Coq.Structures.Equalities]

y:33 [binder, in Coq.Reals.Rbasic_fun]

y:33 [binder, in Coq.Logic.Berardi]

y:33 [binder, in Coq.setoid_ring.Ncring_polynom]

y:33 [binder, in Coq.Reals.Ranalysis5]

y:33 [binder, in Coq.Sets.Image]

y:33 [binder, in Coq.Structures.OrdersTac]

y:33 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:33 [binder, in Coq.micromega.ZMicromega]

y:33 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:33 [binder, in Coq.Relations.Relation_Operators]

y:330 [binder, in Coq.Reals.Rtopology]

y:330 [binder, in Coq.Reals.RIneq]

y:331 [binder, in Coq.ssr.ssrfun]

y:332 [binder, in Coq.Reals.Rtopology]

y:332 [binder, in Coq.QArith.QArith_base]

y:334 [binder, in Coq.ssr.ssrbool]

y:334 [binder, in Coq.Reals.Rtopology]

y:335 [binder, in Coq.MSets.MSetRBT]

y:335 [binder, in Coq.QArith.QArith_base]

y:336 [binder, in Coq.Reals.Rtopology]

y:336 [binder, in Coq.Init.Logic]

y:337 [binder, in Coq.Reals.Rtopology]

y:338 [binder, in Coq.ssr.ssrbool]

y:338 [binder, in Coq.QArith.QArith_base]

y:339 [binder, in Coq.MSets.MSetInterface]

y:339 [binder, in Coq.Lists.List]

y:34 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:34 [binder, in Coq.Logic.Eqdep_dec]

y:34 [binder, in Coq.Logic.EqdepFacts]

y:34 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:34 [binder, in Coq.Structures.OrdersAlt]

y:34 [binder, in Coq.Init.Wf]

y:34 [binder, in Coq.Reals.Rdefinitions]

y:34 [binder, in Coq.Reals.Abstract.ConstructiveAbs]

y:34 [binder, in Coq.Structures.OrderedType]

y:34 [binder, in Coq.Classes.SetoidDec]

y:34 [binder, in Coq.Numbers.NatInt.NZOrder]

y:34 [binder, in Coq.Lists.ListSet]

y:34 [binder, in Coq.Sets.Permut]

y:34 [binder, in Coq.NArith.BinNatDef]

y:34 [binder, in Coq.PArith.BinPosDef]

y:34 [binder, in Coq.Reals.R_sqr]

y:34 [binder, in Coq.Relations.Relation_Definitions]

y:34 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

Y:34 [binder, in Coq.Sets.Infinite_sets]

y:34 [binder, in Coq.QArith.QArith_base]

y:34 [binder, in Coq.Structures.OrdersFacts]

y:340 [binder, in Coq.ssr.ssrfun]

y:340 [binder, in Coq.Reals.Rtopology]

y:342 [binder, in Coq.Lists.List]

y:342 [binder, in Coq.Reals.Ranalysis5]

y:343 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:343 [binder, in Coq.MSets.MSetInterface]

y:343 [binder, in Coq.Reals.Rtopology]

y:343 [binder, in Coq.micromega.ZMicromega]

y:344 [binder, in Coq.Reals.Rtopology]

y:345 [binder, in Coq.ssr.ssrfun]

y:346 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:349 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:349 [binder, in Coq.ssr.ssrfun]

y:349 [binder, in Coq.QArith.QArith_base]

y:35 [binder, in Coq.Program.Wf]

y:35 [binder, in Coq.Sorting.PermutEq]

y:35 [binder, in Coq.Structures.OrdersEx]

Y:35 [binder, in Coq.Sets.Finite_sets_facts]

y:35 [binder, in Coq.FSets.FSetDecide]

y:35 [binder, in Coq.Reals.Ranalysis4]

y:35 [binder, in Coq.Reals.R_sqrt]

y:35 [binder, in Coq.ZArith.Wf_Z]

y:35 [binder, in Coq.Reals.Rsqrt_def]

y:35 [binder, in Coq.Logic.ChoiceFacts]

y:35 [binder, in Coq.MSets.MSetDecide]

y:35 [binder, in Coq.setoid_ring.InitialRing]

y:35 [binder, in Coq.Structures.DecidableType]

y:35 [binder, in Coq.Reals.Rpower]

y:35 [binder, in Coq.Structures.OrderedTypeEx]

y:35 [binder, in Coq.Reals.Rbasic_fun]

y:35 [binder, in Coq.Logic.Berardi]

y:35 [binder, in Coq.Logic.HLevels]

y:35 [binder, in Coq.Sets.Powerset_Classical_facts]

y:35 [binder, in Coq.Reals.Ranalysis5]

y:35 [binder, in Coq.ssr.ssrunder]

y:35 [binder, in Coq.Sets.Multiset]

y:35 [binder, in Coq.Sets.Image]

y:35 [binder, in Coq.Floats.FloatAxioms]

y:35 [binder, in Coq.Reals.ClassicalConstructiveReals]

y:350 [binder, in Coq.ssr.ssrbool]

y:352 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:352 [binder, in Coq.ssr.ssrbool]

y:352 [binder, in Coq.ssr.ssrfun]

y:352 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:353 [binder, in Coq.MSets.MSetInterface]

y:353 [binder, in Coq.QArith.QArith_base]

y:355 [binder, in Coq.MSets.MSetGenTree]

y:355 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:356 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:356 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:356 [binder, in Coq.Init.Logic]

y:357 [binder, in Coq.FSets.FMapWeakList]

y:357 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:357 [binder, in Coq.QArith.QArith_base]

y:358 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:358 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:359 [binder, in Coq.Lists.List]

y:359 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:36 [binder, in Coq.Structures.Orders]

y:36 [binder, in Coq.Program.Wf]

y:36 [binder, in Coq.Relations.Operators_Properties]

y:36 [binder, in Coq.QArith.Qcanon]

y:36 [binder, in Coq.Reals.Ranalysis1]

y:36 [binder, in Coq.Reals.Rtrigo1]

y:36 [binder, in Coq.Reals.Ranalysis4]

y:36 [binder, in Coq.micromega.RingMicromega]

y:36 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:36 [binder, in Coq.Structures.OrdersAlt]

y:36 [binder, in Coq.ZArith.Zeven]

y:36 [binder, in Coq.Reals.Rdefinitions]

y:36 [binder, in Coq.Reals.Abstract.ConstructiveAbs]

y:36 [binder, in Coq.omega.OmegaLemmas]

y:36 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y:36 [binder, in Coq.Classes.EquivDec]

y:36 [binder, in Coq.Reals.NewtonInt]

y:36 [binder, in Coq.ZArith.Zbool]

y:36 [binder, in Coq.setoid_ring.Ncring_polynom]

y:36 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:36 [binder, in Coq.Logic.Diaconescu]

y:36 [binder, in Coq.Sets.Image]

y:36 [binder, in Coq.Structures.OrdersTac]

y:36 [binder, in Coq.Reals.R_sqr]

y:36 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:36 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

Y:36 [binder, in Coq.Sets.Infinite_sets]

y:360 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:360 [binder, in Coq.Reals.Rtopology]

y:360 [binder, in Coq.Reals.Ranalysis5]

y:361 [binder, in Coq.ssr.ssrfun]

y:361 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:363 [binder, in Coq.Reals.Rtopology]

y:364 [binder, in Coq.Init.Logic]

y:364 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:366 [binder, in Coq.ssr.ssrfun]

y:366 [binder, in Coq.Reals.Rtopology]

y:366 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:367 [binder, in Coq.FSets.FSetPositive]

y:368 [binder, in Coq.Reals.Rtopology]

y:368 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:369 [binder, in Coq.Init.Specif]

y:369 [binder, in Coq.Init.Logic]

y:37 [binder, in Coq.Reals.R_sqrt]

y:37 [binder, in Coq.Logic.JMeq]

y:37 [binder, in Coq.setoid_ring.InitialRing]

y:37 [binder, in Coq.ZArith.Zeven]

y:37 [binder, in Coq.Structures.OrderedTypeEx]

y:37 [binder, in Coq.Reals.NewtonInt]

y:37 [binder, in Coq.Classes.CRelationClasses]

y:37 [binder, in Coq.Reals.Rtopology]

y:37 [binder, in Coq.Structures.OrderedType]

y:37 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]

y:37 [binder, in Coq.Reals.Rbasic_fun]

y:37 [binder, in Coq.Logic.Berardi]

y:37 [binder, in Coq.Numbers.NatInt.NZOrder]

y:37 [binder, in Coq.Sets.Permut]

y:37 [binder, in Coq.Reals.Ranalysis5]

y:37 [binder, in Coq.Sets.Image]

y:37 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:37 [binder, in Coq.micromega.ZMicromega]

y:37 [binder, in Coq.QArith.QArith_base]

y:37 [binder, in Coq.Structures.OrdersFacts]

y:370 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:372 [binder, in Coq.FSets.FMapList]

y:373 [binder, in Coq.MSets.MSetRBT]

y:375 [binder, in Coq.FSets.FSetPositive]

y:375 [binder, in Coq.Reals.Rtopology]

y:376 [binder, in Coq.Logic.ChoiceFacts]

y:376 [binder, in Coq.Init.Logic]

y:377 [binder, in Coq.Reals.Rtopology]

y:378 [binder, in Coq.Reals.Rtopology]

y:378 [binder, in Coq.Reals.Ranalysis5]

y:379 [binder, in Coq.ssr.ssrfun]

y:38 [binder, in Coq.Structures.Orders]

y:38 [binder, in Coq.QArith.Qcanon]

y:38 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:38 [binder, in Coq.Logic.Eqdep_dec]

Y:38 [binder, in Coq.Sets.Finite_sets_facts]

Y:38 [binder, in Coq.Sets.Constructive_sets]

y:38 [binder, in Coq.Reals.Ranalysis4]

y:38 [binder, in Coq.micromega.RingMicromega]

y:38 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:38 [binder, in Coq.Structures.OrdersAlt]

y:38 [binder, in Coq.Reals.Rsqrt_def]

y:38 [binder, in Coq.Init.Wf]

y:38 [binder, in Coq.Reals.Rdefinitions]

y:38 [binder, in Coq.Reals.Abstract.ConstructiveAbs]

y:38 [binder, in Coq.Program.Equality]

y:38 [binder, in Coq.omega.OmegaLemmas]

y:38 [binder, in Coq.Classes.EquivDec]

y:38 [binder, in Coq.Reals.NewtonInt]

y:38 [binder, in Coq.Logic.ClassicalDescription]

y:38 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:38 [binder, in Coq.Sets.Multiset]

y:38 [binder, in Coq.Sets.Image]

y:38 [binder, in Coq.Reals.R_sqr]

y:38 [binder, in Coq.Floats.FloatAxioms]

y:38 [binder, in Coq.Reals.ClassicalConstructiveReals]

y:38 [binder, in Coq.Relations.Relation_Operators]

y:380 [binder, in Coq.MSets.MSetRBT]

y:380 [binder, in Coq.Reals.Rtopology]

y:381 [binder, in Coq.FSets.FSetPositive]

y:382 [binder, in Coq.Logic.ChoiceFacts]

y:384 [binder, in Coq.ssr.ssrfun]

y:384 [binder, in Coq.Init.Logic]

y:385 [binder, in Coq.Logic.ChoiceFacts]

y:386 [binder, in Coq.FSets.FSetPositive]

y:386 [binder, in Coq.MSets.MSetRBT]

y:386 [binder, in Coq.Reals.Rtopology]

y:387 [binder, in Coq.Reals.Ranalysis5]

y:388 [binder, in Coq.Logic.ChoiceFacts]

y:389 [binder, in Coq.ssr.ssrfun]

y:389 [binder, in Coq.Reals.Rtopology]

y:39 [binder, in Coq.Reals.Ranalysis1]

y:39 [binder, in Coq.ZArith.BinIntDef]

y:39 [binder, in Coq.Reals.R_sqrt]

y:39 [binder, in Coq.ZArith.Wf_Z]

y:39 [binder, in Coq.setoid_ring.InitialRing]

y:39 [binder, in Coq.Structures.DecidableType]

y:39 [binder, in Coq.Reals.Rpower]

y:39 [binder, in Coq.Structures.OrderedTypeEx]

y:39 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y:39 [binder, in Coq.Reals.NewtonInt]

y:39 [binder, in Coq.Reals.Rbasic_fun]

y:39 [binder, in Coq.Logic.Berardi]

y:39 [binder, in Coq.Logic.HLevels]

y:39 [binder, in Coq.Sets.Image]

y:39 [binder, in Coq.Structures.OrdersTac]

y:39 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:39 [binder, in Coq.QArith.QArith_base]

y:39 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:390 [binder, in Coq.ssr.ssrbool]

y:391 [binder, in Coq.Reals.Rtopology]

y:392 [binder, in Coq.ssr.ssrbool]

y:392 [binder, in Coq.Reals.Rtopology]

y:392 [binder, in Coq.Init.Logic]

y:394 [binder, in Coq.ssr.ssrbool]

y:395 [binder, in Coq.Reals.Rtopology]

y:396 [binder, in Coq.Reals.Rtopology]

y:396 [binder, in Coq.Reals.Ranalysis5]

y:397 [binder, in Coq.ZArith.BinInt]

y:397 [binder, in Coq.ssr.ssrbool]

y:397 [binder, in Coq.FSets.FSetPositive]

y:397 [binder, in Coq.Reals.Rtopology]

y:398 [binder, in Coq.ssr.ssrbool]

y:398 [binder, in Coq.Reals.Rtopology]

y:399 [binder, in Coq.Reals.Ranalysis1]

y:399 [binder, in Coq.ZArith.BinInt]

y:399 [binder, in Coq.Logic.ChoiceFacts]

y:399 [binder, in Coq.Reals.Rtopology]

y:4 [binder, in Coq.Structures.Orders]

y:4 [binder, in Coq.Relations.Operators_Properties]

y:4 [binder, in Coq.micromega.Ztac]

y:4 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:4 [binder, in Coq.Reals.Rminmax]

y:4 [binder, in Coq.Structures.OrdersEx]

y:4 [binder, in Coq.Sets.Relations_3]

y:4 [binder, in Coq.PArith.BinPos]

y:4 [binder, in Coq.ZArith.BinInt]

y:4 [binder, in Coq.Structures.OrdersAlt]

y:4 [binder, in Coq.NArith.BinNat]

y:4 [binder, in Coq.Structures.OrderedTypeEx]

y:4 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y:4 [binder, in Coq.Sets.Uniset]

y:4 [binder, in Coq.Sets.Relations_1_facts]

y:4 [binder, in Coq.Structures.OrderedTypeAlt]

y:4 [binder, in Coq.ZArith.Zbool]

y:4 [binder, in Coq.Strings.Byte]

y:4 [binder, in Coq.Unicode.Utf8_core]

y:4 [binder, in Coq.omega.PreOmega]

y:4 [binder, in Coq.Sets.Relations_3_facts]

y:4 [binder, in Coq.Vectors.VectorEq]

y:4 [binder, in Coq.micromega.ZMicromega]

y:4 [binder, in Coq.Structures.OrdersFacts]

y:40 [binder, in Coq.Structures.Orders]

y:40 [binder, in Coq.QArith.Qcanon]

y:40 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:40 [binder, in Coq.Logic.EqdepFacts]

y:40 [binder, in Coq.Reals.Ranalysis4]

y:40 [binder, in Coq.micromega.RingMicromega]

y:40 [binder, in Coq.Lists.List]

y:40 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:40 [binder, in Coq.Classes.Morphisms]

y:40 [binder, in Coq.Structures.OrdersAlt]

y:40 [binder, in Coq.Reals.NewtonInt]

y:40 [binder, in Coq.Sets.Uniset]

y:40 [binder, in Coq.Structures.OrderedType]

y:40 [binder, in Coq.Classes.SetoidDec]

y:40 [binder, in Coq.Numbers.NatInt.NZOrder]

y:40 [binder, in Coq.Lists.ListSet]

y:40 [binder, in Coq.Sets.Permut]

y:40 [binder, in Coq.Reals.Ranalysis5]

y:40 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:40 [binder, in Coq.Reals.Rgeom]

y:40 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:40 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:400 [binder, in Coq.ssr.ssrbool]

y:400 [binder, in Coq.Init.Logic]

y:402 [binder, in Coq.Reals.Ranalysis1]

y:402 [binder, in Coq.Logic.ChoiceFacts]

y:402 [binder, in Coq.Init.Logic]

y:403 [binder, in Coq.Reals.Ranalysis1]

y:403 [binder, in Coq.ssr.ssrbool]

y:403 [binder, in Coq.FSets.FSetPositive]

y:403 [binder, in Coq.FSets.FMapList]

y:404 [binder, in Coq.Reals.Ranalysis1]

y:404 [binder, in Coq.ssr.ssrbool]

y:405 [binder, in Coq.Reals.Ranalysis1]

y:405 [binder, in Coq.ZArith.BinInt]

y:406 [binder, in Coq.Reals.Ranalysis1]

y:406 [binder, in Coq.Logic.ChoiceFacts]

y:407 [binder, in Coq.Reals.Ranalysis1]

y:407 [binder, in Coq.ZArith.BinInt]

y:407 [binder, in Coq.Lists.List]

y:407 [binder, in Coq.Reals.Ranalysis5]

y:408 [binder, in Coq.Reals.Ranalysis1]

y:409 [binder, in Coq.Reals.Ranalysis1]

y:409 [binder, in Coq.Logic.ChoiceFacts]

y:409 [binder, in Coq.FSets.FSetPositive]

y:41 [binder, in Coq.setoid_ring.Ncring_initial]

y:41 [binder, in Coq.Logic.Eqdep_dec]

y:41 [binder, in Coq.ZArith.BinIntDef]

y:41 [binder, in Coq.Reals.Ranalysis4]

y:41 [binder, in Coq.Logic.ClassicalEpsilon]

y:41 [binder, in Coq.Reals.R_sqrt]

y:41 [binder, in Coq.Logic.JMeq]

y:41 [binder, in Coq.Logic.ChoiceFacts]

y:41 [binder, in Coq.setoid_ring.InitialRing]

y:41 [binder, in Coq.Reals.Rdefinitions]

y:41 [binder, in Coq.Reals.Abstract.ConstructiveAbs]

y:41 [binder, in Coq.Structures.OrderedTypeEx]

y:41 [binder, in Coq.Reals.NewtonInt]

y:41 [binder, in Coq.Reals.Rtopology]

y:41 [binder, in Coq.ssr.ssrunder]

y:41 [binder, in Coq.Sets.Multiset]

y:41 [binder, in Coq.Reals.RList]

y:41 [binder, in Coq.micromega.ZifyInst]

y:41 [binder, in Coq.Floats.FloatAxioms]

y:41 [binder, in Coq.Structures.OrdersFacts]

y:410 [binder, in Coq.Reals.Ranalysis1]

y:410 [binder, in Coq.ZArith.BinInt]

y:411 [binder, in Coq.Reals.Ranalysis1]

y:412 [binder, in Coq.Reals.Ranalysis1]

y:412 [binder, in Coq.ZArith.BinInt]

y:412 [binder, in Coq.Reals.Rtopology]

y:413 [binder, in Coq.Reals.Ranalysis1]

y:414 [binder, in Coq.Reals.Ranalysis1]

y:415 [binder, in Coq.Lists.List]

y:416 [binder, in Coq.ZArith.BinInt]

y:417 [binder, in Coq.Reals.Ranalysis1]

y:418 [binder, in Coq.ZArith.BinInt]

y:418 [binder, in Coq.Reals.Rtopology]

y:42 [binder, in Coq.Structures.Orders]

y:42 [binder, in Coq.Relations.Operators_Properties]

y:42 [binder, in Coq.Reals.Ranalysis1]

y:42 [binder, in Coq.Logic.ConstructiveEpsilon]

y:42 [binder, in Coq.Reals.Abstract.ConstructiveLUB]

y:42 [binder, in Coq.Reals.Ranalysis4]

y:42 [binder, in Coq.micromega.RingMicromega]

y:42 [binder, in Coq.Reals.Rsqrt_def]

y:42 [binder, in Coq.Init.Wf]

y:42 [binder, in Coq.Reals.Rpower]

y:42 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y:42 [binder, in Coq.Reals.NewtonInt]

y:42 [binder, in Coq.Sets.Uniset]

y:42 [binder, in Coq.Reals.Rbasic_fun]

y:42 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:42 [binder, in Coq.Structures.OrdersTac]

y:42 [binder, in Coq.PArith.BinPosDef]

y:42 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:42 [binder, in Coq.QArith.QArith_base]

y:42 [binder, in Coq.Lists.SetoidList]

y:420 [binder, in Coq.Reals.Ranalysis1]

y:420 [binder, in Coq.ZArith.BinInt]

y:422 [binder, in Coq.Reals.Ranalysis1]

y:422 [binder, in Coq.ZArith.BinInt]

y:423 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:424 [binder, in Coq.ZArith.BinInt]

y:424 [binder, in Coq.Reals.Rtopology]

y:424 [binder, in Coq.Reals.Ranalysis5]

y:425 [binder, in Coq.Reals.Ranalysis1]

y:425 [binder, in Coq.Logic.ChoiceFacts]

y:426 [binder, in Coq.ZArith.BinInt]

y:426 [binder, in Coq.Reals.Rtopology]

y:427 [binder, in Coq.Logic.ChoiceFacts]

y:429 [binder, in Coq.ZArith.BinInt]

y:43 [binder, in Coq.Program.Wf]

y:43 [binder, in Coq.QArith.Qcanon]

y:43 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:43 [binder, in Coq.ZArith.BinIntDef]

y:43 [binder, in Coq.Reals.Abstract.ConstructiveLUB]

Y:43 [binder, in Coq.Sets.Finite_sets_facts]

y:43 [binder, in Coq.Reals.Ranalysis4]

y:43 [binder, in Coq.Reals.R_sqrt]

y:43 [binder, in Coq.Structures.OrdersAlt]

y:43 [binder, in Coq.setoid_ring.InitialRing]

y:43 [binder, in Coq.Reals.NewtonInt]

y:43 [binder, in Coq.Reals.Rtopology]

y:43 [binder, in Coq.Structures.OrderedType]

y:43 [binder, in Coq.setoid_ring.Ncring_polynom]

y:43 [binder, in Coq.Sets.Permut]

y:43 [binder, in Coq.Sets.Powerset_facts]

y:43 [binder, in Coq.Reals.Ranalysis5]

y:43 [binder, in Coq.Logic.Diaconescu]

y:43 [binder, in Coq.Reals.Rgeom]

y:43 [binder, in Coq.Relations.Relation_Operators]

y:43 [binder, in Coq.FSets.FSetCompat]

y:43 [binder, in Coq.Structures.OrdersFacts]

y:431 [binder, in Coq.Init.Logic]

y:44 [binder, in Coq.Structures.Orders]

y:44 [binder, in Coq.setoid_ring.Ncring_initial]

y:44 [binder, in Coq.Logic.ConstructiveEpsilon]

y:44 [binder, in Coq.Reals.Ranalysis4]

y:44 [binder, in Coq.micromega.RingMicromega]

y:44 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:44 [binder, in Coq.ZArith.Wf_Z]

y:44 [binder, in Coq.Reals.Abstract.ConstructiveAbs]

y:44 [binder, in Coq.Structures.OrderedTypeEx]

y:44 [binder, in Coq.Reals.NewtonInt]

y:44 [binder, in Coq.Logic.HLevels]

y:44 [binder, in Coq.Sets.Multiset]

y:44 [binder, in Coq.PArith.BinPosDef]

y:44 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:44 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:44 [binder, in Coq.Floats.FloatAxioms]

y:44 [binder, in Coq.QArith.QArith_base]

y:44 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:448 [binder, in Coq.Reals.Ranalysis5]

Y:45 [binder, in Coq.Logic.Decidable]

y:45 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:45 [binder, in Coq.Reals.Ranalysis1]

y:45 [binder, in Coq.ZArith.BinIntDef]

y:45 [binder, in Coq.Lists.List]

y:45 [binder, in Coq.Logic.JMeq]

y:45 [binder, in Coq.Init.Wf]

y:45 [binder, in Coq.setoid_ring.InitialRing]

y:45 [binder, in Coq.Reals.Rpower]

y:45 [binder, in Coq.Program.Equality]

y:45 [binder, in Coq.Reals.NewtonInt]

y:45 [binder, in Coq.Sets.Uniset]

y:45 [binder, in Coq.Structures.OrderedType]

y:45 [binder, in Coq.Reals.Rbasic_fun]

y:45 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:45 [binder, in Coq.Reals.RList]

y:45 [binder, in Coq.Logic.Diaconescu]

y:45 [binder, in Coq.Structures.OrdersTac]

y:45 [binder, in Coq.Reals.R_sqr]

y:45 [binder, in Coq.Structures.OrdersFacts]

y:450 [binder, in Coq.Reals.Ranalysis5]

y:451 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:452 [binder, in Coq.Reals.Ranalysis5]

y:453 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:455 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:456 [binder, in Coq.MSets.MSetRBT]

y:459 [binder, in Coq.MSets.MSetRBT]

y:46 [binder, in Coq.Structures.Orders]

y:46 [binder, in Coq.setoid_ring.Ncring_initial]

y:46 [binder, in Coq.QArith.Qcanon]

y:46 [binder, in Coq.Logic.Eqdep_dec]

Y:46 [binder, in Coq.Sets.Finite_sets_facts]

y:46 [binder, in Coq.Logic.EqdepFacts]

y:46 [binder, in Coq.Reals.R_sqrt]

y:46 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:46 [binder, in Coq.FSets.FMapFacts]

y:46 [binder, in Coq.Logic.ChoiceFacts]

y:46 [binder, in Coq.Structures.OrderedTypeEx]

y:46 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y:46 [binder, in Coq.Classes.EquivDec]

y:46 [binder, in Coq.Reals.Ranalysis5]

y:46 [binder, in Coq.Reals.Rgeom]

y:46 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:46 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:46 [binder, in Coq.QArith.QArith_base]

y:46 [binder, in Coq.FSets.FSetCompat]

y:464 [binder, in Coq.setoid_ring.Field_theory]

y:47 [binder, in Coq.Logic.Decidable]

y:47 [binder, in Coq.Relations.Operators_Properties]

y:47 [binder, in Coq.Logic.ConstructiveEpsilon]

y:47 [binder, in Coq.ZArith.BinIntDef]

y:47 [binder, in Coq.Reals.Rsqrt_def]

y:47 [binder, in Coq.setoid_ring.InitialRing]

y:47 [binder, in Coq.Structures.OrderedType]

y:47 [binder, in Coq.Structures.GenericMinMax]

y:47 [binder, in Coq.Sets.Permut]

y:47 [binder, in Coq.Reals.RList]

y:47 [binder, in Coq.Logic.Diaconescu]

y:47 [binder, in Coq.Reals.R_sqr]

y:470 [binder, in Coq.setoid_ring.Field_theory]

y:472 [binder, in Coq.setoid_ring.Field_theory]

y:474 [binder, in Coq.setoid_ring.Field_theory]

y:476 [binder, in Coq.setoid_ring.Field_theory]

y:479 [binder, in Coq.setoid_ring.Field_theory]

y:48 [binder, in Coq.Structures.Orders]

y:48 [binder, in Coq.QArith.Qcanon]

y:48 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

Y:48 [binder, in Coq.Sets.Finite_sets_facts]

y:48 [binder, in Coq.Reals.Rtrigo1]

y:48 [binder, in Coq.Reals.Ranalysis4]

y:48 [binder, in Coq.ssr.ssrfun]

y:48 [binder, in Coq.Reals.Rpower]

y:48 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y:48 [binder, in Coq.Sets.Uniset]

y:48 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:48 [binder, in Coq.Sets.Multiset]

y:48 [binder, in Coq.Structures.OrdersTac]

y:48 [binder, in Coq.Reals.Rgeom]

y:48 [binder, in Coq.QArith.QArith_base]

y:48 [binder, in Coq.Lists.SetoidList]

y:483 [binder, in Coq.setoid_ring.Field_theory]

y:485 [binder, in Coq.setoid_ring.Field_theory]

y:487 [binder, in Coq.setoid_ring.Field_theory]

y:49 [binder, in Coq.Logic.ConstructiveEpsilon]

Y:49 [binder, in Coq.Sets.Finite_sets_facts]

y:49 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:49 [binder, in Coq.ZArith.Wf_Z]

y:49 [binder, in Coq.Structures.OrderedTypeEx]

y:49 [binder, in Coq.Structures.OrderedType]

y:49 [binder, in Coq.Logic.Diaconescu]

y:49 [binder, in Coq.Reals.R_sqr]

y:49 [binder, in Coq.FSets.FSetCompat]

y:493 [binder, in Coq.MSets.MSetAVL]

y:497 [binder, in Coq.PArith.BinPos]

y:498 [binder, in Coq.MSets.MSetAVL]

y:499 [binder, in Coq.PArith.BinPos]

y:5 [binder, in Coq.Wellfounded.Union]

y:5 [binder, in Coq.Structures.DecidableTypeEx]

y:5 [binder, in Coq.setoid_ring.RealField]

y:5 [binder, in Coq.Sorting.PermutSetoid]

y:5 [binder, in Coq.Wellfounded.Transitive_Closure]

y:5 [binder, in Coq.QArith.Qreals]

y:5 [binder, in Coq.QArith.Qfield]

y:5 [binder, in Coq.Reals.Rdefinitions]

y:5 [binder, in Coq.Reals.Raxioms]

y:5 [binder, in Coq.micromega.ZifyNat]

y:5 [binder, in Coq.Logic.RelationalChoice]

y:5 [binder, in Coq.Structures.OrderedType]

y:5 [binder, in Coq.Classes.SetoidDec]

y:5 [binder, in Coq.Sets.Permut]

y:5 [binder, in Coq.Reals.Rtrigo_calc]

y:5 [binder, in Coq.Sets.Multiset]

y:5 [binder, in Coq.micromega.RMicromega]

y:5 [binder, in Coq.PArith.BinPosDef]

y:5 [binder, in Coq.Reals.R_sqr]

y:5 [binder, in Coq.micromega.ZifyN]

y:5 [binder, in Coq.micromega.ZifyInst]

y:5 [binder, in Coq.Sets.Relations_1]

y:5 [binder, in Coq.Relations.Relation_Definitions]

y:5 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:5 [binder, in Coq.Sorting.Heap]

y:5 [binder, in Coq.Logic.FinFun]

y:5 [binder, in Coq.Reals.Cos_plus]

y:50 [binder, in Coq.Logic.Decidable]

y:50 [binder, in Coq.Structures.Orders]

y:50 [binder, in Coq.Relations.Operators_Properties]

y:50 [binder, in Coq.Reals.Rtrigo1]

y:50 [binder, in Coq.Logic.JMeq]

y:50 [binder, in Coq.Reals.Rpower]

y:50 [binder, in Coq.Reals.PSeries_reg]

y:50 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:50 [binder, in Coq.Relations.Relation_Operators]

y:50 [binder, in Coq.QArith.QArith_base]

y:50 [binder, in Coq.Structures.OrdersFacts]

y:50 [binder, in Coq.Reals.Cos_plus]

y:501 [binder, in Coq.PArith.BinPos]

y:501 [binder, in Coq.Lists.List]

y:502 [binder, in Coq.ssr.ssrbool]

y:503 [binder, in Coq.PArith.BinPos]

y:505 [binder, in Coq.Lists.List]

y:507 [binder, in Coq.ssr.ssrbool]

y:508 [binder, in Coq.Lists.List]

y:509 [binder, in Coq.ssr.ssrbool]

y:509 [binder, in Coq.MSets.MSetAVL]

y:51 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:51 [binder, in Coq.Reals.Ranalysis4]

y:51 [binder, in Coq.FSets.FMapFacts]

y:51 [binder, in Coq.Reals.Rsqrt_def]

y:51 [binder, in Coq.ssr.ssrfun]

y:51 [binder, in Coq.Sets.Uniset]

y:51 [binder, in Coq.Reals.Ranalysis5]

y:51 [binder, in Coq.Sets.Multiset]

y:51 [binder, in Coq.Logic.Diaconescu]

y:51 [binder, in Coq.Structures.OrdersTac]

y:51 [binder, in Coq.Reals.R_sqr]

y:51 [binder, in Coq.Sorting.Mergesort]

y:51 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:515 [binder, in Coq.ssr.ssrbool]

y:515 [binder, in Coq.MSets.MSetRBT]

y:517 [binder, in Coq.Lists.List]

y:519 [binder, in Coq.ZArith.BinInt]

y:519 [binder, in Coq.MSets.MSetAVL]

y:52 [binder, in Coq.Logic.Decidable]

y:52 [binder, in Coq.Structures.Orders]

y:52 [binder, in Coq.Relations.Operators_Properties]

y:52 [binder, in Coq.Logic.EqdepFacts]

y:52 [binder, in Coq.Reals.Ranalysis4]

y:52 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:52 [binder, in Coq.Init.Wf]

y:52 [binder, in Coq.Structures.OrderedTypeEx]

y:52 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y:52 [binder, in Coq.Structures.OrderedType]

y:52 [binder, in Coq.Sets.Powerset_facts]

y:52 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:52 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:52 [binder, in Coq.QArith.QArith_base]

y:52 [binder, in Coq.FSets.FSetCompat]

y:52 [binder, in Coq.Structures.OrdersFacts]

y:521 [binder, in Coq.micromega.Tauto]

y:522 [binder, in Coq.MSets.MSetAVL]

y:524 [binder, in Coq.ssr.ssrbool]

y:526 [binder, in Coq.micromega.Tauto]

y:529 [binder, in Coq.FSets.FMapWeakList]

y:53 [binder, in Coq.Reals.Rderiv]

y:53 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:53 [binder, in Coq.QArith.Qcanon]

y:53 [binder, in Coq.Logic.Eqdep_dec]

y:53 [binder, in Coq.Reals.Rtrigo1]

y:53 [binder, in Coq.FSets.FSetDecide]

y:53 [binder, in Coq.Reals.Ranalysis4]

y:53 [binder, in Coq.MSets.MSetDecide]

y:53 [binder, in Coq.ssr.ssrfun]

y:53 [binder, in Coq.Reals.Rpower]

y:53 [binder, in Coq.FSets.FSetPositive]

y:53 [binder, in Coq.MSets.MSetPositive]

y:53 [binder, in Coq.Reals.Ranalysis5]

y:53 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:53 [binder, in Coq.Reals.R_sqr]

y:53 [binder, in Coq.micromega.ZifyInst]

y:53 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:53 [binder, in Coq.Relations.Relation_Operators]

y:530 [binder, in Coq.MSets.MSetAVL]

y:533 [binder, in Coq.ssr.ssrbool]

y:539 [binder, in Coq.PArith.BinPos]

y:539 [binder, in Coq.ssr.ssrbool]

y:54 [binder, in Coq.Structures.Orders]

y:54 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:54 [binder, in Coq.Logic.JMeq]

y:54 [binder, in Coq.Logic.ChoiceFacts]

y:54 [binder, in Coq.Structures.OrderedTypeEx]

y:54 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y:54 [binder, in Coq.ZArith.Zpower]

y:54 [binder, in Coq.Sets.Uniset]

y:54 [binder, in Coq.Logic.Diaconescu]

y:54 [binder, in Coq.Structures.OrdersTac]

y:54 [binder, in Coq.Reals.ClassicalConstructiveReals]

y:54 [binder, in Coq.QArith.QArith_base]

y:54 [binder, in Coq.Logic.FinFun]

y:54 [binder, in Coq.Structures.OrdersFacts]

y:540 [binder, in Coq.ssr.ssrbool]

y:541 [binder, in Coq.Init.Specif]

y:541 [binder, in Coq.MSets.MSetAVL]

y:542 [binder, in Coq.FSets.FMapWeakList]

y:543 [binder, in Coq.MSets.MSetRBT]

y:544 [binder, in Coq.ssr.ssrbool]

y:546 [binder, in Coq.ssr.ssrbool]

y:548 [binder, in Coq.ssr.ssrbool]

y:549 [binder, in Coq.Strings.Byte]

y:549 [binder, in Coq.FSets.FMapList]

y:55 [binder, in Coq.Relations.Operators_Properties]

y:55 [binder, in Coq.Reals.Ranalysis4]

y:55 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:55 [binder, in Coq.FSets.FMapFacts]

y:55 [binder, in Coq.ssr.ssrfun]

y:55 [binder, in Coq.ZArith.Zbool]

y:55 [binder, in Coq.Structures.OrderedType]

y:55 [binder, in Coq.Sets.Powerset_facts]

y:55 [binder, in Coq.Reals.Ranalysis5]

y:55 [binder, in Coq.Sets.Multiset]

y:55 [binder, in Coq.Reals.R_sqr]

y:55 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:55 [binder, in Coq.Relations.Relation_Operators]

y:55 [binder, in Coq.FSets.FSetCompat]

y:552 [binder, in Coq.ssr.ssrbool]

y:552 [binder, in Coq.FSets.FMapWeakList]

y:554 [binder, in Coq.ssr.ssrbool]

y:555 [binder, in Coq.MSets.MSetAVL]

y:556 [binder, in Coq.FSets.FMapWeakList]

y:558 [binder, in Coq.ssr.ssrbool]

y:56 [binder, in Coq.Structures.Orders]

y:56 [binder, in Coq.Reals.Rsqrt_def]

y:56 [binder, in Coq.Bool.Bool]

y:56 [binder, in Coq.Structures.OrderedTypeEx]

y:56 [binder, in Coq.Classes.EquivDec]

y:56 [binder, in Coq.Reals.Rbasic_fun]

y:56 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:56 [binder, in Coq.QArith.QArith_base]

y:561 [binder, in Coq.FSets.FMapWeakList]

y:562 [binder, in Coq.FSets.FMapList]

y:563 [binder, in Coq.ssr.ssrbool]

y:565 [binder, in Coq.MSets.MSetAVL]

y:566 [binder, in Coq.ssr.ssrbool]

y:566 [binder, in Coq.FSets.FMapWeakList]

y:568 [binder, in Coq.ssr.ssrbool]

y:569 [binder, in Coq.FSets.FMapWeakList]

y:57 [binder, in Coq.Program.Wf]

y:57 [binder, in Coq.Relations.Operators_Properties]

y:57 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:57 [binder, in Coq.Logic.Eqdep_dec]

y:57 [binder, in Coq.FSets.FSetDecide]

y:57 [binder, in Coq.Reals.Ranalysis4]

y:57 [binder, in Coq.Classes.RelationClasses]

y:57 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:57 [binder, in Coq.MSets.MSetDecide]

y:57 [binder, in Coq.ssr.ssrfun]

y:57 [binder, in Coq.Reals.Rpower]

y:57 [binder, in Coq.ZArith.Zpower]

y:57 [binder, in Coq.ZArith.Zbool]

y:57 [binder, in Coq.Logic.Diaconescu]

y:57 [binder, in Coq.Structures.OrdersTac]

y:57 [binder, in Coq.Reals.R_sqr]

y:57 [binder, in Coq.Structures.OrdersFacts]

y:572 [binder, in Coq.MSets.MSetAVL]

y:572 [binder, in Coq.FSets.FMapList]

y:573 [binder, in Coq.FSets.FMapWeakList]

y:575 [binder, in Coq.MSets.MSetRBT]

y:576 [binder, in Coq.FSets.FMapList]

y:58 [binder, in Coq.Program.Wf]

y:58 [binder, in Coq.setoid_ring.Ncring_initial]

y:58 [binder, in Coq.Logic.EqdepFacts]

y:58 [binder, in Coq.Reals.Ranalysis4]

y:58 [binder, in Coq.Lists.List]

y:58 [binder, in Coq.Sets.Uniset]

y:58 [binder, in Coq.Structures.OrderedType]

y:58 [binder, in Coq.Reals.Rbasic_fun]

y:58 [binder, in Coq.Reals.PSeries_reg]

y:58 [binder, in Coq.Reals.Ranalysis5]

y:58 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:58 [binder, in Coq.micromega.RMicromega]

y:58 [binder, in Coq.micromega.ZifyInst]

y:58 [binder, in Coq.QArith.QArith_base]

y:58 [binder, in Coq.FSets.FSetCompat]

y:581 [binder, in Coq.FSets.FMapList]

y:582 [binder, in Coq.MSets.MSetAVL]

y:585 [binder, in Coq.ssr.ssrbool]

y:585 [binder, in Coq.Reals.RIneq]

y:586 [binder, in Coq.MSets.MSetAVL]

y:586 [binder, in Coq.FSets.FMapList]

y:587 [binder, in Coq.Reals.RIneq]

y:588 [binder, in Coq.ssr.ssrbool]

y:589 [binder, in Coq.Reals.RIneq]

y:589 [binder, in Coq.FSets.FMapList]

y:59 [binder, in Coq.Relations.Operators_Properties]

y:59 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:59 [binder, in Coq.Reals.Ranalysis1]

y:59 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:59 [binder, in Coq.Logic.JMeq]

y:59 [binder, in Coq.ZArith.Zbool]

y:59 [binder, in Coq.Sets.Multiset]

y:59 [binder, in Coq.Structures.OrdersTac]

y:59 [binder, in Coq.Reals.R_sqr]

y:59 [binder, in Coq.Lists.SetoidList]

y:591 [binder, in Coq.ssr.ssrbool]

y:591 [binder, in Coq.Reals.RIneq]

y:593 [binder, in Coq.Reals.RIneq]

y:593 [binder, in Coq.FSets.FMapList]

y:594 [binder, in Coq.Lists.List]

y:594 [binder, in Coq.MSets.MSetAVL]

y:595 [binder, in Coq.ssr.ssrbool]

y:595 [binder, in Coq.MSets.MSetAVL]

y:596 [binder, in Coq.MSets.MSetAVL]

y:597 [binder, in Coq.Lists.List]

y:597 [binder, in Coq.MSets.MSetAVL]

y:597 [binder, in Coq.Reals.RIneq]

y:599 [binder, in Coq.ssr.ssrbool]

y:6 [binder, in Coq.Program.Wf]

y:6 [binder, in Coq.micromega.Ztac]

y:6 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:6 [binder, in Coq.Wellfounded.Inverse_Image]

y:6 [binder, in Coq.Reals.Rminmax]

y:6 [binder, in Coq.PArith.BinPos]

y:6 [binder, in Coq.MSets.MSetProperties]

y:6 [binder, in Coq.ZArith.BinInt]

y:6 [binder, in Coq.Numbers.NatInt.NZBase]

y:6 [binder, in Coq.Reals.Exp_prop]

y:6 [binder, in Coq.Reals.Rsqrt_def]

y:6 [binder, in Coq.Logic.ChoiceFacts]

y:6 [binder, in Coq.Init.Wf]

y:6 [binder, in Coq.Relations.Relations]

y:6 [binder, in Coq.NArith.BinNat]

y:6 [binder, in Coq.Classes.EquivDec]

y:6 [binder, in Coq.Logic.ClassicalUniqueChoice]

y:6 [binder, in Coq.ZArith.Zbool]

y:6 [binder, in Coq.Structures.Equalities]

y:6 [binder, in Coq.Reals.Rtopology]

y:6 [binder, in Coq.ZArith.Zpow_alt]

y:6 [binder, in Coq.Bool.BoolEq]

y:6 [binder, in Coq.micromega.ZifyComparison]

y:6 [binder, in Coq.Structures.GenericMinMax]

y:6 [binder, in Coq.Strings.Byte]

y:6 [binder, in Coq.micromega.Fourier_util]

y:6 [binder, in Coq.Logic.HLevels]

y:6 [binder, in Coq.Unicode.Utf8_core]

y:6 [binder, in Coq.Reals.Ranalysis5]

y:6 [binder, in Coq.Sets.Relations_2]

y:6 [binder, in Coq.omega.PreOmega]

y:6 [binder, in Coq.Logic.Adjointification]

y:6 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:6 [binder, in Coq.FSets.FSetProperties]

y:6 [binder, in Coq.Reals.ClassicalConstructiveReals]

y:6 [binder, in Coq.Relations.Relation_Operators]

y:6 [binder, in Coq.Bool.DecBool]

y:6 [binder, in Coq.Lists.SetoidList]

y:6 [binder, in Coq.Structures.OrdersFacts]

y:60 [binder, in Coq.Reals.Ranalysis4]

y:60 [binder, in Coq.FSets.FMapFacts]

y:60 [binder, in Coq.Reals.Rsqrt_def]

y:60 [binder, in Coq.Init.Wf]

y:60 [binder, in Coq.Reals.Rdefinitions]

y:60 [binder, in Coq.Reals.Rpower]

y:60 [binder, in Coq.Reals.Rbasic_fun]

y:60 [binder, in Coq.Sets.Powerset_facts]

y:60 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:60 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:60 [binder, in Coq.Relations.Relation_Operators]

y:60 [binder, in Coq.QArith.QArith_base]

y:60 [binder, in Coq.Structures.OrdersFacts]

y:602 [binder, in Coq.Lists.List]

y:603 [binder, in Coq.ssr.ssrbool]

y:605 [binder, in Coq.PArith.BinPos]

y:608 [binder, in Coq.FSets.FMapFacts]

y:608 [binder, in Coq.MSets.MSetAVL]

y:61 [binder, in Coq.Relations.Operators_Properties]

y:61 [binder, in Coq.Logic.Eqdep_dec]

y:61 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:61 [binder, in Coq.Sets.Uniset]

y:61 [binder, in Coq.ZArith.Zbool]

y:61 [binder, in Coq.Structures.OrderedType]

y:61 [binder, in Coq.Reals.Ranalysis5]

y:61 [binder, in Coq.Structures.OrdersTac]

y:61 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:61 [binder, in Coq.micromega.Tauto]

y:61 [binder, in Coq.Lists.SetoidList]

y:611 [binder, in Coq.FSets.FMapFacts]

y:611 [binder, in Coq.MSets.MSetAVL]

y:612 [binder, in Coq.ssr.ssrbool]

y:618 [binder, in Coq.FSets.FMapWeakList]

y:62 [binder, in Coq.Program.Wf]

y:62 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:62 [binder, in Coq.Reals.Ranalysis4]

y:62 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]

y:62 [binder, in Coq.Lists.List]

y:62 [binder, in Coq.Reals.Rpower]

y:62 [binder, in Coq.Reals.Rbasic_fun]

y:62 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:62 [binder, in Coq.Reals.R_sqr]

y:62 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:62 [binder, in Coq.QArith.QArith_base]

y:62 [binder, in Coq.Logic.FinFun]

y:622 [binder, in Coq.MSets.MSetAVL]

y:625 [binder, in Coq.MSets.MSetAVL]

y:63 [binder, in Coq.Relations.Operators_Properties]

y:63 [binder, in Coq.Reals.Rtrigo1]

y:63 [binder, in Coq.FSets.FSetDecide]

y:63 [binder, in Coq.Classes.RelationClasses]

y:63 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:63 [binder, in Coq.MSets.MSetDecide]

y:63 [binder, in Coq.setoid_ring.InitialRing]

y:63 [binder, in Coq.Structures.OrderedTypeEx]

y:63 [binder, in Coq.Structures.OrdersTac]

y:63 [binder, in Coq.Logic.FinFun]

y:63 [binder, in Coq.Structures.OrdersFacts]

y:634 [binder, in Coq.Lists.List]

y:634 [binder, in Coq.MSets.MSetAVL]

y:638 [binder, in Coq.Lists.List]

y:639 [binder, in Coq.FSets.FMapList]

y:64 [binder, in Coq.QArith.Qcanon]

y:64 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:64 [binder, in Coq.Logic.EqdepFacts]

y:64 [binder, in Coq.FSets.FMapFacts]

y:64 [binder, in Coq.Reals.Rsqrt_def]

y:64 [binder, in Coq.Structures.OrderedType]

y:64 [binder, in Coq.Reals.Rbasic_fun]

y:64 [binder, in Coq.Sets.Powerset_facts]

y:64 [binder, in Coq.Reals.Ranalysis5]

y:64 [binder, in Coq.Sets.Multiset]

y:64 [binder, in Coq.Sets.Image]

y:64 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:64 [binder, in Coq.Lists.SetoidList]

y:644 [binder, in Coq.Init.Logic]

y:645 [binder, in Coq.Lists.List]

y:65 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:65 [binder, in Coq.setoid_ring.InitialRing]

y:65 [binder, in Coq.Reals.Rpower]

y:65 [binder, in Coq.Sets.Uniset]

y:65 [binder, in Coq.micromega.RMicromega]

y:65 [binder, in Coq.Reals.R_sqr]

y:65 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:65 [binder, in Coq.Relations.Relation_Operators]

y:65 [binder, in Coq.QArith.QArith_base]

y:650 [binder, in Coq.Lists.List]

y:652 [binder, in Coq.Lists.List]

y:658 [binder, in Coq.Lists.List]

y:66 [binder, in Coq.Program.Wf]

y:66 [binder, in Coq.Relations.Operators_Properties]

y:66 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:66 [binder, in Coq.QArith.Qcanon]

y:66 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:66 [binder, in Coq.Logic.JMeq]

y:66 [binder, in Coq.Logic.ChoiceFacts]

y:66 [binder, in Coq.Structures.OrderedTypeEx]

y:66 [binder, in Coq.Reals.Raxioms]

y:66 [binder, in Coq.Classes.CRelationClasses]

y:66 [binder, in Coq.Reals.Rbasic_fun]

y:66 [binder, in Coq.Reals.PSeries_reg]

y:66 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:66 [binder, in Coq.Structures.OrdersFacts]

y:662 [binder, in Coq.Lists.List]

y:667 [binder, in Coq.ssr.ssrbool]

y:669 [binder, in Coq.ssr.ssrbool]

y:67 [binder, in Coq.Reals.Ranalysis4]

y:67 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:67 [binder, in Coq.Init.Wf]

y:67 [binder, in Coq.setoid_ring.InitialRing]

y:67 [binder, in Coq.Reals.Rtopology]

y:67 [binder, in Coq.Structures.OrderedType]

y:67 [binder, in Coq.setoid_ring.Ring_theory]

y:67 [binder, in Coq.micromega.RMicromega]

y:67 [binder, in Coq.QArith.QArith_base]

y:671 [binder, in Coq.ssr.ssrbool]

y:673 [binder, in Coq.ssr.ssrbool]

y:68 [binder, in Coq.Relations.Operators_Properties]

y:68 [binder, in Coq.FSets.FSetDecide]

y:68 [binder, in Coq.Reals.Ranalysis4]

y:68 [binder, in Coq.FSets.FMapFacts]

y:68 [binder, in Coq.Logic.ChoiceFacts]

y:68 [binder, in Coq.FSets.FMapInterface]

y:68 [binder, in Coq.MSets.MSetDecide]

y:68 [binder, in Coq.Classes.EquivDec]

y:68 [binder, in Coq.Reals.Raxioms]

y:68 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:69 [binder, in Coq.QArith.Qcanon]

y:69 [binder, in Coq.Logic.Eqdep_dec]

y:69 [binder, in Coq.micromega.ZifyClasses]

y:69 [binder, in Coq.Reals.Ranalysis4]

y:69 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:69 [binder, in Coq.Sets.Uniset]

y:69 [binder, in Coq.Structures.OrderedType]

y:69 [binder, in Coq.Reals.Rbasic_fun]

y:69 [binder, in Coq.Reals.Ranalysis5]

y:69 [binder, in Coq.micromega.RMicromega]

y:69 [binder, in Coq.PArith.BinPosDef]

y:69 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:69 [binder, in Coq.Structures.OrdersFacts]

y:7 [binder, in Coq.Program.Wf]

y:7 [binder, in Coq.Relations.Operators_Properties]

y:7 [binder, in Coq.Structures.DecidableTypeEx]

y:7 [binder, in Coq.Wellfounded.Inverse_Image]

y:7 [binder, in Coq.Sets.Relations_3]

y:7 [binder, in Coq.Arith.Bool_nat]

y:7 [binder, in Coq.Logic.SetoidChoice]

y:7 [binder, in Coq.Reals.R_sqrt]

y:7 [binder, in Coq.micromega.ZifyBool]

y:7 [binder, in Coq.QArith.Qreals]

y:7 [binder, in Coq.Arith.Cantor]

y:7 [binder, in Coq.QArith.Qfield]

y:7 [binder, in Coq.Sets.Cpo]

y:7 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

y:7 [binder, in Coq.Reals.Raxioms]

y:7 [binder, in Coq.Reals.PSeries_reg]

y:7 [binder, in Coq.ssr.ssrunder]

y:7 [binder, in Coq.micromega.RMicromega]

Y:7 [binder, in Coq.Sets.Classical_sets]

y:7 [binder, in Coq.PArith.BinPosDef]

y:7 [binder, in Coq.Reals.R_sqr]

y:7 [binder, in Coq.Relations.Relation_Operators]

y:7 [binder, in Coq.Sorting.Heap]

y:7 [binder, in Coq.Reals.Cos_plus]

y:70 [binder, in Coq.Program.Wf]

y:70 [binder, in Coq.Relations.Operators_Properties]

y:70 [binder, in Coq.Logic.EqdepFacts]

y:70 [binder, in Coq.Reals.Ranalysis4]

y:70 [binder, in Coq.Structures.OrderedTypeEx]

y:70 [binder, in Coq.setoid_ring.Ring_theory]

y:70 [binder, in Coq.Relations.Relation_Operators]

y:70 [binder, in Coq.QArith.QArith_base]

y:70 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:708 [binder, in Coq.ssr.ssrbool]

y:71 [binder, in Coq.Program.Wf]

y:71 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:71 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:71 [binder, in Coq.FSets.FMapFacts]

y:71 [binder, in Coq.ssr.ssrfun]

y:71 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:71 [binder, in Coq.micromega.RMicromega]

y:71 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:710 [binder, in Coq.ssr.ssrbool]

y:712 [binder, in Coq.Lists.List]

y:72 [binder, in Coq.Relations.Operators_Properties]

y:72 [binder, in Coq.QArith.Qcanon]

y:72 [binder, in Coq.Logic.JMeq]

y:72 [binder, in Coq.Reals.Rsqrt_def]

y:72 [binder, in Coq.Structures.OrderedTypeEx]

y:72 [binder, in Coq.Reals.Raxioms]

y:72 [binder, in Coq.Classes.CRelationClasses]

y:72 [binder, in Coq.Structures.OrderedType]

y:72 [binder, in Coq.Logic.Diaconescu]

y:72 [binder, in Coq.QArith.QArith_base]

y:72 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:72 [binder, in Coq.Structures.OrdersFacts]

y:73 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:73 [binder, in Coq.micromega.RingMicromega]

y:73 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]

y:73 [binder, in Coq.Reals.Exp_prop]

y:73 [binder, in Coq.Init.Wf]

y:73 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:73 [binder, in Coq.micromega.RMicromega]

y:73 [binder, in Coq.Logic.Diaconescu]

y:73 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:73 [binder, in Coq.micromega.ZifyInst]

y:73 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:73 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:74 [binder, in Coq.QArith.Qcanon]

y:74 [binder, in Coq.Reals.Ranalysis4]

y:74 [binder, in Coq.Classes.RelationClasses]

y:74 [binder, in Coq.Reals.Rpower]

y:74 [binder, in Coq.Structures.OrderedTypeEx]

y:74 [binder, in Coq.Reals.Raxioms]

y:74 [binder, in Coq.Sets.Uniset]

y:74 [binder, in Coq.Structures.OrderedType]

y:74 [binder, in Coq.Logic.Diaconescu]

y:74 [binder, in Coq.Reals.R_sqr]

y:74 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:74 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:74 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:742 [binder, in Coq.ssr.ssrbool]

y:75 [binder, in Coq.FSets.FSetDecide]

y:75 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:75 [binder, in Coq.FSets.FMapFacts]

y:75 [binder, in Coq.MSets.MSetDecide]

y:75 [binder, in Coq.Reals.Rbasic_fun]

y:75 [binder, in Coq.Reals.Ranalysis5]

y:75 [binder, in Coq.micromega.RMicromega]

y:75 [binder, in Coq.Logic.Diaconescu]

y:75 [binder, in Coq.micromega.ZifyInst]

y:75 [binder, in Coq.Relations.Relation_Operators]

y:75 [binder, in Coq.QArith.QArith_base]

y:75 [binder, in Coq.Structures.OrdersFacts]

y:757 [binder, in Coq.ssr.ssrbool]

y:759 [binder, in Coq.ssr.ssrbool]

y:76 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:76 [binder, in Coq.Logic.Eqdep_dec]

y:76 [binder, in Coq.Reals.Rfunctions]

y:76 [binder, in Coq.Arith.PeanoNat]

y:76 [binder, in Coq.Vectors.Fin]

y:76 [binder, in Coq.Reals.Rtopology]

y:76 [binder, in Coq.Structures.OrderedType]

y:76 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:76 [binder, in Coq.Logic.Diaconescu]

y:76 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:76 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:761 [binder, in Coq.ssr.ssrbool]

y:763 [binder, in Coq.ssr.ssrbool]

y:766 [binder, in Coq.ssr.ssrbool]

y:768 [binder, in Coq.ssr.ssrbool]

y:77 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:77 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:77 [binder, in Coq.Logic.ChoiceFacts]

y:77 [binder, in Coq.Reals.Rpower]

y:77 [binder, in Coq.omega.OmegaLemmas]

y:77 [binder, in Coq.Reals.Rbasic_fun]

y:77 [binder, in Coq.Init.Datatypes]

y:77 [binder, in Coq.Reals.Ranalysis5]

y:77 [binder, in Coq.Logic.Diaconescu]

y:77 [binder, in Coq.micromega.ZifyInst]

y:77 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:770 [binder, in Coq.ssr.ssrbool]

y:772 [binder, in Coq.ssr.ssrbool]

y:774 [binder, in Coq.ssr.ssrbool]

y:776 [binder, in Coq.ssr.ssrbool]

y:778 [binder, in Coq.ssr.ssrbool]

y:78 [binder, in Coq.Logic.JMeq]

y:78 [binder, in Coq.Structures.OrderedType]

y:78 [binder, in Coq.setoid_ring.Ring_theory]

y:78 [binder, in Coq.Structures.EqualitiesFacts]

y:78 [binder, in Coq.QArith.QArith_base]

y:78 [binder, in Coq.Structures.OrdersFacts]

y:780 [binder, in Coq.ssr.ssrbool]

y:782 [binder, in Coq.ssr.ssrbool]

y:784 [binder, in Coq.ssr.ssrbool]

y:786 [binder, in Coq.ssr.ssrbool]

y:788 [binder, in Coq.ssr.ssrbool]

y:79 [binder, in Coq.Classes.RelationClasses]

y:79 [binder, in Coq.MSets.MSetWeakList]

y:79 [binder, in Coq.Reals.Rtopology]

y:79 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:79 [binder, in Coq.micromega.ZifyInst]

y:790 [binder, in Coq.ssr.ssrbool]

y:792 [binder, in Coq.ssr.ssrbool]

y:794 [binder, in Coq.ssr.ssrbool]

y:796 [binder, in Coq.ssr.ssrbool]

y:798 [binder, in Coq.ssr.ssrbool]

y:8 [binder, in Coq.Structures.Orders]

y:8 [binder, in Coq.micromega.Ztac]

y:8 [binder, in Coq.Structures.OrdersLists]

y:8 [binder, in Coq.ZArith.BinIntDef]

y:8 [binder, in Coq.FSets.FSetBridge]

y:8 [binder, in Coq.Reals.Rminmax]

y:8 [binder, in Coq.Sets.Constructive_sets]

y:8 [binder, in Coq.PArith.BinPos]

y:8 [binder, in Coq.Classes.RelationClasses]

y:8 [binder, in Coq.ZArith.BinInt]

y:8 [binder, in Coq.Logic.JMeq]

y:8 [binder, in Coq.Structures.OrdersAlt]

y:8 [binder, in Coq.Wellfounded.Lexicographic_Product]

y:8 [binder, in Coq.Program.Subset]

y:8 [binder, in Coq.Init.Wf]

y:8 [binder, in Coq.NArith.BinNat]

y:8 [binder, in Coq.Sorting.Permutation]

y:8 [binder, in Coq.funind.Recdef]

y:8 [binder, in Coq.Structures.OrderedTypeEx]

y:8 [binder, in Coq.Structures.OrderedTypeAlt]

y:8 [binder, in Coq.Logic.RelationalChoice]

y:8 [binder, in Coq.ZArith.Zbool]

y:8 [binder, in Coq.micromega.ZifyComparison]

y:8 [binder, in Coq.Sets.Permut]

Y:8 [binder, in Coq.Sets.Powerset_Classical_facts]

y:8 [binder, in Coq.setoid_ring.Ring_theory]

y:8 [binder, in Coq.omega.PreOmega]

y:8 [binder, in Coq.Sets.Image]

y:8 [binder, in Coq.Sets.Relations_1]

y:8 [binder, in Coq.Relations.Relation_Definitions]

y:8 [binder, in Coq.Numbers.Cyclic.Int63.Sint63]

y:8 [binder, in Coq.Reals.ROrderedType]

y:8 [binder, in Coq.Floats.FloatAxioms]

y:8 [binder, in Coq.Reals.Cos_rel]

y:8 [binder, in Coq.QArith.QArith_base]

y:8 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:8 [binder, in Coq.Lists.SetoidList]

y:8 [binder, in Coq.Structures.OrdersFacts]

y:80 [binder, in Coq.QArith.Qcanon]

y:80 [binder, in Coq.Logic.ChoiceFacts]

y:80 [binder, in Coq.Reals.Rpower]

y:80 [binder, in Coq.omega.OmegaLemmas]

y:80 [binder, in Coq.Structures.OrderedType]

y:80 [binder, in Coq.Reals.Rbasic_fun]

y:80 [binder, in Coq.Reals.Ratan]

y:80 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:80 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:800 [binder, in Coq.ssr.ssrbool]

y:802 [binder, in Coq.Init.Specif]

y:802 [binder, in Coq.ssr.ssrbool]

y:804 [binder, in Coq.ssr.ssrbool]

y:806 [binder, in Coq.ssr.ssrbool]

y:808 [binder, in Coq.ssr.ssrbool]

y:81 [binder, in Coq.FSets.FSetDecide]

y:81 [binder, in Coq.Reals.Ranalysis4]

y:81 [binder, in Coq.MSets.MSetDecide]

y:81 [binder, in Coq.setoid_ring.Ring_theory]

y:81 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:81 [binder, in Coq.micromega.ZifyInst]

y:81 [binder, in Coq.Structures.OrdersFacts]

y:82 [binder, in Coq.Program.Wf]

y:82 [binder, in Coq.QArith.Qcanon]

y:82 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:82 [binder, in Coq.Arith.PeanoNat]

y:82 [binder, in Coq.Structures.OrderedTypeEx]

y:82 [binder, in Coq.Structures.OrderedType]

y:82 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:824 [binder, in Coq.ssr.ssrbool]

y:826 [binder, in Coq.ssr.ssrbool]

y:828 [binder, in Coq.ssr.ssrbool]

y:83 [binder, in Coq.Logic.Eqdep_dec]

y:83 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]

y:83 [binder, in Coq.Classes.CRelationClasses]

y:83 [binder, in Coq.Reals.Rbasic_fun]

y:83 [binder, in Coq.Reals.Ranalysis5]

y:83 [binder, in Coq.Structures.EqualitiesFacts]

y:83 [binder, in Coq.PArith.BinPosDef]

y:83 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:83 [binder, in Coq.Relations.Relation_Operators]

y:83 [binder, in Coq.Structures.OrdersFacts]

y:830 [binder, in Coq.ssr.ssrbool]

y:836 [binder, in Coq.ssr.ssrbool]

y:838 [binder, in Coq.ssr.ssrbool]

y:84 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:84 [binder, in Coq.FSets.FSetDecide]

y:84 [binder, in Coq.Reals.Rsqrt_def]

y:84 [binder, in Coq.MSets.MSetDecide]

y:84 [binder, in Coq.Init.Wf]

y:84 [binder, in Coq.Arith.PeanoNat]

y:84 [binder, in Coq.omega.OmegaLemmas]

y:84 [binder, in Coq.Structures.OrderedTypeEx]

y:84 [binder, in Coq.Reals.Rtopology]

y:84 [binder, in Coq.Structures.OrderedType]

y:84 [binder, in Coq.Reals.Ranalysis5]

y:84 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:84 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:84 [binder, in Coq.micromega.Tauto]

y:84 [binder, in Coq.Logic.FinFun]

y:840 [binder, in Coq.ssr.ssrbool]

y:842 [binder, in Coq.ssr.ssrbool]

y:844 [binder, in Coq.ssr.ssrbool]

y:846 [binder, in Coq.ssr.ssrbool]

y:848 [binder, in Coq.ssr.ssrbool]

y:85 [binder, in Coq.QArith.Qcanon]

y:85 [binder, in Coq.micromega.ZifyClasses]

y:85 [binder, in Coq.Classes.RelationClasses]

y:85 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]

y:85 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:85 [binder, in Coq.setoid_ring.Ring_theory]

y:85 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:85 [binder, in Coq.PArith.BinPosDef]

y:85 [binder, in Coq.Relations.Relation_Operators]

y:85 [binder, in Coq.Structures.OrdersFacts]

y:850 [binder, in Coq.ssr.ssrbool]

y:852 [binder, in Coq.ssr.ssrbool]

y:854 [binder, in Coq.ssr.ssrbool]

y:856 [binder, in Coq.ssr.ssrbool]

y:858 [binder, in Coq.Lists.List]

y:858 [binder, in Coq.ssr.ssrbool]

y:86 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:86 [binder, in Coq.MSets.MSetWeakList]

y:86 [binder, in Coq.Arith.PeanoNat]

y:86 [binder, in Coq.Structures.OrderedType]

y:86 [binder, in Coq.Reals.Rbasic_fun]

y:86 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:86 [binder, in Coq.Lists.SetoidList]

y:860 [binder, in Coq.ssr.ssrbool]

y:862 [binder, in Coq.ssr.ssrbool]

y:864 [binder, in Coq.ssr.ssrbool]

y:866 [binder, in Coq.ssr.ssrbool]

y:868 [binder, in Coq.ssr.ssrbool]

y:87 [binder, in Coq.QArith.Qcanon]

y:87 [binder, in Coq.Logic.Eqdep_dec]

y:87 [binder, in Coq.Reals.Ranalysis4]

y:87 [binder, in Coq.Reals.Exp_prop]

y:87 [binder, in Coq.Reals.Rpower]

y:87 [binder, in Coq.omega.OmegaLemmas]

y:87 [binder, in Coq.Structures.OrderedTypeEx]

y:87 [binder, in Coq.micromega.Tauto]

y:87 [binder, in Coq.Relations.Relation_Operators]

y:87 [binder, in Coq.Logic.FinFun]

y:87 [binder, in Coq.FSets.FSetCompat]

y:87 [binder, in Coq.Structures.OrdersFacts]

y:87 [binder, in Coq.Reals.Cos_plus]

y:870 [binder, in Coq.ssr.ssrbool]

y:872 [binder, in Coq.ssr.ssrbool]

y:874 [binder, in Coq.ssr.ssrbool]

y:876 [binder, in Coq.ssr.ssrbool]

y:878 [binder, in Coq.ssr.ssrbool]

y:88 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:88 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:88 [binder, in Coq.Floats.SpecFloat]

y:88 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:88 [binder, in Coq.Reals.Rsqrt_def]

y:88 [binder, in Coq.Classes.CRelationClasses]

y:88 [binder, in Coq.Reals.Ranalysis5]

y:88 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:88 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:887 [binder, in Coq.ssr.ssrbool]

y:889 [binder, in Coq.ssr.ssrbool]

y:89 [binder, in Coq.Program.Wf]

y:89 [binder, in Coq.Reals.Exp_prop]

y:89 [binder, in Coq.Logic.ChoiceFacts]

y:89 [binder, in Coq.MSets.MSetGenTree]

y:89 [binder, in Coq.Structures.OrderedType]

y:89 [binder, in Coq.setoid_ring.Ring_theory]

y:89 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:89 [binder, in Coq.FSets.FSetCompat]

y:89 [binder, in Coq.Structures.OrdersFacts]

y:89 [binder, in Coq.Reals.Cos_plus]

y:890 [binder, in Coq.ssr.ssrbool]

y:892 [binder, in Coq.ssr.ssrbool]

y:895 [binder, in Coq.ssr.ssrbool]

y:897 [binder, in Coq.ssr.ssrbool]

y:898 [binder, in Coq.ssr.ssrbool]

y:9 [binder, in Coq.Relations.Operators_Properties]

y:9 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:9 [binder, in Coq.Logic.Eqdep_dec]

y:9 [binder, in Coq.Arith.Bool_nat]

y:9 [binder, in Coq.Logic.SetoidChoice]

y:9 [binder, in Coq.Reals.R_sqrt]

y:9 [binder, in Coq.Logic.ChoiceFacts]

y:9 [binder, in Coq.QArith.Qreals]

y:9 [binder, in Coq.Reals.Abstract.ConstructiveAbs]

y:9 [binder, in Coq.Sets.Partial_Order]

y:9 [binder, in Coq.Classes.CRelationClasses]

y:9 [binder, in Coq.Reals.Cauchy.ConstructiveExtra]

y:9 [binder, in Coq.Structures.Equalities]

y:9 [binder, in Coq.Bool.BoolEq]

y:9 [binder, in Coq.Strings.Byte]

y:9 [binder, in Coq.Setoids.Setoid]

y:9 [binder, in Coq.Reals.R_sqr]

y:9 [binder, in Coq.Reals.ClassicalConstructiveReals]

y:9 [binder, in Coq.Logic.FinFun]

y:9 [binder, in Coq.Sets.Powerset]

y:90 [binder, in Coq.Program.Wf]

y:90 [binder, in Coq.QArith.Qcanon]

y:90 [binder, in Coq.FSets.FSetDecide]

y:90 [binder, in Coq.MSets.MSetDecide]

y:90 [binder, in Coq.Lists.ListSet]

y:90 [binder, in Coq.Reals.Ranalysis5]

y:90 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:90 [binder, in Coq.Reals.ClassicalDedekindReals]

y:900 [binder, in Coq.ssr.ssrbool]

y:903 [binder, in Coq.ssr.ssrbool]

y:905 [binder, in Coq.ssr.ssrbool]

y:906 [binder, in Coq.ssr.ssrbool]

y:908 [binder, in Coq.ssr.ssrbool]

y:91 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:91 [binder, in Coq.setoid_ring.Ncring]

y:91 [binder, in Coq.micromega.Tauto]

y:91 [binder, in Coq.Structures.OrdersFacts]

y:91 [binder, in Coq.Reals.Cos_plus]

y:911 [binder, in Coq.ssr.ssrbool]

y:913 [binder, in Coq.ssr.ssrbool]

y:914 [binder, in Coq.ssr.ssrbool]

y:916 [binder, in Coq.ssr.ssrbool]

y:919 [binder, in Coq.ssr.ssrbool]

y:92 [binder, in Coq.QArith.Qcanon]

y:92 [binder, in Coq.Logic.Eqdep_dec]

y:92 [binder, in Coq.Structures.OrderedType]

y:92 [binder, in Coq.Reals.Ratan]

y:92 [binder, in Coq.Reals.Ranalysis5]

y:92 [binder, in Coq.setoid_ring.Ring_theory]

y:92 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:92 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:921 [binder, in Coq.ssr.ssrbool]

y:922 [binder, in Coq.ssr.ssrbool]

y:924 [binder, in Coq.ssr.ssrbool]

y:927 [binder, in Coq.ssr.ssrbool]

y:929 [binder, in Coq.ssr.ssrbool]

y:93 [binder, in Coq.Sorting.PermutSetoid]

y:93 [binder, in Coq.MSets.MSetWeakList]

y:93 [binder, in Coq.MSets.MSetGenTree]

y:93 [binder, in Coq.Lists.ListSet]

y:93 [binder, in Coq.Reals.Cos_rel]

y:93 [binder, in Coq.Reals.ClassicalDedekindReals]

y:93 [binder, in Coq.Lists.SetoidList]

y:93 [binder, in Coq.Structures.OrdersFacts]

y:930 [binder, in Coq.ssr.ssrbool]

y:932 [binder, in Coq.ssr.ssrbool]

y:932 [binder, in Coq.FSets.FMapAVL]

y:936 [binder, in Coq.FSets.FMapAVL]

y:94 [binder, in Coq.QArith.Qcanon]

y:94 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:94 [binder, in Coq.Logic.Eqdep_dec]

y:94 [binder, in Coq.Floats.SpecFloat]

y:94 [binder, in Coq.Classes.CRelationClasses]

y:94 [binder, in Coq.Reals.Ranalysis5]

y:94 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:94 [binder, in Coq.setoid_ring.Ncring]

y:942 [binder, in Coq.FSets.FMapAVL]

y:946 [binder, in Coq.FSets.FMapAVL]

y:95 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:95 [binder, in Coq.Reals.Rsqrt_def]

y:95 [binder, in Coq.Init.Nat]

y:95 [binder, in Coq.Logic.Hurkens]

y:95 [binder, in Coq.Reals.Rtopology]

y:95 [binder, in Coq.Structures.OrderedType]

y:95 [binder, in Coq.Reals.PSeries_reg]

y:95 [binder, in Coq.setoid_ring.Ring_theory]

y:95 [binder, in Coq.Structures.OrdersFacts]

y:952 [binder, in Coq.FSets.FMapAVL]

y:958 [binder, in Coq.FSets.FMapAVL]

y:96 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:96 [binder, in Coq.Lists.ListSet]

y:96 [binder, in Coq.Reals.PSeries_reg]

y:96 [binder, in Coq.Reals.Ratan]

y:96 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:962 [binder, in Coq.Init.Logic]

y:964 [binder, in Coq.FSets.FMapAVL]

y:97 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

y:97 [binder, in Coq.QArith.Qcanon]

y:97 [binder, in Coq.Logic.Hurkens]

y:97 [binder, in Coq.MSets.MSetGenTree]

y:97 [binder, in Coq.Structures.OrderedType]

y:97 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:97 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:97 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:97 [binder, in Coq.Relations.Relation_Operators]

y:97 [binder, in Coq.Structures.OrdersFacts]

y:970 [binder, in Coq.FSets.FMapAVL]

y:976 [binder, in Coq.FSets.FMapAVL]

y:98 [binder, in Coq.Program.Wf]

y:98 [binder, in Coq.Logic.ConstructiveEpsilon]

y:98 [binder, in Coq.Reals.Rfunctions]

y:98 [binder, in Coq.FSets.FMapFacts]

y:98 [binder, in Coq.Reals.Ranalysis5]

y:984 [binder, in Coq.FSets.FMapAVL]

y:989 [binder, in Coq.FSets.FMapAVL]

y:99 [binder, in Coq.FSets.FSetBridge]

y:99 [binder, in Coq.Floats.SpecFloat]

y:99 [binder, in Coq.Reals.RiemannInt]

y:99 [binder, in Coq.FSets.FMapInterface]

y:99 [binder, in Coq.ssr.ssreflect]

y:99 [binder, in Coq.Structures.OrderedType]

y:99 [binder, in Coq.Lists.ListSet]

y:99 [binder, in Coq.Reals.Ratan]

y:99 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

y:99 [binder, in Coq.Structures.OrdersFacts]

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 | (72746 entries) |

Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1016 entries) |

Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (47311 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 | (787 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 | (1547 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 | (584 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 | (11763 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (959 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (627 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (308 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (475 entries) |

Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (492 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 | (903 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 | (1448 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 | (4360 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (166 entries) |