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

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

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

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

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

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

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

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

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

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

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

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

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

## F

f [projection, in Coq.Reals.Rtopology]f [definition, in Coq.Logic.Berardi]

F [projection, in Coq.Logic.ClassicalFacts]

F [definition, in Coq.micromega.ZMicromega]

fab:30 [binder, in Coq.Numbers.NaryFunctions]

fact [definition, in Coq.Arith.Factorial]

Factorial [library]

Facts [section, in Coq.Lists.List]

Facts [module, in Coq.FSets.FMapFacts]

Facts [module, in Coq.MSets.MSetFacts]

Facts [module, in Coq.FSets.FSetFacts]

Facts.A [variable, in Coq.Lists.List]

fact_simpl [lemma, in Coq.Reals.Rfunctions]

fact_le [lemma, in Coq.Arith.Factorial]

fact_neq_0 [lemma, in Coq.Arith.Factorial]

fact_prodSO [lemma, in Coq.Reals.Rprod]

false [constructor, in Coq.Init.Datatypes]

False [inductive, in Coq.Init.Logic]

falseP [constructor, in Coq.Logic.ClassicalFacts]

FalseP [definition, in Coq.Logic.ClassicalFacts]

false_le [lemma, in Coq.Bool.BoolOrder]

false_predicate [definition, in Coq.Classes.RelationClasses]

false_xorb [abbreviation, in Coq.Bool.Bool]

false_hprop [lemma, in Coq.Logic.HLevels]

family [record, in Coq.Reals.Rtopology]

family_closed_set [definition, in Coq.Reals.Rtopology]

family_P1 [lemma, in Coq.Reals.Rtopology]

family_finite [definition, in Coq.Reals.Rtopology]

family_open_set [definition, in Coq.Reals.Rtopology]

Fapp [definition, in Coq.setoid_ring.Field_theory]

fast_Zred_factor6 [definition, in Coq.omega.OmegaLemmas]

fast_Zred_factor5 [definition, in Coq.omega.OmegaLemmas]

fast_Zred_factor4 [definition, in Coq.omega.OmegaLemmas]

fast_Zred_factor3 [definition, in Coq.omega.OmegaLemmas]

fast_Zred_factor2 [definition, in Coq.omega.OmegaLemmas]

fast_Zred_factor1 [definition, in Coq.omega.OmegaLemmas]

fast_Zmult_assoc_reverse [definition, in Coq.omega.OmegaLemmas]

fast_Zmult_plus_distr_l [definition, in Coq.omega.OmegaLemmas]

fast_Zopp_mult_distr_r [definition, in Coq.omega.OmegaLemmas]

fast_Zopp_plus_distr [definition, in Coq.omega.OmegaLemmas]

fast_Zmult_comm [definition, in Coq.omega.OmegaLemmas]

fast_Zopp_eq_mult_neg_1 [definition, in Coq.omega.OmegaLemmas]

fast_Zred_factor0 [definition, in Coq.omega.OmegaLemmas]

fast_OMEGA14 [definition, in Coq.omega.OmegaLemmas]

fast_OMEGA13 [definition, in Coq.omega.OmegaLemmas]

fast_OMEGA16 [definition, in Coq.omega.OmegaLemmas]

fast_OMEGA15 [definition, in Coq.omega.OmegaLemmas]

fast_OMEGA12 [definition, in Coq.omega.OmegaLemmas]

fast_OMEGA11 [definition, in Coq.omega.OmegaLemmas]

fast_OMEGA10 [definition, in Coq.omega.OmegaLemmas]

fast_Zplus_permute [definition, in Coq.omega.OmegaLemmas]

fast_Zplus_assoc [definition, in Coq.omega.OmegaLemmas]

fast_Zplus_assoc_reverse [definition, in Coq.omega.OmegaLemmas]

fast_Zplus_comm [definition, in Coq.omega.OmegaLemmas]

Fcons [definition, in Coq.setoid_ring.Field_theory]

fcons_ok [lemma, in Coq.setoid_ring.Field_theory]

Fcons0 [definition, in Coq.setoid_ring.Field_theory]

Fcons00 [definition, in Coq.setoid_ring.Field_theory]

Fcons1 [definition, in Coq.setoid_ring.Field_theory]

Fcons2 [definition, in Coq.setoid_ring.Field_theory]

fct_cte [definition, in Coq.Reals.Ranalysis1]

fct:113 [binder, in Coq.micromega.Tauto]

fct:645 [binder, in Coq.micromega.Tauto]

Fdiv_def [projection, in Coq.setoid_ring.Field_theory]

fe [projection, in Coq.Reals.RiemannInt_SF]

FEadd [constructor, in Coq.setoid_ring.Field_theory]

FEc [constructor, in Coq.setoid_ring.Field_theory]

FEdiv [constructor, in Coq.setoid_ring.Field_theory]

FEeval [definition, in Coq.setoid_ring.Field_theory]

FEI [constructor, in Coq.setoid_ring.Field_theory]

FEinv [constructor, in Coq.setoid_ring.Field_theory]

FEmul [constructor, in Coq.setoid_ring.Field_theory]

FEO [constructor, in Coq.setoid_ring.Field_theory]

FEopp [constructor, in Coq.setoid_ring.Field_theory]

FEpow [constructor, in Coq.setoid_ring.Field_theory]

FEq [constructor, in Coq.Floats.PrimFloat]

FEsub [constructor, in Coq.setoid_ring.Field_theory]

FEX [constructor, in Coq.setoid_ring.Field_theory]

fexp [definition, in Coq.Floats.SpecFloat]

FExpr [inductive, in Coq.setoid_ring.Field_theory]

fe1:291 [binder, in Coq.setoid_ring.Field_theory]

fe1:324 [binder, in Coq.setoid_ring.Field_theory]

fe1:332 [binder, in Coq.setoid_ring.Field_theory]

fe1:341 [binder, in Coq.setoid_ring.Field_theory]

fe1:348 [binder, in Coq.setoid_ring.Field_theory]

fe1:354 [binder, in Coq.setoid_ring.Field_theory]

fe1:365 [binder, in Coq.setoid_ring.Field_theory]

fe2:292 [binder, in Coq.setoid_ring.Field_theory]

fe2:325 [binder, in Coq.setoid_ring.Field_theory]

fe2:333 [binder, in Coq.setoid_ring.Field_theory]

fe2:342 [binder, in Coq.setoid_ring.Field_theory]

fe2:349 [binder, in Coq.setoid_ring.Field_theory]

fe2:355 [binder, in Coq.setoid_ring.Field_theory]

fe2:366 [binder, in Coq.setoid_ring.Field_theory]

fe:289 [binder, in Coq.setoid_ring.Field_theory]

fe:298 [binder, in Coq.setoid_ring.Field_theory]

fe:313 [binder, in Coq.setoid_ring.Field_theory]

fe:319 [binder, in Coq.setoid_ring.Field_theory]

FF [definition, in Coq.Reals.RList]

FF [constructor, in Coq.micromega.Tauto]

ff2:351 [binder, in Coq.micromega.Tauto]

ff:47 [binder, in Coq.micromega.QMicromega]

fF:82 [binder, in Coq.ssr.ssrbool]

ff:87 [binder, in Coq.micromega.RMicromega]

ff:99 [binder, in Coq.micromega.RMicromega]

FGt [constructor, in Coq.Floats.PrimFloat]

fg_id' [definition, in Coq.Logic.Adjointification]

fg_id:38 [binder, in Coq.Logic.Adjointification]

fg_id:17 [binder, in Coq.Logic.Adjointification]

fibonacci [definition, in Coq.ZArith.Zgcd_alt]

fibonacci_incr [lemma, in Coq.ZArith.Zgcd_alt]

fibonacci_pos [lemma, in Coq.ZArith.Zgcd_alt]

Field [library]

field_theory [record, in Coq.setoid_ring.Field_theory]

Field_simplify_eq_in_correct [lemma, in Coq.setoid_ring.Field_theory]

Field_simplify_eq_pow_in_correct [lemma, in Coq.setoid_ring.Field_theory]

Field_simplify_aux_ok [lemma, in Coq.setoid_ring.Field_theory]

Field_simplify_eq_pow_correct [lemma, in Coq.setoid_ring.Field_theory]

Field_simplify_eq_correct [lemma, in Coq.setoid_ring.Field_theory]

Field_correct [lemma, in Coq.setoid_ring.Field_theory]

Field_rw_pow_correct [lemma, in Coq.setoid_ring.Field_theory]

Field_rw_correct [lemma, in Coq.setoid_ring.Field_theory]

field_is_integral_domain [lemma, in Coq.setoid_ring.Field_theory]

Field_theory [library]

Field_tac [library]

filter [definition, in Coq.Lists.List]

Filtering [section, in Coq.Lists.List]

Filtering.A [variable, in Coq.Lists.List]

Filtering.eq_dec [variable, in Coq.Lists.List]

filter_ext [lemma, in Coq.Lists.List]

filter_map [lemma, in Coq.Lists.List]

filter_ext_in_iff [lemma, in Coq.Lists.List]

filter_ext_in [lemma, in Coq.Lists.List]

filter_app [lemma, in Coq.Lists.List]

filter_In [lemma, in Coq.Lists.List]

filter_split [lemma, in Coq.Lists.SetoidList]

filter_InA [lemma, in Coq.Lists.SetoidList]

filter_sort [lemma, in Coq.Lists.SetoidList]

filter:97 [binder, in Coq.Reals.Abstract.ConstructiveSum]

Fin [library]

find [definition, in Coq.Lists.List]

find [definition, in Coq.micromega.VarMap]

Find [section, in Coq.Lists.SetoidList]

findA [definition, in Coq.Lists.SetoidList]

findA_NoDupA [lemma, in Coq.Lists.SetoidList]

findex [definition, in Coq.Strings.String]

find_none [lemma, in Coq.Lists.List]

find_some [lemma, in Coq.Lists.List]

find_left_path [lemma, in Coq.Logic.WKL]

Find.A [variable, in Coq.Lists.SetoidList]

Find.B [variable, in Coq.Lists.SetoidList]

Find.eqA [variable, in Coq.Lists.SetoidList]

Find.eqA_dec [variable, in Coq.Lists.SetoidList]

Find.eqA_equiv [variable, in Coq.Lists.SetoidList]

FinFun [library]

Finite [inductive, in Coq.Sets.Finite_sets]

Finite [definition, in Coq.Logic.FinFun]

Finite_downward_closed [lemma, in Coq.Sets.Finite_sets_facts]

finite_cardinal [lemma, in Coq.Sets.Finite_sets_facts]

Finite_sets_facts.U [variable, in Coq.Sets.Finite_sets_facts]

Finite_sets_facts [section, in Coq.Sets.Finite_sets_facts]

finite_greater [lemma, in Coq.Reals.Rseries]

Finite_subset_has_lub [lemma, in Coq.Sets.Integers]

finite_image [lemma, in Coq.Sets.Image]

Finite_Empty_or_not [lemma, in Coq.Logic.FinFun]

Finite_alt [lemma, in Coq.Logic.FinFun]

Finite_sets [library]

Finite_sets_facts [library]

Finite' [definition, in Coq.Logic.FinFun]

Finv_l [projection, in Coq.setoid_ring.Field_theory]

Fin_Finite [lemma, in Coq.Logic.FinFun]

Fin2Restrict [module, in Coq.Logic.FinFun]

Fin2Restrict.extend [definition, in Coq.Logic.FinFun]

Fin2Restrict.extend_injective [lemma, in Coq.Logic.FinFun]

Fin2Restrict.extend_surjective [lemma, in Coq.Logic.FinFun]

Fin2Restrict.extend_n2f [lemma, in Coq.Logic.FinFun]

Fin2Restrict.extend_f2n [lemma, in Coq.Logic.FinFun]

Fin2Restrict.extend_ok [lemma, in Coq.Logic.FinFun]

Fin2Restrict.f2n [definition, in Coq.Logic.FinFun]

Fin2Restrict.f2n_inj [definition, in Coq.Logic.FinFun]

Fin2Restrict.f2n_n2f [definition, in Coq.Logic.FinFun]

Fin2Restrict.f2n_ok [definition, in Coq.Logic.FinFun]

Fin2Restrict.n2f [abbreviation, in Coq.Logic.FinFun]

Fin2Restrict.n2f_ext [definition, in Coq.Logic.FinFun]

Fin2Restrict.n2f_f2n [definition, in Coq.Logic.FinFun]

Fin2Restrict.restrict [definition, in Coq.Logic.FinFun]

Fin2Restrict.restrict_injective [lemma, in Coq.Logic.FinFun]

Fin2Restrict.restrict_surjective [lemma, in Coq.Logic.FinFun]

Fin2Restrict.restrict_n2f [lemma, in Coq.Logic.FinFun]

Fin2Restrict.restrict_f2n [lemma, in Coq.Logic.FinFun]

firstl [definition, in Coq.Numbers.Cyclic.Int31.Int31]

firstl_firstr [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]

firstn [definition, in Coq.Lists.List]

firstn_map [lemma, in Coq.Lists.List]

firstn_removelast [lemma, in Coq.Lists.List]

firstn_rev [lemma, in Coq.Lists.List]

firstn_skipn_rev [lemma, in Coq.Lists.List]

firstn_length [lemma, in Coq.Lists.List]

firstn_skipn [lemma, in Coq.Lists.List]

firstn_skipn_comm [lemma, in Coq.Lists.List]

firstn_firstn [lemma, in Coq.Lists.List]

firstn_app_2 [lemma, in Coq.Lists.List]

firstn_app [lemma, in Coq.Lists.List]

firstn_length_le [lemma, in Coq.Lists.List]

firstn_le_length [lemma, in Coq.Lists.List]

firstn_O [lemma, in Coq.Lists.List]

firstn_all2 [lemma, in Coq.Lists.List]

firstn_all [lemma, in Coq.Lists.List]

firstn_cons [lemma, in Coq.Lists.List]

firstn_nil [lemma, in Coq.Lists.List]

firstr [definition, in Coq.Numbers.Cyclic.Int31.Int31]

firstr_firstl [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]

first_indices_increasing [lemma, in Coq.Reals.Runcountable]

first_two_in_interval_works [lemma, in Coq.Reals.Runcountable]

first_index:49 [binder, in Coq.Reals.Runcountable]

first_two_in_interval [definition, in Coq.Reals.Runcountable]

first_in_holed_interval_works [lemma, in Coq.Reals.Runcountable]

first_in_holed_interval [definition, in Coq.Reals.Runcountable]

first_definitions.Aeq_dec [variable, in Coq.Lists.ListSet]

first_definitions.A [variable, in Coq.Lists.ListSet]

first_definitions [section, in Coq.Lists.ListSet]

Fix [definition, in Coq.Init.Wf]

Fix [projection, in Coq.Logic.ClassicalFacts]

Fix_sub_rect [lemma, in Coq.Program.Wf]

Fix_rects.equiv_lowers [variable, in Coq.Program.Wf]

Fix_F_sub_rect [lemma, in Coq.Program.Wf]

Fix_rects.f [variable, in Coq.Program.Wf]

Fix_rects.Rwf [variable, in Coq.Program.Wf]

Fix_rects.R [variable, in Coq.Program.Wf]

Fix_rects.P [variable, in Coq.Program.Wf]

Fix_rects.A [variable, in Coq.Program.Wf]

Fix_rects [section, in Coq.Program.Wf]

fix_sub_eq [lemma, in Coq.Program.Wf]

Fix_eq [lemma, in Coq.Program.Wf]

Fix_F_inv [lemma, in Coq.Program.Wf]

Fix_F_eq [lemma, in Coq.Program.Wf]

Fix_sub [definition, in Coq.Program.Wf]

Fix_F_sub [definition, in Coq.Program.Wf]

Fix_F_2 [definition, in Coq.Init.Wf]

Fix_eq [lemma, in Coq.Init.Wf]

Fix_F_inv [lemma, in Coq.Init.Wf]

Fix_F_eq [lemma, in Coq.Init.Wf]

Fix_F [definition, in Coq.Init.Wf]

fix_proto [definition, in Coq.Program.Tactics]

fi:91 [binder, in Coq.FSets.FSetPositive]

fi:91 [binder, in Coq.MSets.MSetPositive]

FlatMap [section, in Coq.Lists.List]

FlatMap.A [variable, in Coq.Lists.List]

FlatMap.B [variable, in Coq.Lists.List]

FlatMap.f [variable, in Coq.Lists.List]

flatten_cmp_opt [definition, in Coq.Floats.FloatAxioms]

flat_map_ext [lemma, in Coq.Lists.List]

flat_map_app [lemma, in Coq.Lists.List]

flat_map_concat_map [lemma, in Coq.Lists.List]

flat_map [definition, in Coq.Lists.List]

flat_exist [constructor, in Coq.Sorting.Heap]

flat_spec [inductive, in Coq.Sorting.Heap]

flex:49 [binder, in Coq.ssr.ssreflect]

Flhs [projection, in Coq.micromega.RingMicromega]

flip [definition, in Coq.Classes.CRelationClasses]

flip [definition, in Coq.Program.Basics]

flip_Equivalence [lemma, in Coq.Classes.RelationClasses]

flip_PER [lemma, in Coq.Classes.RelationClasses]

flip_StrictOrder [lemma, in Coq.Classes.RelationClasses]

flip_PreOrder [lemma, in Coq.Classes.RelationClasses]

flip_Antisymmetric [definition, in Coq.Classes.RelationClasses]

flip_Transitive [definition, in Coq.Classes.RelationClasses]

flip_Asymmetric [definition, in Coq.Classes.RelationClasses]

flip_Symmetric [definition, in Coq.Classes.RelationClasses]

flip_Irreflexive [definition, in Coq.Classes.RelationClasses]

flip_Reflexive [lemma, in Coq.Classes.RelationClasses]

flip_arrow [lemma, in Coq.Classes.Morphisms]

flip_atom [lemma, in Coq.Classes.Morphisms]

flip_respectful [lemma, in Coq.Classes.Morphisms]

flip_proper [definition, in Coq.Classes.Morphisms]

flip_arrow [lemma, in Coq.Classes.CMorphisms]

flip_atom [lemma, in Coq.Classes.CMorphisms]

flip_respectful [lemma, in Coq.Classes.CMorphisms]

flip_proper [definition, in Coq.Classes.CMorphisms]

flip_Equivalence [lemma, in Coq.Classes.CRelationClasses]

flip_PER [lemma, in Coq.Classes.CRelationClasses]

flip_StrictOrder [lemma, in Coq.Classes.CRelationClasses]

flip_PreOrder [lemma, in Coq.Classes.CRelationClasses]

flip_Antisymmetric [definition, in Coq.Classes.CRelationClasses]

flip_Transitive [definition, in Coq.Classes.CRelationClasses]

flip_Asymmetric [definition, in Coq.Classes.CRelationClasses]

flip_Symmetric [definition, in Coq.Classes.CRelationClasses]

flip_Irreflexive [definition, in Coq.Classes.CRelationClasses]

flip_Reflexive [lemma, in Coq.Classes.CRelationClasses]

flip_flip [lemma, in Coq.Program.Combinators]

flip_pointwise_relation [lemma, in Coq.Classes.Morphisms_Relations]

flip1 [lemma, in Coq.Classes.Morphisms]

flip1 [lemma, in Coq.Classes.CMorphisms]

flip2 [lemma, in Coq.Classes.Morphisms]

flip2 [lemma, in Coq.Classes.CMorphisms]

float [axiom, in Coq.Floats.PrimFloat]

FloatAxioms [library]

FloatClass [library]

FloatLemmas [library]

FloatOps [section, in Coq.Floats.SpecFloat]

FloatOps [library]

FloatOps.emax [variable, in Coq.Floats.SpecFloat]

FloatOps.Iter [section, in Coq.Floats.SpecFloat]

FloatOps.Iter.f [variable, in Coq.Floats.SpecFloat]

FloatOps.prec [variable, in Coq.Floats.SpecFloat]

FloatOps.Rounding [section, in Coq.Floats.SpecFloat]

FloatOps.ValidBinary [section, in Coq.Floats.SpecFloat]

FloatOps.Zdigits2 [section, in Coq.Floats.SpecFloat]

Floats [library]

float_comparison [inductive, in Coq.Floats.PrimFloat]

float_class [inductive, in Coq.Floats.FloatClass]

floor [definition, in Coq.ZArith.Zcomplements]

floor_ok [lemma, in Coq.ZArith.Zcomplements]

floor_gt0 [lemma, in Coq.ZArith.Zcomplements]

floor_pos [definition, in Coq.ZArith.Zcomplements]

FLt [constructor, in Coq.Floats.PrimFloat]

fl:21 [binder, in Coq.btauto.Reflect]

fl:24 [binder, in Coq.btauto.Reflect]

fl:4 [binder, in Coq.funind.Recdef]

fl:74 [binder, in Coq.btauto.Reflect]

FMapAVL [library]

FMapFacts [library]

FMapFullAVL [library]

FMapInterface [library]

FMapList [library]

FMapPositive [library]

FMaps [library]

FMapWeakList [library]

Fnorm [definition, in Coq.setoid_ring.Field_theory]

Fnorm_ok [lemma, in Coq.setoid_ring.Field_theory]

Fnorm_crossproduct [lemma, in Coq.setoid_ring.Field_theory]

Fnorm_FEeval_PEeval [lemma, in Coq.setoid_ring.Field_theory]

FNotComparable [constructor, in Coq.Floats.PrimFloat]

fn':442 [binder, in Coq.Reals.Ranalysis5]

fn1:19 [binder, in Coq.Lists.StreamMemo]

fn:1 [binder, in Coq.Reals.Rtrigo_reg]

fn:1 [binder, in Coq.Reals.Rtrigo1]

fn:1 [binder, in Coq.Reals.SeqSeries]

fn:101 [binder, in Coq.Reals.PSeries_reg]

fn:117 [binder, in Coq.Reals.PSeries_reg]

fn:126 [binder, in Coq.Reals.PSeries_reg]

fn:132 [binder, in Coq.Reals.PSeries_reg]

fn:14 [binder, in Coq.Program.Subset]

fn:144 [binder, in Coq.Reals.PartSum]

fn:158 [binder, in Coq.Reals.PartSum]

fn:17 [binder, in Coq.Lists.StreamMemo]

fn:43 [binder, in Coq.Reals.PSeries_reg]

fn:441 [binder, in Coq.Reals.Ranalysis5]

fn:51 [binder, in Coq.Reals.PSeries_reg]

fn:59 [binder, in Coq.Reals.PSeries_reg]

fn:61 [binder, in Coq.Reals.PSeries_reg]

fn:68 [binder, in Coq.Reals.PSeries_reg]

fn:9 [binder, in Coq.Program.Subset]

fn:90 [binder, in Coq.Reals.PSeries_reg]

foldA [definition, in Coq.micromega.Tauto]

fold_left_right_assoc_eq [lemma, in Coq.Vectors.VectorSpec]

fold_symmetric [lemma, in Coq.Lists.List]

fold_left_rev_right [lemma, in Coq.Lists.List]

fold_right_app [lemma, in Coq.Lists.List]

fold_right [definition, in Coq.Lists.List]

Fold_Right_Recursor.a0 [variable, in Coq.Lists.List]

Fold_Right_Recursor.f [variable, in Coq.Lists.List]

Fold_Right_Recursor.B [variable, in Coq.Lists.List]

Fold_Right_Recursor.A [variable, in Coq.Lists.List]

Fold_Right_Recursor [section, in Coq.Lists.List]

fold_left_length [lemma, in Coq.Lists.List]

fold_left_app [lemma, in Coq.Lists.List]

fold_left [definition, in Coq.Lists.List]

Fold_Left_Recursor.f [variable, in Coq.Lists.List]

Fold_Left_Recursor.B [variable, in Coq.Lists.List]

Fold_Left_Recursor.A [variable, in Coq.Lists.List]

Fold_Left_Recursor [section, in Coq.Lists.List]

fold_left2 [definition, in Coq.Vectors.VectorDef]

fold_right2 [definition, in Coq.Vectors.VectorDef]

fold_right [definition, in Coq.Vectors.VectorDef]

fold_left [definition, in Coq.Vectors.VectorDef]

fold_right_add2 [lemma, in Coq.Lists.SetoidList]

fold_right_equivlistA2 [lemma, in Coq.Lists.SetoidList]

fold_right_commutes2 [lemma, in Coq.Lists.SetoidList]

fold_right_add_restr2 [lemma, in Coq.Lists.SetoidList]

fold_right_equivlistA_restr2 [lemma, in Coq.Lists.SetoidList]

fold_right_commutes_restr2 [lemma, in Coq.Lists.SetoidList]

fold_right_eqlistA2 [lemma, in Coq.Lists.SetoidList]

fold_right_add [lemma, in Coq.Lists.SetoidList]

fold_right_equivlistA [lemma, in Coq.Lists.SetoidList]

fold_right_commutes [lemma, in Coq.Lists.SetoidList]

fold_right_add_restr [lemma, in Coq.Lists.SetoidList]

fold_right_equivlistA_restr [lemma, in Coq.Lists.SetoidList]

fold_right_commutes_restr [lemma, in Coq.Lists.SetoidList]

fold_right_eqlistA [lemma, in Coq.Lists.SetoidList]

fold:242 [binder, in Coq.FSets.FSetBridge]

Fop [projection, in Coq.micromega.RingMicromega]

FOP_cons [constructor, in Coq.Lists.List]

FOP_nil [constructor, in Coq.Lists.List]

ForAll [inductive, in Coq.Lists.Streams]

Forall [inductive, in Coq.Lists.List]

Forall [inductive, in Coq.Vectors.VectorDef]

forallb [definition, in Coq.Lists.List]

forallb_app [lemma, in Coq.Lists.List]

forallb_forall [lemma, in Coq.Lists.List]

ForallOrdPairs [inductive, in Coq.Lists.List]

ForallOrdPairs_ForallPairs [lemma, in Coq.Lists.List]

ForallOrdPairs_In [lemma, in Coq.Lists.List]

ForallOrdPairs_inclA [lemma, in Coq.Lists.SetoidList]

ForallPairs [definition, in Coq.Lists.List]

ForallPairs [section, in Coq.Lists.List]

ForallPairs_ForallOrdPairs [lemma, in Coq.Lists.List]

ForallPairs.A [variable, in Coq.Lists.List]

ForallPairs.R [variable, in Coq.Lists.List]

ForAll_map [lemma, in Coq.Lists.Streams]

ForAll_coind [lemma, in Coq.Lists.Streams]

ForAll_Str_nth_tl [lemma, in Coq.Lists.Streams]

Forall_nth_order [lemma, in Coq.Vectors.VectorSpec]

Forall_forall [lemma, in Coq.Vectors.VectorSpec]

Forall_impl [lemma, in Coq.Vectors.VectorSpec]

Forall_eq_repeat [lemma, in Coq.Lists.List]

Forall_image [lemma, in Coq.Lists.List]

Forall_flat_map [lemma, in Coq.Lists.List]

Forall_concat [lemma, in Coq.Lists.List]

Forall_map [lemma, in Coq.Lists.List]

Forall_Exists_dec [lemma, in Coq.Lists.List]

Forall_Exists_neg [lemma, in Coq.Lists.List]

Forall_and_inv [lemma, in Coq.Lists.List]

Forall_and [lemma, in Coq.Lists.List]

Forall_impl [lemma, in Coq.Lists.List]

Forall_fold_right [lemma, in Coq.Lists.List]

Forall_dec [lemma, in Coq.Lists.List]

Forall_rect [lemma, in Coq.Lists.List]

Forall_rev [lemma, in Coq.Lists.List]

Forall_elt [lemma, in Coq.Lists.List]

Forall_app [lemma, in Coq.Lists.List]

Forall_nth [lemma, in Coq.Lists.List]

Forall_forall [lemma, in Coq.Lists.List]

Forall_cons_iff [lemma, in Coq.Lists.List]

Forall_nil_iff [lemma, in Coq.Lists.List]

Forall_inv_tail [lemma, in Coq.Lists.List]

Forall_inv [lemma, in Coq.Lists.List]

Forall_cons [constructor, in Coq.Lists.List]

Forall_nil [constructor, in Coq.Lists.List]

forall_subrelation [lemma, in Coq.Classes.Morphisms]

forall_relation [definition, in Coq.Classes.Morphisms]

forall_def [definition, in Coq.Classes.Morphisms]

forall_eq_rect_comp [definition, in Coq.Logic.FunctionalExtensionality]

forall_eq_rect [definition, in Coq.Logic.FunctionalExtensionality]

forall_sig_eq_rect [lemma, in Coq.Logic.FunctionalExtensionality]

forall_extensionalityS [lemma, in Coq.Logic.FunctionalExtensionality]

forall_extensionalityP [lemma, in Coq.Logic.FunctionalExtensionality]

forall_extensionality [lemma, in Coq.Logic.FunctionalExtensionality]

forall_subrelation [lemma, in Coq.Classes.CMorphisms]

forall_relation [definition, in Coq.Classes.CMorphisms]

forall_def [definition, in Coq.Classes.CMorphisms]

forall_hprop [lemma, in Coq.Logic.HLevels]

forall_exists_coincide_unique_domain [lemma, in Coq.Init.Logic]

forall_exists_unique_domain_coincide [lemma, in Coq.Init.Logic]

Forall_cons [constructor, in Coq.Vectors.VectorDef]

Forall_nil [constructor, in Coq.Vectors.VectorDef]

Forall2 [inductive, in Coq.Lists.List]

Forall2 [section, in Coq.Lists.List]

Forall2 [inductive, in Coq.Vectors.VectorDef]

Forall2_nth_order [lemma, in Coq.Vectors.VectorSpec]

Forall2_app [lemma, in Coq.Lists.List]

Forall2_app_inv_r [lemma, in Coq.Lists.List]

Forall2_app_inv_l [lemma, in Coq.Lists.List]

Forall2_refl [lemma, in Coq.Lists.List]

Forall2_cons [constructor, in Coq.Lists.List]

Forall2_nil [constructor, in Coq.Lists.List]

Forall2_cons [constructor, in Coq.Vectors.VectorDef]

Forall2_nil [constructor, in Coq.Vectors.VectorDef]

Forall2.A [variable, in Coq.Lists.List]

Forall2.B [variable, in Coq.Lists.List]

Forall2.R [variable, in Coq.Lists.List]

forE [lemma, in Coq.ssr.ssrbool]

form [inductive, in Coq.rtauto.Rtauto]

Format [module, in Ltac2.Message]

Formula [record, in Coq.micromega.RingMicromega]

formula [inductive, in Coq.btauto.Reflect]

formula_eval [definition, in Coq.btauto.Reflect]

formula_ifb [constructor, in Coq.btauto.Reflect]

formula_xor [constructor, in Coq.btauto.Reflect]

formula_neg [constructor, in Coq.btauto.Reflect]

formula_dsj [constructor, in Coq.btauto.Reflect]

formula_cnj [constructor, in Coq.btauto.Reflect]

formula_top [constructor, in Coq.btauto.Reflect]

formula_btm [constructor, in Coq.btauto.Reflect]

formula_var [constructor, in Coq.btauto.Reflect]

formule [lemma, in Coq.Reals.Ranalysis2]

form_eq_refl [lemma, in Coq.rtauto.Rtauto]

form_eq [definition, in Coq.rtauto.Rtauto]

form1 [lemma, in Coq.Reals.Rtrigo1]

form2 [lemma, in Coq.Reals.Rtrigo1]

form3 [lemma, in Coq.Reals.Rtrigo1]

form4 [lemma, in Coq.Reals.Rtrigo1]

for_base_fp [lemma, in Coq.Reals.R_Ifp]

found:22 [binder, in Coq.Logic.ConstructiveEpsilon]

found:24 [binder, in Coq.Logic.ConstructiveEpsilon]

found:66 [binder, in Coq.Logic.ConstructiveEpsilon]

found:67 [binder, in Coq.Logic.ConstructiveEpsilon]

Fourier [library]

Fourier_util [library]

fp_nat [lemma, in Coq.Reals.R_Ifp]

fp_R0 [lemma, in Coq.Reals.R_Ifp]

frac_part [definition, in Coq.Reals.R_Ifp]

frame_tan [definition, in Coq.Reals.Ratan]

frame:139 [binder, in Coq.ssr.ssreflect]

Free [module, in Ltac2.Fresh]

frefl [lemma, in Coq.ssr.ssrfun]

Fresh [library]

frexp [definition, in Coq.Floats.FloatOps]

frexp_spec [lemma, in Coq.Floats.FloatLemmas]

Frhs [projection, in Coq.micromega.RingMicromega]

frshiftexp [axiom, in Coq.Floats.PrimFloat]

frshiftexp_spec [axiom, in Coq.Floats.FloatAxioms]

fr:22 [binder, in Coq.btauto.Reflect]

fr:25 [binder, in Coq.btauto.Reflect]

fr:324 [binder, in Coq.micromega.ZMicromega]

fr:381 [binder, in Coq.micromega.ZMicromega]

fr:389 [binder, in Coq.micromega.ZMicromega]

fr:393 [binder, in Coq.micromega.ZMicromega]

fr:75 [binder, in Coq.btauto.Reflect]

FS [constructor, in Coq.Vectors.Fin]

FSetAVL [library]

FSetBridge [library]

FSetCompat [library]

FSetDecide [library]

FSetEqProperties [library]

FSetFacts [library]

FSetInterface [library]

FSetList [library]

FSetPositive [library]

FSetProperties [library]

FSets [library]

FSetToFiniteSet [library]

FSetWeakList [library]

Fst [abbreviation, in Coq.Classes.RelationPairs]

fst [definition, in Coq.Init.Datatypes]

FstRel_sub [instance, in Coq.Classes.RelationPairs]

FstRel_ProdRel [lemma, in Coq.Classes.RelationPairs]

fstT [abbreviation, in Coq.Init.Datatypes]

fst_compat [instance, in Coq.Classes.RelationPairs]

fst_measure [instance, in Coq.Classes.RelationPairs]

fsym [lemma, in Coq.ssr.ssrfun]

FS_inj [definition, in Coq.Vectors.Fin]

fS2':32 [binder, in Coq.NArith.BinNat]

fS2:25 [binder, in Coq.NArith.BinNat]

fS2:317 [binder, in Coq.NArith.BinNat]

fS2:322 [binder, in Coq.NArith.BinNat]

FTCN_step1 [lemma, in Coq.Reals.NewtonInt]

FTC_Riemann [lemma, in Coq.Reals.RiemannInt]

FTC_P1 [lemma, in Coq.Reals.RiemannInt]

FTC_Newton [lemma, in Coq.Reals.NewtonInt]

ftrans [lemma, in Coq.ssr.ssrfun]

fT:81 [binder, in Coq.ssr.ssrbool]

Full [inductive, in Coq.rtauto.Bintree]

Full [definition, in Coq.Logic.FinFun]

Fullset [definition, in Coq.Sets.Uniset]

Full_intro [constructor, in Coq.Sets.Ensembles]

Full_set [inductive, in Coq.Sets.Ensembles]

Full_map [lemma, in Coq.rtauto.Bintree]

Full_index_one_empty [lemma, in Coq.rtauto.Bintree]

Full_push_compat [lemma, in Coq.rtauto.Bintree]

FunChoice_Equiv_RelChoice_and_ParamDefinDescr [abbreviation, in Coq.Logic.ChoiceFacts]

FunctExt_BijComp [lemma, in Coq.Logic.ExtensionalityFacts]

FunctExt_iff_UniqInverse [lemma, in Coq.Logic.ExtensionalityFacts]

FunctExt_UniqInverse [lemma, in Coq.Logic.ExtensionalityFacts]

FunctExt_iff_EqDeltaProjs [lemma, in Coq.Logic.ExtensionalityFacts]

FunctionalChoice [abbreviation, in Coq.Logic.ChoiceFacts]

FunctionalChoiceOnInhabitedSet [abbreviation, in Coq.Logic.ChoiceFacts]

FunctionalChoice_on [definition, in Coq.Logic.ChoiceFacts]

FunctionalChoice_on_rel [definition, in Coq.Logic.ChoiceFacts]

FunctionalCountableChoice [abbreviation, in Coq.Logic.ChoiceFacts]

FunctionalCountableChoice_on [definition, in Coq.Logic.ChoiceFacts]

FunctionalDependentChoice [abbreviation, in Coq.Logic.ChoiceFacts]

FunctionalDependentChoice_on [definition, in Coq.Logic.ChoiceFacts]

FunctionalExtensionality [abbreviation, in Coq.Logic.ExtensionalityFacts]

FunctionalExtensionality [library]

FunctionalRelReification [abbreviation, in Coq.Logic.ChoiceFacts]

FunctionalRelReification_on [definition, in Coq.Logic.ChoiceFacts]

functional_extensionality_dep_good_refl [lemma, in Coq.Logic.FunctionalExtensionality]

functional_extensionality_dep_good [definition, in Coq.Logic.FunctionalExtensionality]

functional_extensionality [lemma, in Coq.Logic.FunctionalExtensionality]

functional_extensionality_dep [axiom, in Coq.Logic.FunctionalExtensionality]

functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]

functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]

functional_dependent_choice_imp_functional_countable_choice [lemma, in Coq.Logic.ChoiceFacts]

functional_choice_imp_functional_dependent_choice [lemma, in Coq.Logic.ChoiceFacts]

functional_choice_to_inhabited_forall_commute [lemma, in Coq.Logic.ChoiceFacts]

functional_rel_reification_and_rel_choice_imp_fun_choice [lemma, in Coq.Logic.ChoiceFacts]

functional_choice [lemma, in Coq.Logic.IndefiniteDescription]

funct_choice_imp_description [abbreviation, in Coq.Logic.ChoiceFacts]

funct_choice_imp_rel_choice [abbreviation, in Coq.Logic.ChoiceFacts]

FunInd [library]

fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]

fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]

fun_reification_descr_computational_excluded_middle_in_prop_context [lemma, in Coq.Logic.ChoiceFacts]

fun_choice_and_small_drinker_iff_omniscient_fun_choice [lemma, in Coq.Logic.ChoiceFacts]

fun_choice_and_small_drinker_imp_omniscient_fun_choice [lemma, in Coq.Logic.ChoiceFacts]

fun_choice_and_indep_general_prem_iff_guarded_fun_choice [lemma, in Coq.Logic.ChoiceFacts]

fun_choice_and_indep_general_prem_imp_guarded_fun_choice [lemma, in Coq.Logic.ChoiceFacts]

fun_choice_iff_rel_choice_and_functional_rel_reification [lemma, in Coq.Logic.ChoiceFacts]

fun_choice_imp_functional_rel_reification [lemma, in Coq.Logic.ChoiceFacts]

fun_choice_imp_rel_choice [lemma, in Coq.Logic.ChoiceFacts]

fun_if [lemma, in Coq.ssr.ssrbool]

fun_of_simpl [definition, in Coq.ssr.ssrfun]

Further [constructor, in Coq.Lists.Streams]

fv:419 [binder, in Coq.setoid_ring.Ring_polynom]

fv:427 [binder, in Coq.setoid_ring.Ring_polynom]

fv:434 [binder, in Coq.setoid_ring.Ring_polynom]

fv:470 [binder, in Coq.setoid_ring.Ring_polynom]

fv:478 [binder, in Coq.setoid_ring.Ring_polynom]

fv:486 [binder, in Coq.setoid_ring.Ring_polynom]

fv:502 [binder, in Coq.setoid_ring.Ring_polynom]

fv:528 [binder, in Coq.setoid_ring.Ring_polynom]

fv:67 [binder, in Coq.nsatz.NsatzTactic]

fxnz:128 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

F_sub:130 [binder, in Coq.Program.Wf]

F_unfold [lemma, in Coq.Program.Wf]

f_sub:34 [binder, in Coq.Program.Wf]

f_equal2_mult [definition, in Coq.Init.Peano]

f_equal2_nat [definition, in Coq.Init.Peano]

f_equal2_plus [definition, in Coq.Init.Peano]

f_equal_pred [definition, in Coq.Init.Peano]

f_equal_nat [definition, in Coq.Init.Peano]

f_eq_dep_non_dep [lemma, in Coq.Logic.EqdepFacts]

f_eq_dep [lemma, in Coq.Logic.EqdepFacts]

f_equal__functional_extensionality_dep_good__fun [definition, in Coq.Logic.FunctionalExtensionality]

f_equal__functional_extensionality_dep_good [definition, in Coq.Logic.FunctionalExtensionality]

F_1_neq_0 [projection, in Coq.setoid_ring.Field_theory]

F_R [projection, in Coq.setoid_ring.Field_theory]

F_push [constructor, in Coq.rtauto.Bintree]

F_empty [constructor, in Coq.rtauto.Bintree]

f_eq_g:431 [binder, in Coq.Reals.Ranalysis5]

f_decr:425 [binder, in Coq.Reals.Ranalysis5]

f_eq_g:414 [binder, in Coq.Reals.Ranalysis5]

f_incr:408 [binder, in Coq.Reals.Ranalysis5]

f_derivable:363 [binder, in Coq.Reals.Ranalysis5]

f_decr:361 [binder, in Coq.Reals.Ranalysis5]

f_eq_g:356 [binder, in Coq.Reals.Ranalysis5]

f_derivable:345 [binder, in Coq.Reals.Ranalysis5]

f_incr:343 [binder, in Coq.Reals.Ranalysis5]

f_eq_g:338 [binder, in Coq.Reals.Ranalysis5]

f_interv_is_interv [lemma, in Coq.Reals.Ranalysis5]

f_incr_implies_g_incr_interv [lemma, in Coq.Reals.Ranalysis5]

f_equal_R [definition, in Coq.Reals.RIneq]

f_equal_compose [lemma, in Coq.Init.Logic]

f_equal5 [lemma, in Coq.Init.Logic]

f_equal4 [lemma, in Coq.Init.Logic]

f_equal3 [lemma, in Coq.Init.Logic]

f_equal2 [lemma, in Coq.Init.Logic]

f_equal_dep2 [lemma, in Coq.Init.Logic]

f_equal_dep [lemma, in Coq.Init.Logic]

f_equal [lemma, in Coq.Init.Logic]

f_adjoint [definition, in Coq.Logic.Adjointification]

f_adjoint:33 [binder, in Coq.Logic.Adjointification]

f_adjoint_gives_g_adjoint [definition, in Coq.Logic.Adjointification]

f_adjoint_at_gb:19 [binder, in Coq.Logic.Adjointification]

f_adjoint_gives_g_adjoint_pointwise [definition, in Coq.Logic.Adjointification]

f'':306 [binder, in Coq.ssr.ssrfun]

f'':650 [binder, in Coq.ssr.ssrbool]

f'':651 [binder, in Coq.ssr.ssrbool]

f'':653 [binder, in Coq.ssr.ssrbool]

f':120 [binder, in Coq.micromega.RingMicromega]

f':146 [binder, in Coq.micromega.Tauto]

f':155 [binder, in Coq.Reals.PSeries_reg]

f':161 [binder, in Coq.micromega.RingMicromega]

f':192 [binder, in Coq.Reals.MVT]

f':218 [binder, in Coq.micromega.Tauto]

f':24 [binder, in Coq.Numbers.DecimalQ]

f':24 [binder, in Coq.Numbers.HexadecimalQ]

f':247 [binder, in Coq.micromega.Tauto]

f':253 [binder, in Coq.micromega.Tauto]

f':259 [binder, in Coq.micromega.Tauto]

f':265 [binder, in Coq.micromega.Tauto]

f':27 [binder, in Coq.FSets.FSetFacts]

f':289 [binder, in Coq.ssr.ssrfun]

f':290 [binder, in Coq.ssr.ssrfun]

f':292 [binder, in Coq.ssr.ssrfun]

f':294 [binder, in Coq.ssr.ssrfun]

f':296 [binder, in Coq.ssr.ssrfun]

f':304 [binder, in Coq.ssr.ssrfun]

f':305 [binder, in Coq.ssr.ssrfun]

f':313 [binder, in Coq.ssr.ssrfun]

f':33 [binder, in Coq.MSets.MSetFacts]

f':361 [binder, in Coq.micromega.ZMicromega]

f':41 [binder, in Coq.Reals.MVT]

f':44 [binder, in Coq.NArith.BinNat]

f':553 [binder, in Coq.micromega.Tauto]

f':556 [binder, in Coq.micromega.Tauto]

f':59 [binder, in Coq.Reals.MVT]

f':91 [binder, in Coq.ssr.ssrfun]

f0:20 [binder, in Coq.Lists.StreamMemo]

f0:21 [binder, in Coq.NArith.BinNat]

f0:315 [binder, in Coq.NArith.BinNat]

f0:320 [binder, in Coq.NArith.BinNat]

f0:37 [binder, in Coq.NArith.BinNat]

F0:66 [binder, in Coq.Reals.NewtonInt]

F0:85 [binder, in Coq.Reals.NewtonInt]

F0:91 [binder, in Coq.Reals.NewtonInt]

F1 [constructor, in Coq.Vectors.Fin]

f1 [projection, in Coq.Logic.ClassicalFacts]

f1_o_f2 [projection, in Coq.Logic.ClassicalFacts]

f1:1 [binder, in Coq.Reals.Ranalysis1]

f1:1 [binder, in Coq.Reals.Ranalysis3]

f1:100 [binder, in Coq.ssr.ssreflect]

f1:106 [binder, in Coq.Reals.Ranalysis1]

f1:106 [binder, in Coq.micromega.RingMicromega]

f1:109 [binder, in Coq.Reals.Ranalysis1]

f1:12 [binder, in Coq.Reals.Ranalysis1]

f1:122 [binder, in Coq.micromega.RingMicromega]

f1:126 [binder, in Coq.micromega.RingMicromega]

f1:14 [binder, in Coq.Reals.Ranalysis2]

f1:149 [binder, in Coq.micromega.Tauto]

f1:15 [binder, in Coq.Reals.Ranalysis1]

f1:157 [binder, in Coq.micromega.Tauto]

f1:159 [binder, in Coq.micromega.Tauto]

f1:169 [binder, in Coq.micromega.Tauto]

f1:173 [binder, in Coq.micromega.Tauto]

f1:177 [binder, in Coq.micromega.Tauto]

f1:181 [binder, in Coq.micromega.Tauto]

f1:209 [binder, in Coq.Reals.Ranalysis1]

f1:21 [binder, in Coq.Reals.Ranalysis1]

f1:22 [binder, in Coq.Reals.Ranalysis3]

f1:229 [binder, in Coq.micromega.Tauto]

f1:25 [binder, in Coq.Reals.Ranalysis3]

f1:251 [binder, in Coq.Reals.Ranalysis1]

f1:264 [binder, in Coq.Reals.Ranalysis1]

f1:277 [binder, in Coq.Reals.Ranalysis1]

f1:28 [binder, in Coq.Reals.Ranalysis3]

f1:307 [binder, in Coq.micromega.Tauto]

f1:312 [binder, in Coq.micromega.Tauto]

f1:314 [binder, in Coq.Reals.Ranalysis1]

f1:317 [binder, in Coq.micromega.Tauto]

f1:322 [binder, in Coq.micromega.Tauto]

f1:330 [binder, in Coq.Reals.Ranalysis1]

f1:333 [binder, in Coq.Reals.Ranalysis1]

f1:335 [binder, in Coq.micromega.Tauto]

f1:336 [binder, in Coq.Reals.Ranalysis1]

f1:339 [binder, in Coq.micromega.Tauto]

f1:344 [binder, in Coq.micromega.Tauto]

f1:345 [binder, in Coq.Reals.Ranalysis1]

f1:347 [binder, in Coq.micromega.Tauto]

f1:349 [binder, in Coq.Reals.Ranalysis1]

f1:35 [binder, in Coq.Reals.Ranalysis2]

f1:351 [binder, in Coq.Reals.Ranalysis1]

f1:352 [binder, in Coq.micromega.Tauto]

f1:353 [binder, in Coq.Reals.Ranalysis1]

f1:358 [binder, in Coq.micromega.Tauto]

f1:359 [binder, in Coq.Reals.Ranalysis1]

f1:361 [binder, in Coq.micromega.Tauto]

f1:371 [binder, in Coq.micromega.Tauto]

f1:372 [binder, in Coq.micromega.Tauto]

f1:376 [binder, in Coq.Reals.Ranalysis1]

f1:376 [binder, in Coq.micromega.Tauto]

f1:380 [binder, in Coq.micromega.Tauto]

f1:381 [binder, in Coq.Reals.Ranalysis1]

f1:386 [binder, in Coq.Reals.Ranalysis1]

f1:403 [binder, in Coq.micromega.Tauto]

f1:407 [binder, in Coq.micromega.Tauto]

f1:411 [binder, in Coq.micromega.Tauto]

f1:418 [binder, in Coq.micromega.Tauto]

f1:450 [binder, in Coq.micromega.Tauto]

f1:452 [binder, in Coq.micromega.Tauto]

f1:459 [binder, in Coq.micromega.Tauto]

f1:46 [binder, in Coq.Reals.Ranalysis2]

f1:469 [binder, in Coq.micromega.Tauto]

f1:479 [binder, in Coq.micromega.Tauto]

f1:489 [binder, in Coq.micromega.Tauto]

f1:5 [binder, in Coq.Reals.Ranalysis2]

f1:588 [binder, in Coq.micromega.Tauto]

f1:6 [binder, in Coq.Reals.Ranalysis1]

f1:60 [binder, in Coq.Reals.Ranalysis1]

f1:605 [binder, in Coq.micromega.Tauto]

f1:65 [binder, in Coq.Reals.Ranalysis1]

F1:67 [binder, in Coq.Reals.NewtonInt]

f1:68 [binder, in Coq.Reals.Ranalysis1]

f1:7 [binder, in Coq.Numbers.Natural.Abstract.NIso]

f1:71 [binder, in Coq.Floats.SpecFloat]

f1:79 [binder, in Coq.Floats.SpecFloat]

f1:81 [binder, in Coq.Floats.SpecFloat]

f1:82 [binder, in Coq.Reals.Ranalysis1]

f1:83 [binder, in Coq.Floats.SpecFloat]

f1:84 [binder, in Coq.Reals.Ranalysis1]

F1:86 [binder, in Coq.Reals.NewtonInt]

f1:87 [binder, in Coq.Reals.Ranalysis1]

F1:92 [binder, in Coq.Reals.NewtonInt]

f1:94 [binder, in Coq.Reals.Ranalysis1]

f1:97 [binder, in Coq.Reals.Ranalysis1]

f1:99 [binder, in Coq.Reals.Ranalysis1]

f1:99 [binder, in Coq.micromega.RingMicromega]

f2 [projection, in Coq.Logic.ClassicalFacts]

F2AF [definition, in Coq.setoid_ring.Field_theory]

f2':30 [binder, in Coq.NArith.BinNat]

f2:100 [binder, in Coq.Reals.Ranalysis1]

f2:100 [binder, in Coq.micromega.RingMicromega]

f2:101 [binder, in Coq.ssr.ssreflect]

f2:107 [binder, in Coq.Reals.Ranalysis1]

f2:107 [binder, in Coq.micromega.RingMicromega]

f2:110 [binder, in Coq.Reals.Ranalysis1]

f2:123 [binder, in Coq.micromega.RingMicromega]

f2:127 [binder, in Coq.micromega.RingMicromega]

f2:13 [binder, in Coq.Reals.Ranalysis1]

f2:15 [binder, in Coq.Reals.Ranalysis2]

f2:150 [binder, in Coq.micromega.Tauto]

f2:158 [binder, in Coq.micromega.Tauto]

f2:16 [binder, in Coq.Reals.Ranalysis1]

f2:160 [binder, in Coq.micromega.Tauto]

f2:170 [binder, in Coq.micromega.Tauto]

f2:174 [binder, in Coq.micromega.Tauto]

f2:178 [binder, in Coq.micromega.Tauto]

f2:182 [binder, in Coq.micromega.Tauto]

f2:2 [binder, in Coq.Reals.Ranalysis1]

f2:2 [binder, in Coq.Reals.Ranalysis3]

f2:210 [binder, in Coq.Reals.Ranalysis1]

f2:22 [binder, in Coq.Reals.Ranalysis1]

f2:23 [binder, in Coq.NArith.BinNat]

f2:23 [binder, in Coq.Reals.Ranalysis3]

f2:230 [binder, in Coq.micromega.Tauto]

f2:25 [binder, in Coq.Reals.Ranalysis2]

f2:252 [binder, in Coq.Reals.Ranalysis1]

f2:26 [binder, in Coq.Reals.Ranalysis3]

f2:265 [binder, in Coq.Reals.Ranalysis1]

f2:278 [binder, in Coq.Reals.Ranalysis1]

f2:29 [binder, in Coq.Reals.Ranalysis3]

f2:308 [binder, in Coq.micromega.Tauto]

f2:313 [binder, in Coq.micromega.Tauto]

f2:315 [binder, in Coq.Reals.Ranalysis1]

f2:316 [binder, in Coq.NArith.BinNat]

f2:321 [binder, in Coq.NArith.BinNat]

f2:323 [binder, in Coq.micromega.Tauto]

f2:331 [binder, in Coq.Reals.Ranalysis1]

f2:334 [binder, in Coq.Reals.Ranalysis1]

f2:336 [binder, in Coq.micromega.Tauto]

f2:337 [binder, in Coq.Reals.Ranalysis1]

f2:340 [binder, in Coq.micromega.Tauto]

f2:345 [binder, in Coq.micromega.Tauto]

f2:346 [binder, in Coq.Reals.Ranalysis1]

f2:348 [binder, in Coq.micromega.Tauto]

f2:350 [binder, in Coq.Reals.Ranalysis1]

f2:352 [binder, in Coq.Reals.Ranalysis1]

f2:354 [binder, in Coq.Reals.Ranalysis1]

f2:359 [binder, in Coq.micromega.Tauto]

f2:36 [binder, in Coq.Reals.Ranalysis2]

f2:360 [binder, in Coq.Reals.Ranalysis1]

f2:362 [binder, in Coq.micromega.Tauto]

f2:377 [binder, in Coq.Reals.Ranalysis1]

f2:377 [binder, in Coq.micromega.Tauto]

f2:381 [binder, in Coq.micromega.Tauto]

f2:382 [binder, in Coq.Reals.Ranalysis1]

f2:387 [binder, in Coq.Reals.Ranalysis1]

f2:404 [binder, in Coq.micromega.Tauto]

f2:408 [binder, in Coq.micromega.Tauto]

f2:412 [binder, in Coq.micromega.Tauto]

f2:419 [binder, in Coq.micromega.Tauto]

f2:451 [binder, in Coq.micromega.Tauto]

f2:453 [binder, in Coq.micromega.Tauto]

f2:460 [binder, in Coq.micromega.Tauto]

f2:47 [binder, in Coq.Reals.Ranalysis2]

f2:470 [binder, in Coq.micromega.Tauto]

f2:480 [binder, in Coq.micromega.Tauto]

f2:490 [binder, in Coq.micromega.Tauto]

f2:590 [binder, in Coq.micromega.Tauto]

f2:6 [binder, in Coq.Reals.Ranalysis2]

f2:606 [binder, in Coq.micromega.Tauto]

f2:61 [binder, in Coq.Reals.Ranalysis1]

f2:66 [binder, in Coq.Reals.Ranalysis1]

f2:69 [binder, in Coq.Reals.Ranalysis1]

f2:7 [binder, in Coq.Reals.Ranalysis1]

f2:72 [binder, in Coq.Floats.SpecFloat]

f2:78 [binder, in Coq.PArith.BinPos]

f2:8 [binder, in Coq.Numbers.Natural.Abstract.NIso]

f2:80 [binder, in Coq.Floats.SpecFloat]

f2:82 [binder, in Coq.Floats.SpecFloat]

f2:83 [binder, in Coq.Reals.Ranalysis1]

f2:84 [binder, in Coq.Floats.SpecFloat]

f2:85 [binder, in Coq.Reals.Ranalysis1]

f2:88 [binder, in Coq.Reals.Ranalysis1]

f2:95 [binder, in Coq.Reals.Ranalysis1]

f2:98 [binder, in Coq.Reals.Ranalysis1]

f:1 [binder, in Coq.Numbers.Natural.Abstract.NIso]

f:1 [binder, in Coq.Reals.Ranalysis4]

f:1 [binder, in Coq.Floats.FloatLemmas]

f:1 [binder, in Coq.Reals.MVT]

f:1 [binder, in Coq.Reals.Rprod]

f:1 [binder, in Coq.Floats.FloatOps]

f:1 [binder, in Coq.Reals.RiemannInt]

f:1 [binder, in Coq.Reals.NewtonInt]

f:1 [binder, in Coq.Reals.Ranalysis5]

f:1 [binder, in Coq.Logic.PropFacts]

f:10 [binder, in Coq.Reals.Ranalysis1]

f:10 [binder, in Coq.Init.Decimal]

f:10 [binder, in Coq.Logic.SetoidChoice]

f:10 [binder, in Coq.Init.Hexadecimal]

f:10 [binder, in Coq.Reals.NewtonInt]

f:10 [binder, in Coq.Sets.Uniset]

f:10 [binder, in Coq.Sets.Image]

f:10 [binder, in Coq.Numbers.Natural.Abstract.NStrongRec]

f:100 [binder, in Coq.MSets.MSetEqProperties]

f:100 [binder, in Coq.FSets.FSetEqProperties]

f:100 [binder, in Coq.MSets.MSetRBT]

f:100 [binder, in Coq.Reals.Rtopology]

f:1005 [binder, in Coq.Init.Specif]

f:101 [binder, in Coq.Reals.Ranalysis1]

F:101 [binder, in Coq.rtauto.Bintree]

f:101 [binder, in Coq.Reals.RiemannInt_SF]

f:1019 [binder, in Coq.Lists.List]

f:102 [binder, in Coq.Reals.Ranalysis1]

f:102 [binder, in Coq.FSets.FMapFacts]

f:102 [binder, in Coq.MSets.MSetWeakList]

f:102 [binder, in Coq.Reals.NewtonInt]

f:102 [binder, in Coq.FSets.FSetPositive]

f:102 [binder, in Coq.MSets.MSetRBT]

f:102 [binder, in Coq.micromega.ZMicromega]

f:102 [binder, in Coq.FSets.FSetCompat]

f:1030 [binder, in Coq.Lists.List]

f:1034 [binder, in Coq.Lists.List]

f:104 [binder, in Coq.Reals.Ranalysis1]

f:104 [binder, in Coq.Reals.RiemannInt_SF]

f:104 [binder, in Coq.micromega.Tauto]

f:104 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:1045 [binder, in Coq.Lists.List]

f:105 [binder, in Coq.Reals.MVT]

f:105 [binder, in Coq.FSets.FMapInterface]

f:105 [binder, in Coq.micromega.RMicromega]

f:105 [binder, in Coq.FSets.FSetCompat]

f:1056 [binder, in Coq.Lists.List]

f:106 [binder, in Coq.Reals.Rtopology]

f:106 [binder, in Coq.Structures.GenericMinMax]

f:106 [binder, in Coq.QArith.QArith_base]

f:106 [binder, in Coq.Logic.FinFun]

f:1066 [binder, in Coq.Lists.List]

f:107 [binder, in Coq.Reals.Rderiv]

f:107 [binder, in Coq.Logic.FunctionalExtensionality]

f:107 [binder, in Coq.Logic.ClassicalFacts]

f:107 [binder, in Coq.Lists.SetoidList]

f:107 [binder, in Coq.FSets.FSetCompat]

f:1072 [binder, in Coq.Lists.List]

f:1077 [binder, in Coq.Init.Specif]

f:108 [binder, in Coq.Reals.MVT]

f:108 [binder, in Coq.Reals.NewtonInt]

f:1083 [binder, in Coq.Init.Specif]

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

f:109 [binder, in Coq.Reals.MVT]

f:109 [binder, in Coq.FSets.FMapFacts]

f:109 [binder, in Coq.Logic.FinFun]

f:109 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:1097 [binder, in Coq.Init.Specif]

f:11 [binder, in Coq.Numbers.DecimalQ]

f:11 [binder, in Coq.Numbers.Natural.Abstract.NAxioms]

f:11 [binder, in Coq.Program.Combinators]

f:11 [binder, in Coq.Numbers.HexadecimalQ]

f:11 [binder, in Coq.Reals.ClassicalDedekindReals]

f:110 [binder, in Coq.MSets.MSetRBT]

f:110 [binder, in Coq.Reals.Rlimit]

f:110 [binder, in Coq.FSets.FSetCompat]

f:111 [binder, in Coq.Reals.Ranalysis1]

f:111 [binder, in Coq.Logic.ChoiceFacts]

f:111 [binder, in Coq.Reals.Rtopology]

f:111 [binder, in Coq.Structures.GenericMinMax]

f:111 [binder, in Coq.Reals.RList]

f:112 [binder, in Coq.Reals.RiemannInt]

f:112 [binder, in Coq.Lists.SetoidList]

f:113 [binder, in Coq.PArith.BinPos]

f:113 [binder, in Coq.FSets.FMapInterface]

f:113 [binder, in Coq.Reals.Rtopology]

f:113 [binder, in Coq.Numbers.Integer.Abstract.ZBits]

f:113 [binder, in Coq.FSets.FSetCompat]

f:114 [binder, in Coq.Logic.ClassicalFacts]

f:114 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]

f:114 [binder, in Coq.micromega.Tauto]

f:114 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:115 [binder, in Coq.Reals.Rderiv]

f:115 [binder, in Coq.micromega.RMicromega]

f:115 [binder, in Coq.Logic.FinFun]

f:116 [binder, in Coq.FSets.FSetDecide]

f:116 [binder, in Coq.MSets.MSetEqProperties]

f:116 [binder, in Coq.MSets.MSetDecide]

f:116 [binder, in Coq.FSets.FMapAVL]

f:116 [binder, in Coq.FSets.FSetEqProperties]

f:116 [binder, in Coq.FSets.FSetCompat]

f:117 [binder, in Coq.Reals.Ranalysis1]

f:117 [binder, in Coq.Logic.ChoiceFacts]

f:117 [binder, in Coq.Logic.FinFun]

f:118 [binder, in Coq.Reals.MVT]

f:118 [binder, in Coq.Reals.Rlimit]

f:118 [binder, in Coq.micromega.RMicromega]

f:119 [binder, in Coq.micromega.RingMicromega]

f:119 [binder, in Coq.Vectors.Fin]

f:119 [binder, in Coq.Reals.Ranalysis5]

f:119 [binder, in Coq.micromega.Tauto]

f:119 [binder, in Coq.FSets.FSetCompat]

f:12 [binder, in Coq.Reals.Rderiv]

f:12 [binder, in Coq.Wellfounded.Well_Ordering]

f:12 [binder, in Coq.Init.Decimal]

f:12 [binder, in Coq.Init.Hexadecimal]

f:12 [binder, in Coq.rtauto.Bintree]

F:12 [binder, in Coq.micromega.DeclConstant]

f:12 [binder, in Coq.Logic.Adjointification]

f:12 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:120 [binder, in Coq.Reals.Ranalysis1]

f:120 [binder, in Coq.MSets.MSetProperties]

f:120 [binder, in Coq.FSets.FSetProperties]

f:120 [binder, in Coq.Logic.FinFun]

f:120 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:121 [binder, in Coq.Numbers.DecimalFacts]

f:121 [binder, in Coq.FSets.FMapInterface]

f:121 [binder, in Coq.FSets.FMapFullAVL]

f:121 [binder, in Coq.Reals.Rpower]

f:121 [binder, in Coq.Numbers.HexadecimalFacts]

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

f:121 [binder, in Coq.FSets.FSetCompat]

f:1211 [binder, in Coq.FSets.FMapAVL]

f:1215 [binder, in Coq.FSets.FMapAVL]

f:122 [binder, in Coq.FSets.FSetDecide]

f:122 [binder, in Coq.MSets.MSetDecide]

f:122 [binder, in Coq.FSets.FMapAVL]

f:122 [binder, in Coq.NArith.BinNatDef]

f:1220 [binder, in Coq.FSets.FMapAVL]

f:1226 [binder, in Coq.FSets.FMapAVL]

f:123 [binder, in Coq.Reals.Ranalysis1]

f:123 [binder, in Coq.Numbers.DecimalFacts]

f:123 [binder, in Coq.Classes.RelationClasses]

f:123 [binder, in Coq.FSets.FMapFullAVL]

f:123 [binder, in Coq.Numbers.HexadecimalFacts]

f:123 [binder, in Coq.Reals.RiemannInt_SF]

f:124 [binder, in Coq.micromega.RingMicromega]

f:124 [binder, in Coq.Classes.RelationClasses]

f:124 [binder, in Coq.Logic.FinFun]

f:125 [binder, in Coq.Reals.Ranalysis1]

f:125 [binder, in Coq.Logic.ChoiceFacts]

f:125 [binder, in Coq.FSets.FMapFullAVL]

f:125 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:126 [binder, in Coq.MSets.MSetEqProperties]

f:126 [binder, in Coq.Reals.Abstract.ConstructiveLimits]

f:126 [binder, in Coq.FSets.FSetEqProperties]

f:126 [binder, in Coq.Reals.RiemannInt_SF]

f:127 [binder, in Coq.Reals.Rpower]

f:128 [binder, in Coq.Reals.Ranalysis1]

f:128 [binder, in Coq.FSets.FSetDecide]

f:128 [binder, in Coq.micromega.RingMicromega]

f:128 [binder, in Coq.MSets.MSetProperties]

f:128 [binder, in Coq.Reals.MVT]

f:128 [binder, in Coq.MSets.MSetDecide]

f:128 [binder, in Coq.FSets.FMapAVL]

f:128 [binder, in Coq.FSets.FSetProperties]

f:128 [binder, in Coq.Logic.FinFun]

f:129 [binder, in Coq.PArith.BinPos]

f:129 [binder, in Coq.Classes.RelationClasses]

f:13 [binder, in Coq.Logic.ChoiceFacts]

f:13 [binder, in Coq.ssr.ssrfun]

f:13 [binder, in Coq.Arith.PeanoNat]

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

f:13 [binder, in Coq.Logic.FinFun]

f:130 [binder, in Coq.MSets.MSetInterface]

f:130 [binder, in Coq.Classes.RelationClasses]

f:130 [binder, in Coq.Init.Nat]

f:130 [binder, in Coq.QArith.QArith_base]

f:131 [binder, in Coq.Vectors.VectorSpec]

f:131 [binder, in Coq.Reals.Ranalysis1]

f:131 [binder, in Coq.micromega.RingMicromega]

f:131 [binder, in Coq.FSets.FMapFullAVL]

f:131 [binder, in Coq.ssr.ssrfun]

f:131 [binder, in Coq.Reals.Abstract.ConstructiveLimits]

f:131 [binder, in Coq.micromega.ZMicromega]

f:132 [binder, in Coq.MSets.MSetEqProperties]

f:132 [binder, in Coq.FSets.FSetEqProperties]

f:133 [binder, in Coq.MSets.MSetInterface]

f:133 [binder, in Coq.micromega.RingMicromega]

f:133 [binder, in Coq.Reals.Rsqrt_def]

f:133 [binder, in Coq.Logic.FinFun]

f:134 [binder, in Coq.Floats.SpecFloat]

f:134 [binder, in Coq.Reals.RiemannInt]

f:135 [binder, in Coq.Reals.MVT]

f:135 [binder, in Coq.Logic.FinFun]

f:136 [binder, in Coq.MSets.MSetInterface]

f:136 [binder, in Coq.MSets.MSetProperties]

f:136 [binder, in Coq.Floats.SpecFloat]

f:136 [binder, in Coq.FSets.FSetProperties]

f:137 [binder, in Coq.Logic.FinFun]

f:1372 [binder, in Coq.FSets.FMapAVL]

f:1374 [binder, in Coq.FSets.FMapAVL]

f:1376 [binder, in Coq.FSets.FMapAVL]

f:138 [binder, in Coq.Vectors.VectorSpec]

f:138 [binder, in Coq.micromega.ZMicromega]

f:1382 [binder, in Coq.FSets.FMapAVL]

f:139 [binder, in Coq.Floats.SpecFloat]

F:139 [binder, in Coq.Logic.Hurkens]

f:139 [binder, in Coq.micromega.Tauto]

f:14 [binder, in Coq.Logic.Hurkens]

f:14 [binder, in Coq.Reals.NewtonInt]

f:14 [binder, in Coq.Sets.Multiset]

f:14 [binder, in Coq.Sets.Image]

f:140 [binder, in Coq.MSets.MSetProperties]

f:140 [binder, in Coq.Reals.MVT]

f:140 [binder, in Coq.FSets.FSetProperties]

f:140 [binder, in Coq.Logic.FinFun]

f:141 [binder, in Coq.Reals.RiemannInt_SF]

f:142 [binder, in Coq.Reals.PSeries_reg]

f:142 [binder, in Coq.Reals.RiemannInt_SF]

F:143 [binder, in Coq.Arith.Wf_nat]

f:143 [binder, in Coq.Logic.FunctionalExtensionality]

F:143 [binder, in Coq.Logic.Hurkens]

f:143 [binder, in Coq.ssr.ssrfun]

f:143 [binder, in Coq.micromega.Tauto]

f:143 [binder, in Coq.Logic.FinFun]

f:1438 [binder, in Coq.FSets.FMapAVL]

f:144 [binder, in Coq.Reals.Ranalysis1]

f:144 [binder, in Coq.Sorting.PermutSetoid]

f:145 [binder, in Coq.Reals.Rderiv]

f:145 [binder, in Coq.Vectors.VectorSpec]

f:145 [binder, in Coq.MSets.MSetWeakList]

f:145 [binder, in Coq.Logic.Hurkens]

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

f:145 [binder, in Coq.micromega.Tauto]

f:145 [binder, in Coq.Logic.FinFun]

f:146 [binder, in Coq.Reals.MVT]

f:147 [binder, in Coq.Logic.FunctionalExtensionality]

f:147 [binder, in Coq.micromega.ZMicromega]

f:1475 [binder, in Coq.FSets.FMapAVL]

f:148 [binder, in Coq.Floats.SpecFloat]

f:148 [binder, in Coq.MSets.MSetWeakList]

f:148 [binder, in Coq.Reals.PSeries_reg]

f:148 [binder, in Coq.Logic.ClassicalFacts]

f:148 [binder, in Coq.Lists.SetoidList]

f:1480 [binder, in Coq.FSets.FMapAVL]

f:1486 [binder, in Coq.FSets.FMapAVL]

f:1492 [binder, in Coq.FSets.FMapAVL]

f:1499 [binder, in Coq.FSets.FMapAVL]

f:15 [binder, in Coq.Logic.SetoidChoice]

f:15 [binder, in Coq.Logic.FunctionalExtensionality]

f:15 [binder, in Coq.Reals.RiemannInt]

f:15 [binder, in Coq.Logic.ClassicalChoice]

f:15 [binder, in Coq.Logic.IndefiniteDescription]

f:15 [binder, in Coq.Sets.Image]

f:150 [binder, in Coq.MSets.MSetWeakList]

f:150 [binder, in Coq.Lists.ListSet]

f:1506 [binder, in Coq.FSets.FMapAVL]

f:151 [binder, in Coq.Reals.RiemannInt_SF]

f:152 [binder, in Coq.Vectors.VectorSpec]

f:153 [binder, in Coq.MSets.MSetWeakList]

F:154 [binder, in Coq.Logic.Hurkens]

f:154 [binder, in Coq.Reals.PSeries_reg]

f:154 [binder, in Coq.Lists.SetoidList]

f:155 [binder, in Coq.Reals.MVT]

f:155 [binder, in Coq.Logic.ClassicalFacts]

f:156 [binder, in Coq.Reals.Ranalysis1]

f:156 [binder, in Coq.MSets.MSetWeakList]

F:158 [binder, in Coq.Logic.Hurkens]

f:158 [binder, in Coq.Lists.ListSet]

f:158 [binder, in Coq.Reals.RiemannInt_SF]

f:159 [binder, in Coq.MSets.MSetWeakList]

f:159 [binder, in Coq.micromega.ZMicromega]

f:16 [binder, in Coq.MSets.MSetWeakList]

f:16 [binder, in Coq.Logic.ClassicalUniqueChoice]

f:16 [binder, in Coq.Numbers.Natural.Abstract.NAxioms]

f:160 [binder, in Coq.micromega.RingMicromega]

f:161 [binder, in Coq.Vectors.VectorSpec]

f:161 [binder, in Coq.Reals.Ranalysis1]

f:161 [binder, in Coq.Reals.Rfunctions]

f:161 [binder, in Coq.MSets.MSetWeakList]

F:161 [binder, in Coq.Logic.Hurkens]

f:164 [binder, in Coq.Reals.Ranalysis5]

f:164 [binder, in Coq.micromega.ZMicromega]

f:165 [binder, in Coq.MSets.MSetWeakList]

f:165 [binder, in Coq.Reals.RiemannInt_SF]

f:165 [binder, in Coq.micromega.Tauto]

f:166 [binder, in Coq.Reals.Ranalysis1]

f:167 [binder, in Coq.Reals.Rfunctions]

F:167 [binder, in Coq.Logic.Hurkens]

f:169 [binder, in Coq.MSets.MSetInterface]

f:169 [binder, in Coq.MSets.MSetWeakList]

F:169 [binder, in Coq.Logic.Hurkens]

f:169 [binder, in Coq.ssr.ssrfun]

f:17 [binder, in Coq.Numbers.NaryFunctions]

f:17 [binder, in Coq.Floats.FloatOps]

f:17 [binder, in Coq.rtauto.Bintree]

F:17 [binder, in Coq.micromega.DeclConstant]

f:17 [binder, in Coq.MSets.MSetGenTree]

f:17 [binder, in Coq.Sets.Image]

f:17 [binder, in Coq.Program.Basics]

f:17 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:170 [binder, in Coq.Vectors.VectorSpec]

f:170 [binder, in Coq.Reals.Ranalysis1]

f:170 [binder, in Coq.micromega.RingMicromega]

f:171 [binder, in Coq.micromega.ZMicromega]

f:172 [binder, in Coq.Reals.MVT]

f:172 [binder, in Coq.Classes.Morphisms]

f:172 [binder, in Coq.FSets.FMapFacts]

f:172 [binder, in Coq.MSets.MSetWeakList]

f:173 [binder, in Coq.Init.Logic]

f:173 [binder, in Coq.micromega.ZMicromega]

f:174 [binder, in Coq.Reals.Ranalysis1]

f:174 [binder, in Coq.Reals.Rfunctions]

f:175 [binder, in Coq.MSets.MSetWeakList]

f:176 [binder, in Coq.Reals.RiemannInt_SF]

f:177 [binder, in Coq.PArith.BinPos]

f:177 [binder, in Coq.FSets.FMapFacts]

f:178 [binder, in Coq.Reals.Ranalysis1]

F:178 [binder, in Coq.Logic.Hurkens]

f:178 [binder, in Coq.MSets.MSetRBT]

f:178 [binder, in Coq.FSets.FSetCompat]

f:179 [binder, in Coq.ssr.ssrfun]

f:179 [binder, in Coq.FSets.FMapPositive]

f:179 [binder, in Coq.FSets.FSetCompat]

f:18 [binder, in Coq.Program.Wf]

f:18 [binder, in Coq.Reals.Ranalysis4]

f:18 [binder, in Coq.Numbers.DecimalQ]

f:18 [binder, in Coq.Logic.ChoiceFacts]

f:18 [binder, in Coq.Reals.NewtonInt]

f:18 [binder, in Coq.Reals.Ranalysis5]

f:18 [binder, in Coq.Numbers.HexadecimalQ]

f:18 [binder, in Coq.Reals.ClassicalDedekindReals]

f:18 [binder, in Coq.btauto.Reflect]

f:180 [binder, in Coq.Reals.Rfunctions]

f:180 [binder, in Coq.FSets.FMapFacts]

f:180 [binder, in Coq.Reals.Ranalysis5]

f:180 [binder, in Coq.FSets.FSetCompat]

F:181 [binder, in Coq.Logic.Hurkens]

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

f:181 [binder, in Coq.Reals.RiemannInt_SF]

f:181 [binder, in Coq.FSets.FSetCompat]

f:182 [binder, in Coq.Reals.Ranalysis1]

f:182 [binder, in Coq.Classes.Morphisms]

f:183 [binder, in Coq.FSets.FMapFacts]

f:183 [binder, in Coq.MSets.MSetRBT]

f:183 [binder, in Coq.FSets.FMapPositive]

F:183 [binder, in Coq.Reals.Rtopology]

f:183 [binder, in Coq.micromega.ZMicromega]

f:183 [binder, in Coq.FSets.FSetCompat]

F:184 [binder, in Coq.Logic.Hurkens]

f:184 [binder, in Coq.Structures.GenericMinMax]

F:184 [binder, in Coq.Logic.ClassicalFacts]

f:184 [binder, in Coq.Reals.RiemannInt_SF]

f:185 [binder, in Coq.PArith.BinPos]

f:185 [binder, in Coq.micromega.ZMicromega]

f:185 [binder, in Coq.FSets.FSetCompat]

f:186 [binder, in Coq.Reals.Ranalysis1]

f:186 [binder, in Coq.Reals.RiemannInt]

F:186 [binder, in Coq.Logic.ClassicalFacts]

f:186 [binder, in Coq.micromega.Tauto]

f:187 [binder, in Coq.Classes.Morphisms]

f:187 [binder, in Coq.FSets.FMapFullAVL]

F:187 [binder, in Coq.Logic.Hurkens]

f:187 [binder, in Coq.Structures.GenericMinMax]

f:188 [binder, in Coq.Reals.RiemannInt_SF]

f:189 [binder, in Coq.Reals.Ranalysis1]

f:189 [binder, in Coq.PArith.BinPos]

f:189 [binder, in Coq.Init.Specif]

f:189 [binder, in Coq.FSets.FMapPositive]

f:19 [binder, in Coq.Reals.Ranalysis1]

f:19 [binder, in Coq.Sets.Image]

f:19 [binder, in Coq.Reals.ClassicalDedekindReals]

f:19 [binder, in Coq.btauto.Reflect]

f:190 [binder, in Coq.Reals.RiemannInt]

f:191 [binder, in Coq.Reals.MVT]

f:191 [binder, in Coq.micromega.Tauto]

f:191 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:192 [binder, in Coq.FSets.FMapFacts]

f:192 [binder, in Coq.MSets.MSetRBT]

f:192 [binder, in Coq.Logic.ClassicalFacts]

f:193 [binder, in Coq.PArith.BinPos]

f:194 [binder, in Coq.Reals.Ranalysis1]

f:195 [binder, in Coq.Classes.Morphisms]

f:195 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:196 [binder, in Coq.MSets.MSetRBT]

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

f:197 [binder, in Coq.Logic.ChoiceFacts]

f:197 [binder, in Coq.FSets.FMapPositive]

f:197 [binder, in Coq.micromega.Tauto]

f:198 [binder, in Coq.PArith.BinPos]

f:198 [binder, in Coq.Logic.ClassicalFacts]

f:198 [binder, in Coq.Vectors.VectorDef]

f:199 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

F:2 [binder, in Coq.micromega.DeclConstant]

f:2 [binder, in Coq.Reals.Abstract.ConstructiveSum]

f:2 [binder, in Coq.Logic.Adjointification]

f:20 [binder, in Coq.Reals.Ranalysis4]

f:20 [binder, in Coq.Logic.ExtensionalityFacts]

f:20 [binder, in Coq.Logic.Hurkens]

f:20 [binder, in Coq.Reals.NewtonInt]

f:200 [binder, in Coq.Reals.Rtopology]

f:201 [binder, in Coq.Reals.Ranalysis1]

f:201 [binder, in Coq.PArith.BinPos]

f:201 [binder, in Coq.micromega.RingMicromega]

f:201 [binder, in Coq.MSets.MSetRBT]

f:202 [binder, in Coq.Reals.RiemannInt]

f:202 [binder, in Coq.Classes.CMorphisms]

f:203 [binder, in Coq.FSets.FMapPositive]

f:203 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:204 [binder, in Coq.Reals.RiemannInt]

f:204 [binder, in Coq.Reals.Rtopology]

f:204 [binder, in Coq.Reals.RiemannInt_SF]

f:205 [binder, in Coq.Reals.Ranalysis1]

f:205 [binder, in Coq.micromega.RingMicromega]

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

f:207 [binder, in Coq.Reals.Ranalysis1]

f:208 [binder, in Coq.Reals.RiemannInt]

f:209 [binder, in Coq.PArith.BinPos]

f:209 [binder, in Coq.FSets.FMapPositive]

f:209 [binder, in Coq.micromega.Tauto]

f:209 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:21 [binder, in Coq.Logic.FunctionalExtensionality]

f:21 [binder, in Coq.ssr.ssrfun]

f:21 [binder, in Coq.Lists.ListDec]

f:21 [binder, in Coq.rtauto.Bintree]

f:21 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:210 [binder, in Coq.Reals.RiemannInt_SF]

f:211 [binder, in Coq.Logic.Hurkens]

f:212 [binder, in Coq.micromega.RingMicromega]

f:212 [binder, in Coq.Logic.Hurkens]

f:212 [binder, in Coq.Sorting.Permutation]

f:212 [binder, in Coq.Classes.CMorphisms]

f:213 [binder, in Coq.Logic.Hurkens]

f:214 [binder, in Coq.Logic.Hurkens]

f:214 [binder, in Coq.FSets.FMapPositive]

f:214 [binder, in Coq.Structures.GenericMinMax]

f:215 [binder, in Coq.Logic.Hurkens]

f:215 [binder, in Coq.Sorting.Permutation]

f:215 [binder, in Coq.micromega.Tauto]

f:216 [binder, in Coq.Logic.Hurkens]

f:216 [binder, in Coq.Vectors.VectorDef]

f:217 [binder, in Coq.MSets.MSetList]

f:217 [binder, in Coq.Logic.Hurkens]

f:217 [binder, in Coq.Classes.CMorphisms]

f:217 [binder, in Coq.MSets.MSetRBT]

f:217 [binder, in Coq.Reals.Rtopology]

f:217 [binder, in Coq.Structures.GenericMinMax]

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

f:217 [binder, in Coq.micromega.Tauto]

f:218 [binder, in Coq.Logic.Hurkens]

f:218 [binder, in Coq.Sorting.Permutation]

f:22 [binder, in Coq.Classes.RelationPairs]

f:22 [binder, in Coq.Reals.RiemannInt]

f:22 [binder, in Coq.Reals.NewtonInt]

f:22 [binder, in Coq.Sets.Image]

f:22 [binder, in Coq.Program.Basics]

f:220 [binder, in Coq.Structures.GenericMinMax]

F:221 [binder, in Coq.Logic.Hurkens]

f:221 [binder, in Coq.MSets.MSetRBT]

f:222 [binder, in Coq.MSets.MSetList]

f:222 [binder, in Coq.Sorting.Permutation]

f:222 [binder, in Coq.Classes.CMorphisms]

F:223 [binder, in Coq.Logic.Hurkens]

f:223 [binder, in Coq.Structures.GenericMinMax]

f:223 [binder, in Coq.Reals.Abstract.ConstructiveSum]

f:224 [binder, in Coq.FSets.FMapFullAVL]

f:225 [binder, in Coq.MSets.MSetList]

F:225 [binder, in Coq.Logic.Hurkens]

f:225 [binder, in Coq.MSets.MSetPositive]

f:225 [binder, in Coq.Reals.Rtopology]

f:226 [binder, in Coq.MSets.MSetInterface]

f:226 [binder, in Coq.Sorting.Permutation]

f:226 [binder, in Coq.MSets.MSetRBT]

f:226 [binder, in Coq.Reals.RiemannInt_SF]

f:226 [binder, in Coq.micromega.Tauto]

F:227 [binder, in Coq.Logic.Hurkens]

f:227 [binder, in Coq.Vectors.VectorDef]

f:229 [binder, in Coq.MSets.MSetInterface]

f:229 [binder, in Coq.MSets.MSetList]

f:229 [binder, in Coq.FSets.FMapFullAVL]

f:23 [binder, in Coq.Numbers.DecimalQ]

f:23 [binder, in Coq.Numbers.HexadecimalQ]

f:23 [binder, in Coq.FSets.FSetFacts]

f:23 [binder, in Coq.Reals.ClassicalDedekindReals]

f:230 [binder, in Coq.Classes.CMorphisms]

f:231 [binder, in Coq.MSets.MSetInterface]

f:231 [binder, in Coq.Reals.RiemannInt]

f:231 [binder, in Coq.MSets.MSetList]

f:232 [binder, in Coq.Reals.Ranalysis1]

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

f:233 [binder, in Coq.MSets.MSetInterface]

f:233 [binder, in Coq.micromega.RingMicromega]

f:233 [binder, in Coq.Reals.RiemannInt_SF]

f:234 [binder, in Coq.Reals.RiemannInt]

f:234 [binder, in Coq.MSets.MSetList]

f:234 [binder, in Coq.FSets.FMapWeakList]

f:235 [binder, in Coq.Reals.Ranalysis1]

f:235 [binder, in Coq.MSets.MSetInterface]

f:235 [binder, in Coq.micromega.RingMicromega]

f:235 [binder, in Coq.FSets.FMapFullAVL]

f:236 [binder, in Coq.FSets.FSetBridge]

f:236 [binder, in Coq.micromega.RingMicromega]

f:237 [binder, in Coq.MSets.MSetList]

f:238 [binder, in Coq.Reals.Ranalysis1]

f:238 [binder, in Coq.Classes.CMorphisms]

f:239 [binder, in Coq.FSets.FSetBridge]

f:24 [binder, in Coq.Reals.Ranalysis1]

f:24 [binder, in Coq.ssr.ssrfun]

f:24 [binder, in Coq.Logic.ClassicalUniqueChoice]

f:24 [binder, in Coq.Reals.RiemannInt_SF]

f:24 [binder, in Coq.micromega.Tauto]

f:24 [binder, in Coq.rtauto.Rtauto]

f:240 [binder, in Coq.Reals.RiemannInt]

f:240 [binder, in Coq.FSets.FSetInterface]

f:240 [binder, in Coq.FSets.FMapPositive]

f:240 [binder, in Coq.FSets.FMapWeakList]

f:241 [binder, in Coq.MSets.MSetList]

f:241 [binder, in Coq.FSets.FMapFullAVL]

f:241 [binder, in Coq.Reals.Abstract.ConstructiveSum]

f:241 [binder, in Coq.micromega.Tauto]

f:242 [binder, in Coq.Sorting.Permutation]

f:242 [binder, in Coq.FSets.FMapList]

f:243 [binder, in Coq.Reals.Ranalysis1]

f:244 [binder, in Coq.FSets.FMapWeakList]

f:244 [binder, in Coq.Reals.Ranalysis5]

f:244 [binder, in Coq.Reals.RiemannInt_SF]

f:244 [binder, in Coq.Vectors.VectorDef]

f:245 [binder, in Coq.MSets.MSetList]

f:246 [binder, in Coq.Reals.Ranalysis1]

f:246 [binder, in Coq.FSets.FSetBridge]

f:247 [binder, in Coq.MSets.MSetInterface]

f:247 [binder, in Coq.MSets.MSetPositive]

f:247 [binder, in Coq.Reals.Abstract.ConstructiveSum]

f:248 [binder, in Coq.MSets.MSetList]

f:248 [binder, in Coq.FSets.FMapFullAVL]

f:248 [binder, in Coq.Sorting.Permutation]

f:248 [binder, in Coq.Init.Logic]

f:248 [binder, in Coq.FSets.FMapList]

f:249 [binder, in Coq.FSets.FSetBridge]

f:249 [binder, in Coq.FSets.FMapWeakList]

f:25 [binder, in Coq.Floats.FloatLemmas]

f:25 [binder, in Coq.Classes.RelationPairs]

f:25 [binder, in Coq.Reals.RiemannInt]

f:25 [binder, in Coq.Sets.Image]

f:25 [binder, in Coq.Sets.Infinite_sets]

f:25 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:251 [binder, in Coq.FSets.FSetBridge]

f:251 [binder, in Coq.MSets.MSetList]

f:251 [binder, in Coq.FSets.FMapPositive]

f:251 [binder, in Coq.Reals.Abstract.ConstructiveSum]

f:251 [binder, in Coq.micromega.ZMicromega]

f:252 [binder, in Coq.FSets.FMapList]

f:252 [binder, in Coq.Reals.RiemannInt_SF]

f:253 [binder, in Coq.FSets.FSetBridge]

f:253 [binder, in Coq.MSets.MSetList]

f:253 [binder, in Coq.MSets.MSetPositive]

f:254 [binder, in Coq.MSets.MSetPositive]

f:254 [binder, in Coq.FSets.FMapWeakList]

f:255 [binder, in Coq.Reals.RiemannInt]

f:255 [binder, in Coq.FSets.FMapFullAVL]

f:256 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]

f:257 [binder, in Coq.Reals.Ranalysis5]

f:257 [binder, in Coq.FSets.FMapList]

f:257 [binder, in Coq.Reals.RiemannInt_SF]

f:257 [binder, in Coq.Lists.SetoidList]

f:258 [binder, in Coq.FSets.FMapPositive]

f:258 [binder, in Coq.Logic.ClassicalFacts]

f:259 [binder, in Coq.FSets.FSetBridge]

f:259 [binder, in Coq.Logic.EqdepFacts]

f:259 [binder, in Coq.MSets.MSetPositive]

f:259 [binder, in Coq.Lists.SetoidList]

f:26 [binder, in Coq.Reals.Ranalysis1]

f:26 [binder, in Coq.Logic.ExtensionalityFacts]

F:26 [binder, in Coq.Logic.Hurkens]

f:26 [binder, in Coq.Logic.ClassicalUniqueChoice]

f:26 [binder, in Coq.Reals.NewtonInt]

f:26 [binder, in Coq.Logic.ClassicalDescription]

f:26 [binder, in Coq.FSets.FSetFacts]

f:261 [binder, in Coq.MSets.MSetPositive]

f:261 [binder, in Coq.Reals.RiemannInt_SF]

f:262 [binder, in Coq.FSets.FSetBridge]

f:262 [binder, in Coq.FSets.FMapList]

f:262 [binder, in Coq.Lists.SetoidList]

f:263 [binder, in Coq.micromega.RingMicromega]

f:263 [binder, in Coq.NArith.BinNat]

f:265 [binder, in Coq.FSets.FSetBridge]

f:266 [binder, in Coq.FSets.FSetBridge]

f:266 [binder, in Coq.MSets.MSetPositive]

f:267 [binder, in Coq.micromega.RingMicromega]

f:269 [binder, in Coq.MSets.MSetPositive]

f:27 [binder, in Coq.Reals.MVT]

f:27 [binder, in Coq.Logic.ChoiceFacts]

f:27 [binder, in Coq.Classes.CMorphisms]

f:27 [binder, in Coq.Reals.ClassicalDedekindReals]

f:270 [binder, in Coq.FSets.FSetBridge]

f:270 [binder, in Coq.micromega.RingMicromega]

f:270 [binder, in Coq.Init.Specif]

f:271 [binder, in Coq.ssr.ssrbool]

f:271 [binder, in Coq.NArith.BinNat]

f:271 [binder, in Coq.Reals.RiemannInt_SF]

f:271 [binder, in Coq.micromega.Tauto]

f:272 [binder, in Coq.MSets.MSetPositive]

f:273 [binder, in Coq.FSets.FSetBridge]

f:273 [binder, in Coq.micromega.RingMicromega]

f:273 [binder, in Coq.Reals.Rtopology]

f:274 [binder, in Coq.Logic.EqdepFacts]

f:274 [binder, in Coq.FSets.FMapFacts]

f:274 [binder, in Coq.MSets.MSetPositive]

f:275 [binder, in Coq.FSets.FSetBridge]

f:275 [binder, in Coq.NArith.BinNat]

f:276 [binder, in Coq.Lists.SetoidList]

F:277 [binder, in Coq.Logic.Hurkens]

f:277 [binder, in Coq.Reals.RiemannInt_SF]

f:279 [binder, in Coq.FSets.FSetBridge]

f:279 [binder, in Coq.NArith.BinNat]

f:28 [binder, in Coq.Classes.Morphisms]

f:28 [binder, in Coq.Classes.RelationPairs]

f:28 [binder, in Coq.MSets.MSetFacts]

f:28 [binder, in Coq.MSets.MSetWeakList]

f:28 [binder, in Coq.Logic.ClassicalFacts]

F:28 [binder, in Coq.rtauto.Rtauto]

F:280 [binder, in Coq.Logic.Hurkens]

f:280 [binder, in Coq.FSets.FMapWeakList]

f:282 [binder, in Coq.FSets.FSetBridge]

f:282 [binder, in Coq.FSets.FMapPositive]

f:283 [binder, in Coq.MSets.MSetProperties]

f:283 [binder, in Coq.Init.Logic]

f:283 [binder, in Coq.Reals.RiemannInt_SF]

f:283 [binder, in Coq.FSets.FSetProperties]

f:284 [binder, in Coq.FSets.FSetBridge]

f:284 [binder, in Coq.NArith.BinNat]

f:286 [binder, in Coq.FSets.FMapFacts]

F:286 [binder, in Coq.Logic.Hurkens]

f:286 [binder, in Coq.Reals.Rtopology]

f:287 [binder, in Coq.NArith.BinNat]

F:288 [binder, in Coq.Logic.Hurkens]

f:288 [binder, in Coq.FSets.FMapList]

f:289 [binder, in Coq.FSets.FSetBridge]

f:289 [binder, in Coq.FSets.FMapFacts]

f:289 [binder, in Coq.Reals.RiemannInt_SF]

f:29 [binder, in Coq.MSets.MSetProperties]

f:29 [binder, in Coq.Floats.FloatLemmas]

f:29 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]

f:29 [binder, in Coq.Classes.CEquivalence]

f:29 [binder, in Coq.FSets.FSetProperties]

f:29 [binder, in Coq.Classes.Equivalence]

F:290 [binder, in Coq.Logic.Hurkens]

f:291 [binder, in Coq.FSets.FSetBridge]

f:291 [binder, in Coq.MSets.MSetProperties]

f:291 [binder, in Coq.Logic.Hurkens]

f:291 [binder, in Coq.FSets.FSetProperties]

f:292 [binder, in Coq.Init.Specif]

F:293 [binder, in Coq.Logic.Hurkens]

f:294 [binder, in Coq.Reals.Ranalysis1]

f:294 [binder, in Coq.Logic.Hurkens]

f:294 [binder, in Coq.Reals.RiemannInt_SF]

f:295 [binder, in Coq.NArith.BinNat]

f:295 [binder, in Coq.micromega.ZMicromega]

f:296 [binder, in Coq.Reals.Rtopology]

f:296 [binder, in Coq.micromega.Tauto]

f:297 [binder, in Coq.micromega.ZMicromega]

f:298 [binder, in Coq.Reals.Ranalysis1]

f:298 [binder, in Coq.Reals.RiemannInt]

f:298 [binder, in Coq.Lists.SetoidList]

f:3 [binder, in Coq.Reals.Ranalysis4]

f:3 [binder, in Coq.Floats.PrimFloat]

f:3 [binder, in Coq.Logic.ExtensionalityFacts]

f:3 [binder, in Coq.Logic.FunctionalExtensionality]

f:3 [binder, in Coq.Relations.Relations]

f:3 [binder, in Coq.Program.Combinators]

f:3 [binder, in Coq.ZArith.Zmisc]

f:3 [binder, in Coq.Logic.FinFun]

f:30 [binder, in Coq.MSets.MSetFacts]

f:30 [binder, in Coq.Reals.NewtonInt]

f:30 [binder, in Coq.Reals.RiemannInt_SF]

f:30 [binder, in Coq.micromega.Tauto]

f:30 [binder, in Coq.Reals.ClassicalDedekindReals]

f:30 [binder, in Coq.Sets.Infinite_sets]

f:30 [binder, in Coq.Logic.FinFun]

f:300 [binder, in Coq.Reals.RiemannInt_SF]

f:300 [binder, in Coq.micromega.Tauto]

f:301 [binder, in Coq.FSets.FSetPositive]

f:301 [binder, in Coq.Lists.SetoidList]

f:302 [binder, in Coq.micromega.RingMicromega]

f:302 [binder, in Coq.Init.Specif]

f:303 [binder, in Coq.ssr.ssrbool]

f:303 [binder, in Coq.micromega.Tauto]

f:304 [binder, in Coq.MSets.MSetGenTree]

f:305 [binder, in Coq.Reals.Ranalysis1]

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

f:306 [binder, in Coq.Reals.Rtopology]

f:306 [binder, in Coq.Reals.RiemannInt_SF]

f:307 [binder, in Coq.micromega.RingMicromega]

f:307 [binder, in Coq.MSets.MSetGenTree]

f:307 [binder, in Coq.Reals.Ranalysis5]

f:309 [binder, in Coq.Lists.SetoidList]

f:31 [binder, in Coq.Reals.Ranalysis1]

f:31 [binder, in Coq.Classes.RelationPairs]

F:31 [binder, in Coq.Logic.Hurkens]

f:31 [binder, in Coq.NArith.Nnat]

f:31 [binder, in Coq.Logic.ClassicalFacts]

f:31 [binder, in Coq.FSets.FSetFacts]

F:31 [binder, in Coq.btauto.Reflect]

f:31 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:310 [binder, in Coq.MSets.MSetGenTree]

f:311 [binder, in Coq.Vectors.VectorSpec]

f:312 [binder, in Coq.FSets.FMapFacts]

f:313 [binder, in Coq.Init.Specif]

f:313 [binder, in Coq.Reals.RiemannInt_SF]

f:314 [binder, in Coq.micromega.RingMicromega]

f:314 [binder, in Coq.Init.Logic]

f:314 [binder, in Coq.Reals.RiemannInt_SF]

F:315 [binder, in Coq.Reals.Rtopology]

f:316 [binder, in Coq.Vectors.VectorSpec]

f:316 [binder, in Coq.Reals.Ranalysis5]

f:317 [binder, in Coq.Reals.Ranalysis1]

f:317 [binder, in Coq.Reals.Rtopology]

f:317 [binder, in Coq.MSets.MSetGenTree]

f:32 [binder, in Coq.MSets.MSetProperties]

f:32 [binder, in Coq.Logic.ExtensionalityFacts]

f:32 [binder, in Coq.MSets.MSetFacts]

f:32 [binder, in Coq.MSets.MSetWeakList]

f:32 [binder, in Coq.FSets.FSetProperties]

f:320 [binder, in Coq.Reals.Ranalysis1]

f:320 [binder, in Coq.Reals.Rtopology]

f:322 [binder, in Coq.Vectors.VectorSpec]

f:322 [binder, in Coq.Reals.Ranalysis1]

f:322 [binder, in Coq.Reals.RiemannInt_SF]

f:323 [binder, in Coq.Init.Specif]

f:323 [binder, in Coq.FSets.FSetPositive]

f:323 [binder, in Coq.Reals.Ranalysis5]

f:324 [binder, in Coq.Reals.Ranalysis1]

f:324 [binder, in Coq.FSets.FMapFacts]

f:324 [binder, in Coq.Reals.Rtopology]

f:326 [binder, in Coq.Reals.Ranalysis1]

f:326 [binder, in Coq.micromega.Tauto]

f:327 [binder, in Coq.FSets.FMapPositive]

f:328 [binder, in Coq.Reals.Ranalysis1]

F:328 [binder, in Coq.Logic.Hurkens]

f:328 [binder, in Coq.Reals.RiemannInt_SF]

f:329 [binder, in Coq.ssr.ssrbool]

f:329 [binder, in Coq.FSets.FSetPositive]

f:329 [binder, in Coq.Reals.RiemannInt_SF]

f:33 [binder, in Coq.Floats.FloatLemmas]

f:33 [binder, in Coq.Logic.Hurkens]

f:33 [binder, in Coq.Reals.ClassicalDedekindReals]

F:33 [binder, in Coq.rtauto.Rtauto]

f:330 [binder, in Coq.Reals.RiemannInt]

f:330 [binder, in Coq.Reals.Ranalysis5]

F:331 [binder, in Coq.Logic.Hurkens]

f:331 [binder, in Coq.micromega.Tauto]

f:332 [binder, in Coq.FSets.FMapFacts]

f:332 [binder, in Coq.FSets.FSetPositive]

f:333 [binder, in Coq.FSets.FMapWeakList]

f:334 [binder, in Coq.FSets.FMapPositive]

f:335 [binder, in Coq.FSets.FSetPositive]

f:336 [binder, in Coq.FSets.FSetPositive]

f:336 [binder, in Coq.Reals.RiemannInt_SF]

F:337 [binder, in Coq.Logic.Hurkens]

f:337 [binder, in Coq.FSets.FMapWeakList]

f:337 [binder, in Coq.Init.Logic]

f:339 [binder, in Coq.Reals.RiemannInt]

F:339 [binder, in Coq.Logic.Hurkens]

f:34 [binder, in Coq.Reals.Ranalysis1]

f:34 [binder, in Coq.Classes.RelationPairs]

f:34 [binder, in Coq.Logic.ClassicalFacts]

f:34 [binder, in Coq.Reals.ClassicalDedekindReals]

f:341 [binder, in Coq.Reals.Ranalysis1]

f:341 [binder, in Coq.ssr.ssrbool]

f:341 [binder, in Coq.Logic.Hurkens]

f:341 [binder, in Coq.FSets.FSetPositive]

f:342 [binder, in Coq.Init.Logic]

f:343 [binder, in Coq.Logic.Hurkens]

f:344 [binder, in Coq.FSets.FSetPositive]

f:345 [binder, in Coq.FSets.FMapFacts]

F:345 [binder, in Coq.Logic.Hurkens]

f:345 [binder, in Coq.Reals.RiemannInt_SF]

f:346 [binder, in Coq.FSets.FSetPositive]

f:346 [binder, in Coq.FSets.FMapWeakList]

f:347 [binder, in Coq.Reals.Ranalysis1]

F:347 [binder, in Coq.Logic.Hurkens]

f:348 [binder, in Coq.Reals.Ranalysis1]

f:348 [binder, in Coq.Reals.Ranalysis5]

F:349 [binder, in Coq.Logic.Hurkens]

f:349 [binder, in Coq.FSets.FMapWeakList]

f:35 [binder, in Coq.Reals.RiemannInt]

f:35 [binder, in Coq.Logic.FinFun]

F:351 [binder, in Coq.Logic.Hurkens]

f:351 [binder, in Coq.FSets.FSetPositive]

f:351 [binder, in Coq.Init.Logic]

f:352 [binder, in Coq.FSets.FMapWeakList]

f:353 [binder, in Coq.Reals.RiemannInt_SF]

f:354 [binder, in Coq.FSets.FSetPositive]

f:356 [binder, in Coq.Reals.Ranalysis1]

f:356 [binder, in Coq.FSets.FMapWeakList]

f:356 [binder, in Coq.Reals.RiemannInt_SF]

f:357 [binder, in Coq.FSets.FSetPositive]

f:357 [binder, in Coq.Init.Logic]

f:36 [binder, in Coq.Numbers.DecimalQ]

f:36 [binder, in Coq.MSets.MSetWeakList]

F:36 [binder, in Coq.Logic.Hurkens]

f:36 [binder, in Coq.ssr.ssrfun]

f:36 [binder, in Coq.Reals.Rlimit]

f:36 [binder, in Coq.Numbers.HexadecimalQ]

F:36 [binder, in Coq.rtauto.Rtauto]

f:360 [binder, in Coq.FSets.FSetPositive]

f:360 [binder, in Coq.FSets.FMapWeakList]

f:362 [binder, in Coq.FSets.FSetPositive]

f:363 [binder, in Coq.FSets.FMapWeakList]

f:364 [binder, in Coq.Reals.Ranalysis1]

f:364 [binder, in Coq.Reals.Ranalysis5]

f:364 [binder, in Coq.Init.Logic]

f:365 [binder, in Coq.Reals.RiemannInt_SF]

f:365 [binder, in Coq.micromega.Tauto]

f:366 [binder, in Coq.Logic.ChoiceFacts]

f:367 [binder, in Coq.Reals.Ranalysis1]

f:369 [binder, in Coq.Logic.ChoiceFacts]

f:37 [binder, in Coq.Sorting.PermutEq]

f:37 [binder, in Coq.Reals.Ranalysis1]

f:37 [binder, in Coq.Numbers.HexadecimalPos]

f:37 [binder, in Coq.Floats.FloatLemmas]

f:37 [binder, in Coq.Classes.RelationPairs]

f:37 [binder, in Coq.Logic.ChoiceFacts]

f:37 [binder, in Coq.Numbers.DecimalPos]

f:37 [binder, in Coq.Reals.RiemannInt_SF]

f:37 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:370 [binder, in Coq.Reals.Ranalysis1]

f:371 [binder, in Coq.micromega.ZMicromega]

f:372 [binder, in Coq.Reals.Ranalysis5]

f:373 [binder, in Coq.Reals.Ranalysis1]

f:373 [binder, in Coq.Reals.RiemannInt_SF]

f:373 [binder, in Coq.micromega.Tauto]

f:374 [binder, in Coq.FSets.FMapList]

f:374 [binder, in Coq.micromega.ZMicromega]

f:374 [binder, in Coq.micromega.Tauto]

f:376 [binder, in Coq.Reals.RiemannInt_SF]

f:377 [binder, in Coq.Reals.RiemannInt]

f:378 [binder, in Coq.FSets.FMapWeakList]

f:378 [binder, in Coq.FSets.FMapList]

f:38 [binder, in Coq.PArith.Pnat]

f:38 [binder, in Coq.Logic.ExtensionalityFacts]

f:38 [binder, in Coq.Logic.Hurkens]

f:38 [binder, in Coq.micromega.Tauto]

f:38 [binder, in Coq.Sets.Infinite_sets]

f:381 [binder, in Coq.Reals.Rtopology]

f:381 [binder, in Coq.Reals.Ranalysis5]

f:387 [binder, in Coq.FSets.FMapList]

f:388 [binder, in Coq.micromega.Tauto]

f:389 [binder, in Coq.micromega.Tauto]

f:39 [binder, in Coq.FSets.FSetBridge]

f:39 [binder, in Coq.Numbers.NaryFunctions]

f:39 [binder, in Coq.Numbers.DecimalQ]

f:39 [binder, in Coq.NArith.BinNat]

f:39 [binder, in Coq.MSets.MSetGenTree]

f:39 [binder, in Coq.Logic.ClassicalDescription]

f:39 [binder, in Coq.Numbers.HexadecimalQ]

f:390 [binder, in Coq.Reals.Ranalysis5]

f:390 [binder, in Coq.FSets.FMapList]

f:393 [binder, in Coq.Reals.Ranalysis1]

f:393 [binder, in Coq.micromega.Tauto]

f:394 [binder, in Coq.micromega.Tauto]

f:395 [binder, in Coq.FSets.FMapList]

f:395 [binder, in Coq.micromega.Tauto]

f:396 [binder, in Coq.micromega.Tauto]

f:398 [binder, in Coq.FSets.FMapList]

f:398 [binder, in Coq.micromega.Tauto]

f:399 [binder, in Coq.Reals.Ranalysis5]

f:4 [binder, in Coq.Reals.Rderiv]

f:4 [binder, in Coq.Logic.ExtensionalFunctionRepresentative]

f:4 [binder, in Coq.Reals.Ranalysis1]

f:4 [binder, in Coq.Floats.FloatLemmas]

f:4 [binder, in Coq.Floats.PrimFloat]

f:4 [binder, in Coq.Classes.RelationPairs]

f:4 [binder, in Coq.Floats.FloatOps]

f:4 [binder, in Coq.ZArith.Zpow_alt]

f:4 [binder, in Coq.Sets.Image]

f:4 [binder, in Coq.btauto.Reflect]

f:40 [binder, in Coq.Reals.Ranalysis1]

f:40 [binder, in Coq.Numbers.HexadecimalPos]

f:40 [binder, in Coq.Reals.MVT]

f:40 [binder, in Coq.MSets.MSetWeakList]

f:40 [binder, in Coq.Structures.GenericMinMax]

f:40 [binder, in Coq.Numbers.DecimalPos]

f:40 [binder, in Coq.Sets.Infinite_sets]

f:40 [binder, in Coq.Logic.FinFun]

F:40 [binder, in Coq.rtauto.Rtauto]

f:400 [binder, in Coq.MSets.MSetRBT]

f:400 [binder, in Coq.Reals.Rtopology]

f:400 [binder, in Coq.micromega.Tauto]

f:402 [binder, in Coq.FSets.FMapList]

f:404 [binder, in Coq.MSets.MSetRBT]

f:406 [binder, in Coq.FSets.FMapList]

f:409 [binder, in Coq.Lists.List]

f:41 [binder, in Coq.Classes.Morphisms]

f:41 [binder, in Coq.Classes.CMorphisms]

f:41 [binder, in Coq.Sets.Image]

f:410 [binder, in Coq.FSets.FMapList]

f:413 [binder, in Coq.FSets.FMapList]

f:416 [binder, in Coq.Reals.RiemannInt]

f:416 [binder, in Coq.Reals.Ranalysis5]

f:419 [binder, in Coq.MSets.MSetRBT]

f:42 [binder, in Coq.Logic.ClassicalEpsilon]

f:42 [binder, in Coq.Logic.ChoiceFacts]

f:42 [binder, in Coq.Init.Datatypes]

f:42 [binder, in Coq.Reals.RiemannInt_SF]

f:42 [binder, in Coq.micromega.Tauto]

f:42 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:422 [binder, in Coq.MSets.MSetRBT]

f:423 [binder, in Coq.Lists.List]

f:423 [binder, in Coq.Reals.RiemannInt]

f:425 [binder, in Coq.MSets.MSetRBT]

f:426 [binder, in Coq.Reals.Ranalysis1]

f:426 [binder, in Coq.micromega.Tauto]

f:427 [binder, in Coq.MSets.MSetRBT]

f:428 [binder, in Coq.Reals.RiemannInt]

f:428 [binder, in Coq.Logic.ChoiceFacts]

f:429 [binder, in Coq.Lists.List]

f:43 [binder, in Coq.Reals.Ranalysis1]

f:43 [binder, in Coq.Init.Wf]

f:43 [binder, in Coq.ssr.ssrfun]

f:43 [binder, in Coq.MSets.MSetGenTree]

f:43 [binder, in Coq.Logic.FinFun]

f:430 [binder, in Coq.Reals.Ranalysis1]

f:430 [binder, in Coq.Logic.ChoiceFacts]

f:430 [binder, in Coq.MSets.MSetRBT]

f:431 [binder, in Coq.setoid_ring.Field_theory]

f:432 [binder, in Coq.Logic.ChoiceFacts]

f:433 [binder, in Coq.Logic.ChoiceFacts]

f:433 [binder, in Coq.Init.Specif]

f:435 [binder, in Coq.Reals.Ranalysis1]

f:435 [binder, in Coq.Lists.List]

f:435 [binder, in Coq.Reals.RiemannInt]

f:435 [binder, in Coq.MSets.MSetRBT]

f:435 [binder, in Coq.micromega.Tauto]

f:438 [binder, in Coq.MSets.MSetRBT]

f:44 [binder, in Coq.Reals.PSeries_reg]

f:440 [binder, in Coq.MSets.MSetRBT]

f:441 [binder, in Coq.Reals.Ranalysis1]

f:441 [binder, in Coq.Lists.List]

f:442 [binder, in Coq.Reals.RiemannInt]

f:442 [binder, in Coq.micromega.ZMicromega]

f:443 [binder, in Coq.MSets.MSetRBT]

f:443 [binder, in Coq.Reals.Ranalysis5]

f:445 [binder, in Coq.micromega.ZMicromega]

f:446 [binder, in Coq.MSets.MSetRBT]

f:446 [binder, in Coq.FSets.FMapList]

f:447 [binder, in Coq.Lists.List]

f:449 [binder, in Coq.Reals.Ranalysis1]

f:449 [binder, in Coq.micromega.Tauto]

f:45 [binder, in Coq.Classes.Morphisms]

f:45 [binder, in Coq.MSets.MSetList]

f:45 [binder, in Coq.Vectors.Fin]

f:45 [binder, in Coq.Classes.SetoidDec]

f:45 [binder, in Coq.Structures.GenericMinMax]

f:45 [binder, in Coq.Reals.Rlimit]

f:45 [binder, in Coq.Sets.Image]

F:45 [binder, in Coq.rtauto.Rtauto]

f:450 [binder, in Coq.FSets.FMapFacts]

f:450 [binder, in Coq.Reals.RiemannInt]

f:450 [binder, in Coq.Init.Logic]

f:453 [binder, in Coq.Lists.List]

f:454 [binder, in Coq.Reals.RiemannInt]

f:454 [binder, in Coq.micromega.Tauto]

f:455 [binder, in Coq.Reals.Ranalysis1]

f:455 [binder, in Coq.FSets.FMapFacts]

f:455 [binder, in Coq.Init.Specif]

f:456 [binder, in Coq.Init.Logic]

f:458 [binder, in Coq.Reals.RiemannInt]

f:46 [binder, in Coq.Classes.CMorphisms]

f:46 [binder, in Coq.Reals.NewtonInt]

f:460 [binder, in Coq.FSets.FMapFacts]

f:462 [binder, in Coq.Reals.RiemannInt]

f:465 [binder, in Coq.FSets.FMapFacts]

f:465 [binder, in Coq.Init.Specif]

f:47 [binder, in Coq.Reals.Ranalysis1]

F:47 [binder, in Coq.Arith.Wf_nat]

f:47 [binder, in Coq.Logic.ChoiceFacts]

f:47 [binder, in Coq.Reals.Rlimit]

f:47 [binder, in Coq.Floats.FloatAxioms]

f:47 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:476 [binder, in Coq.Init.Specif]

f:48 [binder, in Coq.Logic.FunctionalExtensionality]

f:48 [binder, in Coq.MSets.MSetList]

f:48 [binder, in Coq.NArith.BinNat]

F:48 [binder, in Coq.Reals.NewtonInt]

f:48 [binder, in Coq.Sets.Image]

f:48 [binder, in Coq.PArith.BinPosDef]

f:48 [binder, in Coq.Logic.FinFun]

f:486 [binder, in Coq.Init.Specif]

f:489 [binder, in Coq.Lists.List]

f:49 [binder, in Coq.Reals.Ratan]

f:49 [binder, in Coq.micromega.ZMicromega]

f:49 [binder, in Coq.Floats.FloatAxioms]

f:495 [binder, in Coq.Lists.List]

f:497 [binder, in Coq.Reals.RiemannInt]

f:498 [binder, in Coq.ssr.ssrbool]

f:499 [binder, in Coq.micromega.Tauto]

f:5 [binder, in Coq.Floats.PrimFloat]

f:5 [binder, in Coq.Reals.NewtonInt]

F:5 [binder, in Coq.micromega.DeclConstant]

f:5 [binder, in Coq.Program.Basics]

f:5 [binder, in Coq.Numbers.Natural.Abstract.NStrongRec]

f:50 [binder, in Coq.Logic.JMeq]

f:50 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:501 [binder, in Coq.Lists.List]

f:504 [binder, in Coq.Reals.RiemannInt]

f:505 [binder, in Coq.FSets.FMapWeakList]

f:507 [binder, in Coq.FSets.FMapWeakList]

f:509 [binder, in Coq.FSets.FMapWeakList]

f:51 [binder, in Coq.Reals.Ranalysis1]

F:51 [binder, in Coq.Arith.Wf_nat]

F:51 [binder, in Coq.btauto.Algebra]

f:51 [binder, in Coq.NArith.BinNat]

f:51 [binder, in Coq.Reals.Rlimit]

f:51 [binder, in Coq.Logic.FinFun]

F:51 [binder, in Coq.rtauto.Rtauto]

f:510 [binder, in Coq.ssr.ssrbool]

f:511 [binder, in Coq.Reals.RiemannInt]

f:514 [binder, in Coq.Lists.List]

f:515 [binder, in Coq.FSets.FMapWeakList]

f:518 [binder, in Coq.micromega.Tauto]

f:52 [binder, in Coq.MSets.MSetProperties]

f:52 [binder, in Coq.Classes.RelationPairs]

f:52 [binder, in Coq.MSets.MSetList]

f:52 [binder, in Coq.Sets.Image]

f:52 [binder, in Coq.FSets.FSetProperties]

f:52 [binder, in Coq.rtauto.Rtauto]

f:520 [binder, in Coq.ssr.ssrbool]

f:525 [binder, in Coq.FSets.FMapList]

f:526 [binder, in Coq.Reals.RiemannInt]

f:527 [binder, in Coq.FSets.FMapList]

f:528 [binder, in Coq.ssr.ssrbool]

f:529 [binder, in Coq.FSets.FMapList]

f:53 [binder, in Coq.Reals.Ranalysis1]

f:53 [binder, in Coq.Reals.RiemannInt]

f:53 [binder, in Coq.Vectors.Fin]

f:53 [binder, in Coq.Reals.RiemannInt_SF]

f:53 [binder, in Coq.Floats.FloatAxioms]

f:53 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:530 [binder, in Coq.Init.Logic]

f:532 [binder, in Coq.Reals.RiemannInt]

f:535 [binder, in Coq.FSets.FMapList]

f:54 [binder, in Coq.micromega.RingMicromega]

f:54 [binder, in Coq.Logic.FunctionalExtensionality]

f:540 [binder, in Coq.micromega.Tauto]

f:541 [binder, in Coq.Reals.RiemannInt]

f:544 [binder, in Coq.Reals.RiemannInt]

f:545 [binder, in Coq.FSets.FMapFacts]

f:547 [binder, in Coq.Reals.RiemannInt]

f:547 [binder, in Coq.micromega.Tauto]

f:55 [binder, in Coq.Reals.Ranalysis1]

f:55 [binder, in Coq.Numbers.NaryFunctions]

f:55 [binder, in Coq.Logic.Hurkens]

f:55 [binder, in Coq.micromega.QMicromega]

f:55 [binder, in Coq.Reals.Rlimit]

F:55 [binder, in Coq.rtauto.Rtauto]

f:550 [binder, in Coq.micromega.Tauto]

f:552 [binder, in Coq.micromega.Tauto]

f:553 [binder, in Coq.PArith.BinPos]

f:553 [binder, in Coq.Reals.RiemannInt]

f:553 [binder, in Coq.Init.Logic]

f:555 [binder, in Coq.micromega.Tauto]

f:557 [binder, in Coq.Reals.RiemannInt]

f:56 [binder, in Coq.Init.Peano]

f:56 [binder, in Coq.Logic.ChoiceFacts]

f:56 [binder, in Coq.MSets.MSetList]

f:56 [binder, in Coq.Vectors.Fin]

f:56 [binder, in Coq.Sets.Image]

f:56 [binder, in Coq.Reals.RiemannInt_SF]

f:561 [binder, in Coq.FSets.FMapFacts]

f:563 [binder, in Coq.Init.Logic]

f:569 [binder, in Coq.Reals.RiemannInt]

f:57 [binder, in Coq.MSets.MSetInterface]

f:57 [binder, in Coq.NArith.BinNat]

f:57 [binder, in Coq.Reals.NewtonInt]

f:57 [binder, in Coq.micromega.ZMicromega]

f:572 [binder, in Coq.Lists.List]

f:574 [binder, in Coq.Init.Logic]

f:576 [binder, in Coq.Lists.List]

f:576 [binder, in Coq.Reals.RiemannInt]

f:58 [binder, in Coq.Reals.MVT]

f:58 [binder, in Coq.Logic.FunctionalExtensionality]

F:58 [binder, in Coq.rtauto.Rtauto]

f:580 [binder, in Coq.Lists.List]

f:583 [binder, in Coq.Init.Logic]

f:584 [binder, in Coq.Lists.List]

f:587 [binder, in Coq.Lists.List]

f:587 [binder, in Coq.FSets.FMapFacts]

f:589 [binder, in Coq.FSets.FMapFacts]

F:59 [binder, in Coq.Arith.Wf_nat]

f:59 [binder, in Coq.Logic.ChoiceFacts]

f:59 [binder, in Coq.Vectors.Fin]

f:59 [binder, in Coq.micromega.ZMicromega]

f:59 [binder, in Coq.Logic.FinFun]

f:590 [binder, in Coq.FSets.FMapFacts]

f:592 [binder, in Coq.FSets.FMapFacts]

f:592 [binder, in Coq.FSets.FMapWeakList]

f:593 [binder, in Coq.FSets.FMapFacts]

f:595 [binder, in Coq.FSets.FMapFacts]

f:596 [binder, in Coq.FSets.FMapFacts]

f:598 [binder, in Coq.FSets.FMapFacts]

f:6 [binder, in Coq.Wellfounded.Well_Ordering]

f:6 [binder, in Coq.Numbers.NatInt.NZDomain]

f:6 [binder, in Coq.Program.Combinators]

f:60 [binder, in Coq.MSets.MSetList]

f:60 [binder, in Coq.ssr.ssrfun]

f:60 [binder, in Coq.NArith.BinNat]

f:60 [binder, in Coq.Sets.Image]

f:606 [binder, in Coq.FSets.FMapWeakList]

f:61 [binder, in Coq.Reals.Ranalysis2]

f:611 [binder, in Coq.FSets.FMapWeakList]

f:613 [binder, in Coq.ssr.ssrbool]

f:613 [binder, in Coq.FSets.FMapList]

f:616 [binder, in Coq.micromega.Tauto]

f:617 [binder, in Coq.FSets.FMapWeakList]

f:619 [binder, in Coq.ssr.ssrbool]

f:62 [binder, in Coq.Init.Peano]

f:62 [binder, in Coq.Reals.RiemannInt]

f:62 [binder, in Coq.FSets.FMapInterface]

F:62 [binder, in Coq.Logic.Hurkens]

f:62 [binder, in Coq.Classes.EquivDec]

f:62 [binder, in Coq.NArith.Ndigits]

f:62 [binder, in Coq.Reals.Rlimit]

f:623 [binder, in Coq.FSets.FMapWeakList]

f:625 [binder, in Coq.micromega.Tauto]

f:627 [binder, in Coq.FSets.FMapList]

f:63 [binder, in Coq.Reals.Ranalysis1]

f:63 [binder, in Coq.MSets.MSetProperties]

F:63 [binder, in Coq.Arith.Wf_nat]

f:63 [binder, in Coq.NArith.Nnat]

f:63 [binder, in Coq.Reals.Rtopology]

f:63 [binder, in Coq.FSets.FSetProperties]

f:63 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:630 [binder, in Coq.FSets.FMapWeakList]

f:632 [binder, in Coq.FSets.FMapList]

f:633 [binder, in Coq.micromega.Tauto]

f:637 [binder, in Coq.FSets.FMapWeakList]

f:638 [binder, in Coq.FSets.FMapList]

f:64 [binder, in Coq.Reals.Rderiv]

f:64 [binder, in Coq.Numbers.NaryFunctions]

f:64 [binder, in Coq.Reals.RiemannInt_SF]

f:642 [binder, in Coq.micromega.Tauto]

f:643 [binder, in Coq.MSets.MSetAVL]

f:644 [binder, in Coq.FSets.FMapList]

f:646 [binder, in Coq.MSets.MSetAVL]

f:648 [binder, in Coq.MSets.MSetAVL]

f:648 [binder, in Coq.micromega.Tauto]

f:65 [binder, in Coq.ssr.ssrfun]

f:65 [binder, in Coq.Reals.NewtonInt]

f:65 [binder, in Coq.Reals.RList]

f:651 [binder, in Coq.MSets.MSetAVL]

f:651 [binder, in Coq.FSets.FMapList]

f:653 [binder, in Coq.MSets.MSetAVL]

f:654 [binder, in Coq.Init.Logic]

f:656 [binder, in Coq.MSets.MSetAVL]

f:658 [binder, in Coq.MSets.MSetAVL]

f:658 [binder, in Coq.FSets.FMapList]

f:66 [binder, in Coq.Reals.Ranalysis2]

f:66 [binder, in Coq.MSets.MSetEqProperties]

f:66 [binder, in Coq.Reals.MVT]

f:66 [binder, in Coq.FSets.FSetEqProperties]

f:66 [binder, in Coq.Reals.Ranalysis5]

f:66 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

f:661 [binder, in Coq.MSets.MSetAVL]

f:661 [binder, in Coq.Init.Logic]

f:664 [binder, in Coq.MSets.MSetAVL]

f:67 [binder, in Coq.Reals.RiemannInt_SF]

f:67 [binder, in Coq.micromega.Tauto]

f:673 [binder, in Coq.Init.Specif]

f:678 [binder, in Coq.MSets.MSetRBT]

F:68 [binder, in Coq.Logic.Hurkens]

f:68 [binder, in Coq.Reals.Rtopology]

f:68 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:680 [binder, in Coq.MSets.MSetRBT]

f:682 [binder, in Coq.FSets.FMapFacts]

f:69 [binder, in Coq.Logic.ChoiceFacts]

f:69 [binder, in Coq.Reals.Rlimit]

f:690 [binder, in Coq.MSets.MSetRBT]

f:691 [binder, in Coq.FSets.FMapFacts]

f:692 [binder, in Coq.MSets.MSetRBT]

f:694 [binder, in Coq.MSets.MSetRBT]

f:7 [binder, in Coq.Reals.Rderiv]

f:7 [binder, in Coq.Floats.PrimFloat]

f:7 [binder, in Coq.Floats.FloatOps]

f:7 [binder, in Coq.Classes.CRelationClasses]

f:7 [binder, in Coq.btauto.Reflect]

f:70 [binder, in Coq.MSets.MSetProperties]

f:70 [binder, in Coq.Logic.Hurkens]

f:70 [binder, in Coq.NArith.BinNat]

f:70 [binder, in Coq.Reals.RiemannInt_SF]

f:70 [binder, in Coq.FSets.FSetProperties]

f:701 [binder, in Coq.FSets.FMapFacts]

f:702 [binder, in Coq.Init.Specif]

f:707 [binder, in Coq.Lists.List]

f:71 [binder, in Coq.Reals.Ranalysis1]

f:71 [binder, in Coq.Numbers.NaryFunctions]

F:71 [binder, in Coq.Arith.Wf_nat]

f:71 [binder, in Coq.Reals.Rtopology]

f:715 [binder, in Coq.Init.Specif]

f:717 [binder, in Coq.Lists.List]

f:72 [binder, in Coq.PArith.BinPos]

f:72 [binder, in Coq.Numbers.Natural.Abstract.NBits]

f:72 [binder, in Coq.ssr.ssrfun]

f:72 [binder, in Coq.micromega.Tauto]

f:73 [binder, in Coq.Reals.Ranalysis1]

f:73 [binder, in Coq.Reals.Rseries]

f:73 [binder, in Coq.ssr.ssrfun]

f:73 [binder, in Coq.Reals.Rtopology]

f:730 [binder, in Coq.Init.Specif]

f:74 [binder, in Coq.Reals.RiemannInt]

f:74 [binder, in Coq.NArith.BinNat]

f:74 [binder, in Coq.Reals.Rlimit]

f:74 [binder, in Coq.Reals.Ratan]

F:74 [binder, in Coq.rtauto.Rtauto]

f:743 [binder, in Coq.Init.Specif]

F:75 [binder, in Coq.Arith.Wf_nat]

f:75 [binder, in Coq.ssr.ssrfun]

f:75 [binder, in Coq.Init.Datatypes]

f:76 [binder, in Coq.Reals.Rderiv]

f:76 [binder, in Coq.Logic.FinFun]

f:77 [binder, in Coq.Numbers.NaryFunctions]

f:77 [binder, in Coq.Reals.Rseries]

f:77 [binder, in Coq.FSets.FSetInterface]

f:77 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:78 [binder, in Coq.Reals.Ranalysis1]

f:78 [binder, in Coq.Reals.MVT]

f:78 [binder, in Coq.Logic.FunctionalExtensionality]

f:78 [binder, in Coq.micromega.QMicromega]

f:78 [binder, in Coq.Reals.Ranalysis5]

f:79 [binder, in Coq.Reals.Rsqrt_def]

f:79 [binder, in Coq.Reals.RiemannInt]

f:79 [binder, in Coq.micromega.QMicromega]

f:79 [binder, in Coq.Sorting.CPermutation]

f:79 [binder, in Coq.Logic.FinFun]

f:8 [binder, in Coq.Reals.Ranalysis4]

f:8 [binder, in Coq.Floats.PrimFloat]

f:8 [binder, in Coq.Floats.FloatOps]

f:8 [binder, in Coq.Logic.ClassicalUniqueChoice]

F:8 [binder, in Coq.micromega.DeclConstant]

f:8 [binder, in Coq.Numbers.Natural.Abstract.NStrongRec]

f:8 [binder, in Coq.Logic.FinFun]

f:81 [binder, in Coq.Reals.MVT]

f:81 [binder, in Coq.Logic.ChoiceFacts]

f:81 [binder, in Coq.Numbers.Natural.Abstract.NBits]

f:81 [binder, in Coq.MSets.MSetRBT]

f:81 [binder, in Coq.Init.Datatypes]

f:81 [binder, in Coq.Reals.RiemannInt_SF]

f:82 [binder, in Coq.MSets.MSetProperties]

f:82 [binder, in Coq.ssr.ssrfun]

f:82 [binder, in Coq.micromega.QMicromega]

f:82 [binder, in Coq.Sorting.CPermutation]

f:82 [binder, in Coq.FSets.FSetProperties]

f:82 [binder, in Coq.Logic.FinFun]

f:83 [binder, in Coq.PArith.BinPos]

f:83 [binder, in Coq.micromega.RingMicromega]

F:83 [binder, in Coq.Arith.Wf_nat]

f:83 [binder, in Coq.Reals.Rlimit]

f:83 [binder, in Coq.Reals.RiemannInt_SF]

f:839 [binder, in Coq.Init.Logic]

f:84 [binder, in Coq.Reals.MVT]

f:84 [binder, in Coq.Reals.RiemannInt]

f:84 [binder, in Coq.Reals.NewtonInt]

f:84 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:85 [binder, in Coq.Floats.SpecFloat]

f:85 [binder, in Coq.Reals.MVT]

f:85 [binder, in Coq.FSets.FMapFacts]

f:85 [binder, in Coq.FSets.FMapInterface]

f:853 [binder, in Coq.Lists.List]

f:86 [binder, in Coq.ssr.ssrfun]

f:86 [binder, in Coq.Reals.Rtopology]

f:86 [binder, in Coq.PArith.BinPosDef]

f:86 [binder, in Coq.Logic.FinFun]

f:869 [binder, in Coq.Init.Logic]

F:87 [binder, in Coq.Arith.Wf_nat]

f:87 [binder, in Coq.Classes.Morphisms]

f:87 [binder, in Coq.setoid_ring.Field_theory]

f:87 [binder, in Coq.MSets.MSetAVL]

f:87 [binder, in Coq.ssr.ssrfun]

f:88 [binder, in Coq.ZArith.BinIntDef]

f:88 [binder, in Coq.PArith.BinPos]

f:88 [binder, in Coq.FSets.FMapAVL]

f:88 [binder, in Coq.Numbers.Cyclic.Int31.Int31]

f:88 [binder, in Coq.Sorting.CPermutation]

f:88 [binder, in Coq.Reals.Rlimit]

f:882 [binder, in Coq.Init.Logic]

f:889 [binder, in Coq.Lists.List]

f:89 [binder, in Coq.micromega.RingMicromega]

f:89 [binder, in Coq.FSets.FMapFacts]

f:89 [binder, in Coq.Logic.FunctionalExtensionality]

f:89 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:897 [binder, in Coq.Init.Logic]

f:9 [binder, in Coq.Classes.RelationPairs]

f:9 [binder, in Coq.Logic.FunctionalExtensionality]

f:9 [binder, in Coq.Reals.RiemannInt]

f:9 [binder, in Coq.Relations.Relations]

f:9 [binder, in Coq.Arith.PeanoNat]

f:9 [binder, in Coq.Reals.Ratan]

f:90 [binder, in Coq.ssr.ssrfun]

f:90 [binder, in Coq.Reals.Rpower]

f:90 [binder, in Coq.Reals.NewtonInt]

f:91 [binder, in Coq.Logic.ChoiceFacts]

f:91 [binder, in Coq.FSets.FMapInterface]

f:91 [binder, in Coq.Classes.CMorphisms]

f:91 [binder, in Coq.Reals.Rtopology]

f:91 [binder, in Coq.Reals.PSeries_reg]

f:91 [binder, in Coq.Reals.RiemannInt_SF]

f:910 [binder, in Coq.Init.Logic]

f:92 [binder, in Coq.FSets.FMapFacts]

f:92 [binder, in Coq.Numbers.Integer.Abstract.ZBits]

f:92 [binder, in Coq.micromega.ZMicromega]

f:93 [binder, in Coq.Reals.Rsqrt_def]

f:93 [binder, in Coq.MSets.MSetAVL]

f:93 [binder, in Coq.Reals.Rtopology]

f:93 [binder, in Coq.FSets.FSetCompat]

f:935 [binder, in Coq.Init.Specif]

f:94 [binder, in Coq.Reals.Rderiv]

f:94 [binder, in Coq.Reals.MVT]

f:94 [binder, in Coq.Logic.FunctionalExtensionality]

f:94 [binder, in Coq.MSets.MSetRBT]

f:94 [binder, in Coq.Reals.RiemannInt_SF]

f:94 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:95 [binder, in Coq.micromega.RingMicromega]

f:96 [binder, in Coq.Reals.Ranalysis1]

f:96 [binder, in Coq.Numbers.NaryFunctions]

f:96 [binder, in Coq.FSets.FMapFacts]

f:96 [binder, in Coq.Reals.Rpower]

F:96 [binder, in Coq.rtauto.Bintree]

f:96 [binder, in Coq.Reals.NewtonInt]

f:96 [binder, in Coq.micromega.RMicromega]

f:964 [binder, in Coq.Init.Specif]

f:97 [binder, in Coq.MSets.MSetEqProperties]

f:97 [binder, in Coq.Reals.MVT]

f:97 [binder, in Coq.setoid_ring.Field_theory]

f:97 [binder, in Coq.FSets.FSetEqProperties]

f:97 [binder, in Coq.Reals.Rtopology]

f:97 [binder, in Coq.Reals.RList]

f:971 [binder, in Coq.Lists.List]

f:977 [binder, in Coq.Init.Specif]

f:98 [binder, in Coq.Reals.MVT]

f:98 [binder, in Coq.FSets.FMapInterface]

f:99 [binder, in Coq.Reals.Rtopology]

f:99 [binder, in Coq.Reals.Rlimit]

f:99 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

f:99 [binder, in Coq.FSets.FSetCompat]

f:992 [binder, in Coq.Init.Specif]

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

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

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

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

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

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

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

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

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

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

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

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

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