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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

## Y

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

ybound:51 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

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

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

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':112 [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':34 [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':52 [binder, in Coq.Logic.Decidable]

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

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

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

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

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

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

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

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.Wellfounded.Lexicographic_Product]

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

y0:23 [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:625 [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:176 [binder, in Coq.Init.Logic]

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

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

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

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

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

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

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

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

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

y1:324 [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:356 [binder, in Coq.Lists.List]

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

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

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:89 [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:177 [binder, in Coq.Init.Logic]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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:90 [binder, in Coq.Init.Datatypes]

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

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

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

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

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

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

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

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

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.QArith.Qreals]

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.Reals.Cauchy.ConstructiveCauchyReals]

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.Structures.OrdersFacts]

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

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

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

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

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

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

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

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

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

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

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

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:1011 [binder, in Coq.Lists.List]

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

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.Arith.PeanoNat]

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.QArith.QArith_base]

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

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

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

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

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

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.Numbers.Cyclic.Int63.Int63]

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

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

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

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

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

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

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

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

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

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

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

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

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.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.QArith.QArith_base]

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

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

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

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.QArith.Qcanon]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.Init.Logic_Type]

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.Cauchy.ConstructiveCauchyRealsMult]

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.Numbers.Cyclic.Int63.Int63]

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

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

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:111 [binder, in Coq.Program.Wf]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.Numbers.Cyclic.Int63.Int63]

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

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

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

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

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

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

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.QArith.QArith_base]

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

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

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:1154 [binder, in Coq.FSets.FMapAVL]

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

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

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

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.QArith.QArith_base]

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

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.Reals.RiemannInt]

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

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.Logic.Hurkens]

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

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

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

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

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

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.Logic.SetoidChoice]

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

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

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

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.ZArith.Zbool]

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.Logic.Eqdep_dec]

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.Structures.OrdersFacts]

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

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

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

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

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

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

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

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.FSets.FMapFacts]

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

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

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.Relations.Relation_Operators]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.Reals.Cauchy.ConstructiveCauchyReals]

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

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.Reals.Rbasic_fun]

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

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

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

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

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

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

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

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

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

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

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.ConstructiveLUB]

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

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

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

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.MSets.MSetDecide]

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

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

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.Reals.Cauchy.ConstructiveCauchyReals]

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

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

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.Reals.Abstract.ConstructiveReals]

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

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

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

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.Init.Logic]

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.MVT]

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.FSets.FSetEqProperties]

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

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

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

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

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

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

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

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

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

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.Relations.Relation_Operators]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.Logic.Eqdep_dec]

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

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

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.Structures.OrdersFacts]

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

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

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

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

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

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

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

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

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

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

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

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

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.Arith.Wf_nat]

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.Logic.ChoiceFacts]

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

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

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

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

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.Structures.OrderedType]

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

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.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.Reals.Abstract.ConstructiveReals]

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

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

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.Numbers.Cyclic.Int63.Int63]

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

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

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

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

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: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.Abstract.ConstructiveReals]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.ssr.ssrfun]

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

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

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

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

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

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

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.QArith.QArith_base]

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.SeqProp]

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

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

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.Wellfounded.Lexicographic_Product]

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

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

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

y:15 [binder, in Coq.Init.Logic_Type]

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.Numbers.HexadecimalQ]

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

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

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.Numbers.Cyclic.Int63.Int63]

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

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

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

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:152 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.Structures.OrdersFacts]

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

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

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

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

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

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

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.QArith.Qreals]

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

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

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.Numbers.HexadecimalQ]

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

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

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

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.Logic.Eqdep_dec]

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:160 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

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

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.Numbers.Cyclic.Int63.Int63]

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

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

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:163 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

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: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.FSets.FMapAVL]

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

y:166 [binder, in Coq.ZArith.Znumtheory]

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

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

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.Rpower]

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.micromega.ZifyBool]

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

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

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

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

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.QArith.Qround]

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

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.ssr.ssrfun]

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:171 [binder, in Coq.Reals.MVT]

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

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

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

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

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

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

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

y:175 [binder, in Coq.Vectors.VectorSpec]

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.setoid_ring.Ncring]

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

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

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

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

y:179 [binder, in Coq.Vectors.Fin]

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

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

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.Init.Wf]

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

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

y:18 [binder, in Coq.Reals.Rdefinitions]

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.FSets.FSetBridge]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

y:186 [binder, in Coq.micromega.ZMicromega]

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

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

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

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

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

y:188 [binder, in Coq.micromega.RingMicromega]

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

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

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.Reals.Ranalysis5]

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.FSets.FMapFacts]

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

y:19 [binder, in Coq.Wellfounded.Lexicographic_Product]

y:19 [binder, in Coq.micromega.ZifyBool]

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

y:19 [binder, in Coq.Init.Logic_Type]

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.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.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.Arith.PeanoNat]

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

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

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.micromega.RingMicromega]

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

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

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

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

y:194 [binder, in Coq.micromega.RingMicromega]

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

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:194 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

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

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

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

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

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

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

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.Reals.Rfunctions]

y:198 [binder, in Coq.FSets.FMapPositive]

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

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: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.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.FSets.FSetFacts]

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.Cauchy.ConstructiveCauchyAbs]

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.Numbers.Cyclic.Int63.Int63]

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.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.Sets.Multiset]

y:20 [binder, in Coq.Classes.DecidableClass]

y:20 [binder, in Coq.Sets.Image]

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

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

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

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

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

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

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.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.Lists.SetoidList]

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

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

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.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:208 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

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

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.QArith.QArith_base]

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

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: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.Logic.JMeq]

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

y:21 [binder, in Coq.Wellfounded.Lexicographic_Product]

y:21 [binder, in Coq.micromega.ZifyBool]

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

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.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.Cauchy.ConstructiveCauchyReals]

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.Reals.Cauchy.ConstructiveCauchyRealsMult]

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.Numbers.Cyclic.Int63.Int63]

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.QArith.QArith_base]

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

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

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:213 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:213 [binder, in Coq.micromega.ZMicromega]

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

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

y:214 [binder, in Coq.Reals.Ranalysis1]

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

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.QArith.QArith_base]

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.Numbers.Cyclic.Int63.Int63]

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:217 [binder, in Coq.QArith.QArith_base]

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:219 [binder, in Coq.QArith.QArith_base]

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.ConstructiveCauchyAbs]

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

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.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.Sets.Powerset_facts]

Y:22 [binder, in Coq.Sets.Powerset_Classical_facts]

y:22 [binder, in Coq.Classes.DecidableClass]

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

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.Reals.Ranalysis1]

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

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.Logic.ChoiceFacts]

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

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

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

y:222 [binder, in Coq.Reals.Ranalysis1]

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

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

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

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

y:224 [binder, in Coq.Reals.Ranalysis1]

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.ssr.ssrfun]

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

y:226 [binder, in Coq.Reals.Ranalysis1]

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

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

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.ZArith.Znat]

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.Abstract.ConstructivePower]

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

y:23 [binder, in Coq.micromega.ZifyBool]

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

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

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.Reals.Cauchy.ConstructiveCauchyReals]

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.Reals.Cauchy.ConstructiveCauchyRealsMult]

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:232 [binder, in Coq.Logic.ChoiceFacts]

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

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

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.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.Lists.List]

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.Reals.Cauchy.ConstructiveCauchyRealsMult]

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

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

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

y:24 [binder, in Coq.Classes.Morphisms]

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

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

y:24 [binder, in Coq.Wellfounded.Lexicographic_Product]

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

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

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.Sets.Permut]

y:24 [binder, in Coq.Reals.RList]

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.Lists.List]

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

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

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

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

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.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:242 [binder, in Coq.FSets.FSetProperties]

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

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

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

y:244 [binder, in Coq.MSets.MSetProperties]

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

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

y:244 [binder, in Coq.FSets.FSetProperties]

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

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

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:247 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

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.Numbers.Cyclic.Int63.Int63]

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

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.Numbers.Natural.Abstract.NDefOps]

y:25 [binder, in Coq.Wellfounded.Lexicographic_Product]

y:25 [binder, in Coq.micromega.ZifyBool]

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

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

y:25 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]

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

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.Reals.Cauchy.ConstructiveCauchyRealsMult]

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.QArith.QArith_base]

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

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:252 [binder, in Coq.Init.Logic]

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.Numbers.Cyclic.Int63.Int63]

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.Reals.Ranalysis5]

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.Lists.SetoidList]

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

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

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

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

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.FSets.FSetPositive]

y:257 [binder, in Coq.FSets.FSetProperties]

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

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:258 [binder, in Coq.micromega.ZMicromega]

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.QArith.QArith_base]

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.QArith.Qcabs]

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

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

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

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

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

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

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.Reals.PSeries_reg]

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

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

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

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

y:260 [binder, in Coq.Logic.ClassicalFacts]

y:260 [binder, in Coq.micromega.Tauto]

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

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

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

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

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

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

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

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

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.Init.Logic]

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

y:265 [binder, in Coq.setoid_ring.Ncring_tac]

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

y:265 [binder, in Coq.micromega.Tauto]

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

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

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

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

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

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

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

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

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

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

y:268 [binder, in Coq.micromega.ZMicromega]

y:268 [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.Structures.OrdersAlt]

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

y:27 [binder, in Coq.micromega.ZifyBool]

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

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

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.Logic.ClassicalDescription]

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.Reals.Cauchy.ConstructiveCauchyRealsMult]

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:271 [binder, in Coq.Logic.ChoiceFacts]

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

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

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

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

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

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.Lists.SetoidList]

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

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

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

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

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

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

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.Cauchy.ConstructiveCauchyAbs]

y:28 [binder, in Coq.ZArith.Wf_Z]

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

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

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

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.Reals.R_sqr]

y:28 [binder, in Coq.ZArith.Znumtheory]

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

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

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

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

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:283 [binder, in Coq.Reals.Ranalysis1]

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

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

y:284 [binder, in Coq.Reals.Ranalysis1]

y:285 [binder, in Coq.Reals.Ranalysis1]

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

y:285 [binder, in Coq.MSets.MSetPositive]

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

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:287 [binder, in Coq.Reals.Ranalysis1]

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

y:288 [binder, in Coq.Reals.Ranalysis1]

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

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

y:289 [binder, in Coq.Reals.Ranalysis1]

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.Init.Wf]

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

y:29 [binder, in Coq.Reals.Rdefinitions]

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.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.Structures.OrdersFacts]

y:290 [binder, in Coq.Reals.Ranalysis1]

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:293 [binder, in Coq.MSets.MSetInterface]

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

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

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

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

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

y:296 [binder, in Coq.MSets.MSetInterface]

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

y:296 [binder, in Coq.MSets.MSetPositive]

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

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

y:297 [binder, in Coq.FSets.FMapPositive]

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

y:298 [binder, in Coq.ssr.ssrbool]

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

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.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.Arith.Wf_nat]

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

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

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

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

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.Sets.Multiset]

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

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

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

y:300 [binder, in Coq.MSets.MSetInterface]

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

y:302 [binder, in Coq.Reals.Ranalysis1]

y:302 [binder, in Coq.MSets.MSetInterface]

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

y:303 [binder, in Coq.Reals.Ranalysis1]

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

y:304 [binder, in Coq.Reals.Ranalysis1]

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

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

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

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

y:306 [binder, in Coq.ssr.ssrbool]

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

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

y:307 [binder, in Coq.MSets.MSetPositive]

y:308 [binder, in Coq.MSets.MSetInterface]

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

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.Classes.Morphisms]

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.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.Reals.Cauchy.ConstructiveCauchyReals]

y:31 [binder, in Coq.Sets.Image]

y:310 [binder, in Coq.Reals.Ranalysis1]

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

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

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

y:310 [binder, in Coq.ssr.ssrbool]

y:311 [binder, in Coq.Reals.Ranalysis1]

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

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

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

y:313 [binder, in Coq.MSets.MSetPositive]

y:314 [binder, in Coq.MSets.MSetInterface]

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

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

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

y:319 [binder, in Coq.MSets.MSetPositive]

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.ZArith.Wf_Z]

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.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.Floats.FloatAxioms]

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

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

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

y:32 [binder, in Coq.Classes.Equivalence]

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

y:322 [binder, in Coq.ssr.ssrbool]

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

y:324 [binder, in Coq.ssr.ssrbool]

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

y:324 [binder, in Coq.Reals.RIneq]

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

y:325 [binder, in Coq.micromega.ZMicromega]

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

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

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

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.Logic.Eqdep_dec]

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.Reals.Cauchy.ConstructiveCauchyAbs]

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

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

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.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.Reals.Cauchy.ConstructiveCauchyReals]

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.Relations.Relation_Operators]

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

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

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

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

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

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

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

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

y:339 [binder, in Coq.MSets.MSetInterface]

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

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

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

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

y:34 [binder, in Coq.Numbers.DecimalQ]

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.Sets.Infinite_sets]

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.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:344 [binder, in Coq.Reals.Rtopology]

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

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

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

y:35 [binder, in Coq.Sorting.PermutEq]

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.Reals.Cauchy.ConstructiveCauchyAbs]

y:35 [binder, in Coq.Numbers.DecimalQ]

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

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

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

y:35 [binder, in Coq.micromega.ZifyBool]

y:35 [binder, in Coq.Structures.DecidableType]

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.Reals.Cauchy.ConstructiveCauchyReals]

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:351 [binder, in Coq.Reals.Abstract.ConstructiveReals]

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

y:353 [binder, in Coq.MSets.MSetInterface]

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

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

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

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

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

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

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

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

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

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

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.Structures.OrdersAlt]

y:36 [binder, in Coq.ZArith.Wf_Z]

y:36 [binder, in Coq.ZArith.Zeven]

y:36 [binder, in Coq.Reals.Rdefinitions]

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

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.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.Cauchy.ConstructiveCauchyRealsMult]

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

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

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

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

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

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

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

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

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

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

y:362 [binder, in Coq.ssr.ssrbool]

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

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

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

y:364 [binder, in Coq.ssr.ssrbool]

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

y:366 [binder, in Coq.ssr.ssrbool]

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

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

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

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

y:368 [binder, in Coq.ssr.ssrbool]

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

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

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

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

y:37 [binder, in Coq.Reals.R_sqrt]

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

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

y:37 [binder, in Coq.micromega.ZifyBool]

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.Reals.Cauchy.ConstructiveCauchyReals]

y:37 [binder, in Coq.Sets.Image]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.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.Logic.JMeq]

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

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

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

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

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

y:38 [binder, in Coq.Reals.Rdefinitions]

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

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.Sets.Multiset]

y:38 [binder, in Coq.Sets.Image]

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:380 [binder, in Coq.Reals.Ranalysis5]

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

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

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

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

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

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:388 [binder, in Coq.Logic.ChoiceFacts]

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

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

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

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

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.setoid_ring.InitialRing]

y:39 [binder, in Coq.micromega.ZifyBool]

y:39 [binder, in Coq.Structures.DecidableType]

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.Reals.Abstract.ConstructiveRealsMorphisms]

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

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

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

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

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

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

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

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

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

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

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

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:399 [binder, in Coq.Init.Logic]

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.QArith.Qreals]

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.Eqdep_dec]

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.Reals.ArithProp]

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

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

y:40 [binder, in Coq.ZArith.Wf_Z]

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

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.Logic.ClassicalDescription]

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:401 [binder, in Coq.ZArith.BinInt]

y:402 [binder, in Coq.Reals.Ranalysis1]

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

y:403 [binder, in Coq.Reals.Ranalysis1]

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.ZArith.BinInt]

y:405 [binder, in Coq.Reals.Ranalysis1]

y:406 [binder, in Coq.Reals.Ranalysis1]

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

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

y:407 [binder, in Coq.Reals.Ranalysis1]

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.ZArith.BinIntDef]

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

y:41 [binder, in Coq.Reals.R_sqrt]

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

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.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:414 [binder, in Coq.ZArith.BinInt]

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.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.Logic.JMeq]

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.Structures.OrdersTac]

y:42 [binder, in Coq.PArith.BinPosDef]

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

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:423 [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.Reals.Rtopology]

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

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

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

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

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

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.Logic.ClassicalEpsilon]

y:43 [binder, in Coq.Reals.R_sqrt]

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

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

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

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.Reals.Cauchy.ConstructiveCauchyReals]

y:43 [binder, in Coq.Reals.RList]

y:43 [binder, in Coq.Logic.Diaconescu]

y:43 [binder, in Coq.Reals.Rgeom]

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

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

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

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

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

y:44 [binder, in Coq.setoid_ring.Ncring_initial]

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

y:44 [binder, in Coq.micromega.RingMicromega]

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.Reals.Abstract.ConstructiveRealsMorphisms]

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

y:449 [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.Logic.Eqdep_dec]

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

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

y:45 [binder, in Coq.ZArith.Wf_Z]

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.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.micromega.ZifyInst]

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

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

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

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

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.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.JMeq]

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.FSets.FSetCompat]

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

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

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

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

y:468 [binder, in Coq.ssr.ssrbool]

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

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

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

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

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

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:471 [binder, in Coq.ssr.ssrbool]

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

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

y:473 [binder, in Coq.ssr.ssrbool]

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

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

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

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

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

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

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

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

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.Logic.ChoiceFacts]

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

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.Lists.SetoidList]

y:481 [binder, in Coq.ssr.ssrbool]

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:488 [binder, in Coq.Lists.List]

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

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

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

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:490 [binder, in Coq.ssr.ssrbool]

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:499 [binder, in Coq.ssr.ssrbool]

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.Qfield]

y:5 [binder, in Coq.Reals.Rdefinitions]

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

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.ZifyInst]

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

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

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.Reals.Cauchy.ConstructiveRcomplete]

y:50 [binder, in Coq.ZArith.Wf_Z]

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

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

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

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

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

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

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

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

y:503 [binder, in Coq.ssr.ssrbool]

y:504 [binder, in Coq.ssr.ssrbool]

y:508 [binder, in Coq.ssr.ssrbool]

y:509 [binder, in Coq.MSets.MSetAVL]

y:51 [binder, in Coq.Logic.Decidable]

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.Logic.JMeq]

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.QArith.Qpower]

y:51 [binder, in Coq.Sorting.Mergesort]

y:510 [binder, in Coq.ssr.ssrbool]

y:512 [binder, in Coq.ssr.ssrbool]

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

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

y:516 [binder, in Coq.ssr.ssrbool]

y:518 [binder, in Coq.ssr.ssrbool]

y:519 [binder, in Coq.MSets.MSetAVL]

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

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

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

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

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

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

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.ConstructiveCauchyReals]

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

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

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

y:522 [binder, in Coq.ssr.ssrbool]

y:522 [binder, in Coq.MSets.MSetAVL]

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

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

y:527 [binder, in Coq.ssr.ssrbool]

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.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.FSets.FSetPositive]

y:53 [binder, in Coq.MSets.MSetPositive]

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

y:53 [binder, in Coq.Logic.Diaconescu]

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

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

y:530 [binder, in Coq.ssr.ssrbool]

y:530 [binder, in Coq.MSets.MSetAVL]

y:532 [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.Reals.Cauchy.ConstructiveCauchyAbs]

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

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.Structures.OrdersTac]

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

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

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

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

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

y:541 [binder, in Coq.MSets.MSetAVL]

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

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

y:549 [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.FSets.FMapFacts]

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

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.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:555 [binder, in Coq.ssr.ssrbool]

y:555 [binder, in Coq.MSets.MSetAVL]

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

y:559 [binder, in Coq.ssr.ssrbool]

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

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

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

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.Cauchy.ConstructiveCauchyReals]

y:56 [binder, in Coq.Logic.Diaconescu]

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

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

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.Lists.List]

y:565 [binder, in Coq.MSets.MSetAVL]

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

y:567 [binder, in Coq.ssr.ssrbool]

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

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.FSets.FSetDecide]

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

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

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

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.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.Lists.List]

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

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

y:576 [binder, in Coq.ssr.ssrbool]

y:576 [binder, in Coq.Reals.RIneq]

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

y:578 [binder, in Coq.Reals.RIneq]

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.Reals.Cauchy.ConstructiveCauchyAbs]

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.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:580 [binder, in Coq.Reals.RIneq]

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

y:582 [binder, in Coq.MSets.MSetAVL]

y:582 [binder, in Coq.Reals.RIneq]

y:586 [binder, in Coq.MSets.MSetAVL]

y:586 [binder, in Coq.Reals.RIneq]

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

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.ZArith.Zbool]

y:59 [binder, in Coq.Sets.Multiset]

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

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

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

y:594 [binder, in Coq.MSets.MSetAVL]

y:595 [binder, in Coq.MSets.MSetAVL]

y:596 [binder, in Coq.MSets.MSetAVL]

y:597 [binder, in Coq.MSets.MSetAVL]

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.Init.Wf]

y:6 [binder, in Coq.micromega.ZifyBool]

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

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

y:6 [binder, in Coq.NArith.BinNat]

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

y:6 [binder, in Coq.Logic.RelationalChoice]

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.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.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.Reals.Cauchy.ConstructiveCauchyAbs]

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

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

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.Rbasic_fun]

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

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

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

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

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

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

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

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

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

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

y:608 [binder, in Coq.MSets.MSetAVL]

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

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

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

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.Reals.Cauchy.ConstructiveCauchyReals]

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

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

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

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

y:611 [binder, in Coq.MSets.MSetAVL]

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

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.ConstructiveCauchyAbs]

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

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

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

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

y:622 [binder, in Coq.MSets.MSetAVL]

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

y:625 [binder, in Coq.MSets.MSetAVL]

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

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

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

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.MSets.MSetDecide]

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

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

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

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

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

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

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

y:631 [binder, in Coq.ssr.ssrbool]

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

y:633 [binder, in Coq.ssr.ssrbool]

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

y:634 [binder, in Coq.MSets.MSetAVL]

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

y:635 [binder, in Coq.ssr.ssrbool]

y:637 [binder, in Coq.ssr.ssrbool]

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.Reals.Cauchy.ConstructiveCauchyAbs]

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.Reals.ClassicalDedekindReals]

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

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

y:65 [binder, in Coq.Sets.Uniset]

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

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

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.micromega.ZifyClasses]

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

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:67 [binder, in Coq.Program.Wf]

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

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

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.Reals.ClassicalDedekindReals]

y:670 [binder, in Coq.ssr.ssrbool]

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

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

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.Reals.Cauchy.ConstructiveCauchyAbs]

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:685 [binder, in Coq.Lists.List]

y:685 [binder, in Coq.ssr.ssrbool]

y:687 [binder, in Coq.ssr.ssrbool]

y:689 [binder, in Coq.ssr.ssrbool]

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

y:69 [binder, in Coq.QArith.Qcanon]

y:69 [binder, in Coq.Logic.Eqdep_dec]

y:69 [binder, in Coq.Reals.Ranalysis4]

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.Cauchy.ConstructiveCauchyReals]

y:69 [binder, in Coq.PArith.BinPosDef]

y:69 [binder, in Coq.Structures.OrdersFacts]

y:691 [binder, in Coq.ssr.ssrbool]

y:694 [binder, in Coq.ssr.ssrbool]

y:696 [binder, in Coq.Init.Specif]

y:696 [binder, in Coq.ssr.ssrbool]

y:698 [binder, in Coq.ssr.ssrbool]

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.Reals.R_sqrt]

y:7 [binder, in Coq.Logic.ChoiceFacts]

y:7 [binder, in Coq.Wellfounded.Lexicographic_Product]

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.Reals.Cauchy.ConstructiveCauchyReals]

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.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.Reals.Abstract.ConstructiveRealsMorphisms]

y:700 [binder, in Coq.ssr.ssrbool]

y:702 [binder, in Coq.Init.Specif]

y:702 [binder, in Coq.ssr.ssrbool]

y:704 [binder, in Coq.ssr.ssrbool]

y:706 [binder, in Coq.ssr.ssrbool]

y:708 [binder, in Coq.ssr.ssrbool]

y:71 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:71 [binder, in Coq.FSets.FMapFacts]

y:71 [binder, in Coq.Logic.ChoiceFacts]

y:71 [binder, in Coq.ssr.ssrfun]

y:71 [binder, in Coq.Reals.Ranalysis5]

y:71 [binder, in Coq.Reals.R_sqr]

y:710 [binder, in Coq.ssr.ssrbool]

y:712 [binder, in Coq.ssr.ssrbool]

y:714 [binder, in Coq.ssr.ssrbool]

y:716 [binder, in Coq.Init.Specif]

y:716 [binder, in Coq.ssr.ssrbool]

y:718 [binder, in Coq.ssr.ssrbool]

y:72 [binder, in Coq.Relations.Operators_Properties]

y:72 [binder, in Coq.QArith.Qcanon]

y:72 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

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.Reals.Cauchy.ConstructiveCauchyReals]

y:72 [binder, in Coq.Logic.Diaconescu]

y:72 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

y:72 [binder, in Coq.Structures.OrdersFacts]

y:720 [binder, in Coq.ssr.ssrbool]

y:722 [binder, in Coq.ssr.ssrbool]

y:724 [binder, in Coq.ssr.ssrbool]

y:726 [binder, in Coq.ssr.ssrbool]

y:728 [binder, in Coq.ssr.ssrbool]

y:73 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:73 [binder, in Coq.micromega.RingMicromega]

y:73 [binder, in Coq.Reals.Exp_prop]

y:73 [binder, in Coq.Logic.JMeq]

y:73 [binder, in Coq.Logic.Diaconescu]

y:73 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:73 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:730 [binder, in Coq.ssr.ssrbool]

y:732 [binder, in Coq.ssr.ssrbool]

y:734 [binder, in Coq.ssr.ssrbool]

y:736 [binder, in Coq.ssr.ssrbool]

y:74 [binder, in Coq.QArith.Qcanon]

y:74 [binder, in Coq.Reals.Rfunctions]

y:74 [binder, in Coq.Classes.RelationClasses]

y:74 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

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.Abstract.ConstructiveRealsMorphisms]

y:749 [binder, in Coq.ssr.ssrbool]

y:75 [binder, in Coq.FSets.FSetDecide]

y:75 [binder, in Coq.FSets.FMapFacts]

y:75 [binder, in Coq.MSets.MSetDecide]

y:75 [binder, in Coq.Init.Wf]

y:75 [binder, in Coq.Reals.Rbasic_fun]

y:75 [binder, in Coq.Reals.Ranalysis5]

y:75 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:75 [binder, in Coq.Logic.Diaconescu]

y:75 [binder, in Coq.Relations.Relation_Operators]

y:75 [binder, in Coq.Structures.OrdersFacts]

y:751 [binder, in Coq.ssr.ssrbool]

y:753 [binder, in Coq.ssr.ssrbool]

y:755 [binder, in Coq.ssr.ssrbool]

y:76 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:76 [binder, in Coq.Reals.Ranalysis4]

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.Logic.Diaconescu]

y:76 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:76 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:76 [binder, in Coq.QArith.QArith_base]

y:762 [binder, in Coq.ssr.ssrbool]

y:764 [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.Logic.Eqdep_dec]

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: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.Structures.OrderedType]

y:78 [binder, in Coq.Reals.Ratan]

y:78 [binder, in Coq.setoid_ring.Ring_theory]

y:78 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

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.Reals.Cauchy.ConstructiveCauchyAbs]

y:79 [binder, in Coq.Logic.JMeq]

y:79 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

y:79 [binder, in Coq.Logic.ChoiceFacts]

y:79 [binder, in Coq.MSets.MSetWeakList]

y:79 [binder, in Coq.Reals.Rtopology]

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.Program.Subset]

y:8 [binder, in Coq.Init.Wf]

y:8 [binder, in Coq.micromega.ZifyBool]

y:8 [binder, in Coq.QArith.Qreals]

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.ZArith.Zpow_alt]

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.Reals.ROrderedType]

y:8 [binder, in Coq.Floats.FloatAxioms]

y:8 [binder, in Coq.Reals.Cos_rel]

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.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.Cauchy.ConstructiveCauchyRealsMult]

y:80 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:800 [binder, in Coq.ssr.ssrbool]

y:802 [binder, in Coq.ssr.ssrbool]

y:804 [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.Reals.Rpower]

y:81 [binder, in Coq.setoid_ring.Ring_theory]

y:81 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:81 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:81 [binder, in Coq.Reals.ClassicalDedekindReals]

y:81 [binder, in Coq.QArith.QArith_base]

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.Logic.Eqdep_dec]

y:82 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:82 [binder, in Coq.Logic.ChoiceFacts]

y:82 [binder, in Coq.Arith.PeanoNat]

y:82 [binder, in Coq.Structures.OrderedType]

y:824 [binder, in Coq.Lists.List]

y:83 [binder, in Coq.micromega.ZifyClasses]

y:83 [binder, in Coq.Classes.CRelationClasses]

y:83 [binder, in Coq.Reals.Rbasic_fun]

y:83 [binder, in Coq.Structures.EqualitiesFacts]

y:83 [binder, in Coq.PArith.BinPosDef]

y:83 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:83 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:83 [binder, in Coq.Relations.Relation_Operators]

y:83 [binder, in Coq.QArith.QArith_base]

y:83 [binder, in Coq.Structures.OrdersFacts]

y:84 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:84 [binder, in Coq.Logic.Eqdep_dec]

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.Reals.Cauchy.ConstructiveCauchyReals]

y:84 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]

y:84 [binder, in Coq.Logic.FinFun]

y:85 [binder, in Coq.QArith.Qcanon]

y:85 [binder, in Coq.Classes.RelationClasses]

y:85 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]

y:85 [binder, in Coq.setoid_ring.Ring_theory]

y:85 [binder, in Coq.PArith.BinPosDef]

y:85 [binder, in Coq.Relations.Relation_Operators]

y:85 [binder, in Coq.Structures.OrdersFacts]

y:86 [binder, in Coq.Reals.Abstract.ConstructiveReals]

y:86 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:86 [binder, in Coq.MSets.MSetWeakList]

y:86 [binder, in Coq.Structures.OrderedTypeEx]

y:86 [binder, in Coq.Structures.OrderedType]

y:86 [binder, in Coq.Reals.Rbasic_fun]

y:86 [binder, in Coq.Reals.Ranalysis5]

y:86 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]

y:86 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:86 [binder, in Coq.QArith.QArith_base]

y:86 [binder, in Coq.Lists.SetoidList]

y:87 [binder, in Coq.QArith.Qcanon]

y:87 [binder, in Coq.Reals.Ranalysis4]

y:87 [binder, in Coq.Reals.Exp_prop]

y:87 [binder, in Coq.omega.OmegaLemmas]

y:87 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]

y:87 [binder, in Coq.micromega.ZifyInst]

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:88 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

y:88 [binder, in Coq.Floats.SpecFloat]

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.QArith.QArith_base]

y:89 [binder, in Coq.Program.Wf]

y:89 [binder, in Coq.Logic.Eqdep_dec]

y:89 [binder, in Coq.Reals.Exp_prop]

y:89 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

y:89 [binder, in Coq.Structures.OrderedTypeEx]

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: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.Reals.Abstract.ConstructiveAbs]

y:9 [binder, in Coq.Logic.ClassicalUniqueChoice]

y:9 [binder, in Coq.Sets.Partial_Order]

y:9 [binder, in Coq.Classes.CRelationClasses]

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.Reals.Abstract.ConstructiveReals]

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.Cauchy.ConstructiveCauchyReals]

y:90 [binder, in Coq.micromega.ZifyInst]

y:90 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

y:90 [binder, in Coq.QArith.QArith_base]

y:91 [binder, in Coq.Lists.List]

y:91 [binder, in Coq.setoid_ring.Ncring]

y:91 [binder, in Coq.Structures.OrdersFacts]

y:91 [binder, in Coq.Reals.Cos_plus]

y:92 [binder, in Coq.QArith.Qcanon]

y:92 [binder, in Coq.Logic.ChoiceFacts]

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.QArith.QArith_base]

y:93 [binder, in Coq.Logic.Eqdep_dec]

y:93 [binder, in Coq.Sorting.PermutSetoid]

y:93 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

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.Cauchy.ConstructiveCauchyReals]

y:93 [binder, in Coq.Reals.Cos_rel]

y:93 [binder, in Coq.Lists.SetoidList]

y:93 [binder, in Coq.Structures.OrdersFacts]

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.Floats.SpecFloat]

y:94 [binder, in Coq.Classes.CRelationClasses]

y:94 [binder, in Coq.Reals.PSeries_reg]

y:94 [binder, in Coq.Reals.Ranalysis5]

y:94 [binder, in Coq.setoid_ring.Ncring]

y:94 [binder, in Coq.QArith.QArith_base]

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.setoid_ring.Ring_theory]

y:95 [binder, in Coq.Init.Logic]

y:95 [binder, in Coq.micromega.ZifyInst]

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.Reals.Rfunctions]

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.QArith.QArith_base]

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.Reals.Cauchy.ConstructiveCauchyAbs]

y:97 [binder, in Coq.Numbers.Cyclic.Int63.Int63]

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.Numbers.Cyclic.Abstract.CyclicAxioms]

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.Eqdep_dec]

y:98 [binder, in Coq.FSets.FMapFacts]

y:98 [binder, in Coq.Reals.Ranalysis5]

y:98 [binder, in Coq.QArith.QArith_base]

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.Structures.OrderedType]

y:99 [binder, in Coq.Lists.ListSet]

y:99 [binder, in Coq.Reals.Ratan]

y:99 [binder, in Coq.Structures.OrdersFacts]

y:994 [binder, in Coq.Lists.List]

Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (68863 entries) |

Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (985 entries) |

Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (44709 entries) |

Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (761 entries) |

Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1497 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (570 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11380 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (976 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (603 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (298 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (460 entries) |

Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (476 entries) |

Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (811 entries) |

Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1157 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4018 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (162 entries) |