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

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

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

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

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

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

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

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

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

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

## G

g [definition, in Coq.Logic.Berardi]Gauss [lemma, in Coq.ZArith.Znumtheory]

gcd [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

gcd [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

gcd [definition, in Coq.Init.Nat]

Gcd [module, in Coq.Numbers.NatInt.NZGcd]

gcd [definition, in Coq.Numbers.Cyclic.Int63.Uint63]

gcd_greatest [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

gcd_divide_r [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

gcd_divide_l [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

gcd_divide [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

gcd_gt [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

gcd_spec [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]

gcd_rec [definition, in Coq.Numbers.Cyclic.Int63.Uint63]

Gcd.gcd [axiom, in Coq.Numbers.NatInt.NZGcd]

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

ge [definition, in Coq.Init.Peano]

gen [lemma, in Coq.Init.Logic]

genCuttingPlane [definition, in Coq.micromega.ZMicromega]

genCuttingPlaneNone [lemma, in Coq.micromega.ZMicromega]

GeneralizedSetoidFunctionalChoice [abbreviation, in Coq.Logic.ChoiceFacts]

GeneralizedSetoidFunctionalChoice_on [definition, in Coq.Logic.ChoiceFacts]

Generalized_induction_on_finite_sets [lemma, in Coq.Sets.Finite_sets_facts]

generalized_excluded_middle [definition, in Coq.Logic.ClassicalFacts]

Generic [section, in Coq.Logic.Classical_Pred_Type]

Generic [module, in Coq.Logic.Hurkens]

GenericAbs [module, in Coq.Numbers.Integer.Abstract.ZSgnAbs]

GenericAbs.abs [definition, in Coq.Numbers.Integer.Abstract.ZSgnAbs]

GenericAbs.abs_neq [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]

GenericAbs.abs_eq [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]

GenericInstances [section, in Coq.Classes.Morphisms]

GenericInstances [section, in Coq.Classes.CMorphisms]

GenericInstances.U [variable, in Coq.Classes.Morphisms]

GenericMinMax [module, in Coq.Structures.GenericMinMax]

GenericMinMax [library]

GenericMinMax.ge_not_lt [lemma, in Coq.Structures.GenericMinMax]

GenericMinMax.max [definition, in Coq.Structures.GenericMinMax]

GenericMinMax.max_r [lemma, in Coq.Structures.GenericMinMax]

GenericMinMax.max_l [lemma, in Coq.Structures.GenericMinMax]

GenericMinMax.min [definition, in Coq.Structures.GenericMinMax]

GenericMinMax.min_r [lemma, in Coq.Structures.GenericMinMax]

GenericMinMax.min_l [lemma, in Coq.Structures.GenericMinMax]

GenericSgn [module, in Coq.Numbers.Integer.Abstract.ZSgnAbs]

GenericSgn.sgn [definition, in Coq.Numbers.Integer.Abstract.ZSgnAbs]

GenericSgn.sgn_neg [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]

GenericSgn.sgn_pos [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]

GenericSgn.sgn_null [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]

Generic.I [definition, in Coq.Logic.Hurkens]

Generic.induct [definition, in Coq.Logic.Hurkens]

Generic.le [definition, in Coq.Logic.Hurkens]

Generic.lemma1 [lemma, in Coq.Logic.Hurkens]

Generic.lemma2 [lemma, in Coq.Logic.Hurkens]

Generic.le' [definition, in Coq.Logic.Hurkens]

Generic.Omega [lemma, in Coq.Logic.Hurkens]

Generic.paradox [lemma, in Coq.Logic.Hurkens]

Generic.Paradox [section, in Coq.Logic.Hurkens]

Generic.Paradox.appU0 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.appU1 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.app0 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.app1 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.betaU1 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.beta1 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.El0 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.El1 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.F [variable, in Coq.Logic.Hurkens]

Generic.Paradox.ForallU0 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.ForallU1 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.Forall0 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.Forall1 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.lamU0 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.lamU1 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.lam0 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.lam1 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.u0 [variable, in Coq.Logic.Hurkens]

Generic.Paradox.U1 [variable, in Coq.Logic.Hurkens]

_ ·₀ [ _ ] [notation, in Coq.Logic.Hurkens]

_ ·₀ _ [notation, in Coq.Logic.Hurkens]

_ ⟶₀ _ [notation, in Coq.Logic.Hurkens]

_ ·₁ [ _ ] [notation, in Coq.Logic.Hurkens]

_ ·₁ _ [notation, in Coq.Logic.Hurkens]

_ ⟶₁ _ [notation, in Coq.Logic.Hurkens]

λ₀ _ , _ [notation, in Coq.Logic.Hurkens]

λ₀¹ _ , _ [notation, in Coq.Logic.Hurkens]

λ₁ _ , _ [notation, in Coq.Logic.Hurkens]

λ₂ _ , _ [notation, in Coq.Logic.Hurkens]

∀₀ _ : _ , _ [notation, in Coq.Logic.Hurkens]

∀₀¹ _ : _ , _ [notation, in Coq.Logic.Hurkens]

∀₁ _ : _ , _ [notation, in Coq.Logic.Hurkens]

∀₂ _ , _ [notation, in Coq.Logic.Hurkens]

Generic.sb [definition, in Coq.Logic.Hurkens]

Generic.U [variable, in Coq.Logic.Classical_Pred_Type]

Generic.U [definition, in Coq.Logic.Hurkens]

Generic.U0 [abbreviation, in Coq.Logic.Hurkens]

Generic.V [definition, in Coq.Logic.Hurkens]

Generic.WF [definition, in Coq.Logic.Hurkens]

gen_phiZ_morph [instance, in Coq.setoid_ring.Ncring_initial]

gen_phiZ_ext [lemma, in Coq.setoid_ring.Ncring_initial]

gen_phiZ_mul [lemma, in Coq.setoid_ring.Ncring_initial]

gen_phiZ_opp [lemma, in Coq.setoid_ring.Ncring_initial]

gen_phiZ_add [lemma, in Coq.setoid_ring.Ncring_initial]

gen_phiZ1_add_pos_neg [lemma, in Coq.setoid_ring.Ncring_initial]

gen_Zeqb_ok [lemma, in Coq.setoid_ring.Ncring_initial]

gen_phiZ [definition, in Coq.setoid_ring.Ncring_initial]

gen_phiZ1 [definition, in Coq.setoid_ring.Ncring_initial]

gen_phiPOS [definition, in Coq.setoid_ring.Ncring_initial]

gen_phiPOS1 [definition, in Coq.setoid_ring.Ncring_initial]

gen_setoid_fun_choice_imp_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]

gen_phiZ_complete [lemma, in Coq.setoid_ring.Field_theory]

gen_phiZ_inj [lemma, in Coq.setoid_ring.Field_theory]

gen_phiPOS_discr_sgn [lemma, in Coq.setoid_ring.Field_theory]

gen_phiN_complete [lemma, in Coq.setoid_ring.Field_theory]

gen_phiN_inj [lemma, in Coq.setoid_ring.Field_theory]

gen_phiPOS_inj [lemma, in Coq.setoid_ring.Field_theory]

GEN_DIV.nphi [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.zphi [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.morph [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.ARth [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.Reqe [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.Rsth [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.phi [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.ceqb [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.copp [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.csub [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.cmul [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.cadd [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.cI [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.cO [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.C [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.req [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.ropp [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.rsub [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.rmul [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.radd [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.rI [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.rO [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV.R [variable, in Coq.setoid_ring.InitialRing]

GEN_DIV [section, in Coq.setoid_ring.InitialRing]

gen_phiNword_morph [lemma, in Coq.setoid_ring.InitialRing]

gen_phiNword_ok [lemma, in Coq.setoid_ring.InitialRing]

gen_phiNword_Nwcons [lemma, in Coq.setoid_ring.InitialRing]

gen_phiNword_cons [lemma, in Coq.setoid_ring.InitialRing]

gen_phiNword0_ok [lemma, in Coq.setoid_ring.InitialRing]

gen_phiNword [definition, in Coq.setoid_ring.InitialRing]

gen_phiN_morph [lemma, in Coq.setoid_ring.InitialRing]

gen_phiN_sub [lemma, in Coq.setoid_ring.InitialRing]

gen_phiN_mult [lemma, in Coq.setoid_ring.InitialRing]

gen_phiN_add [lemma, in Coq.setoid_ring.InitialRing]

gen_phiN [definition, in Coq.setoid_ring.InitialRing]

gen_phiN1 [definition, in Coq.setoid_ring.InitialRing]

gen_phiZ_morph [lemma, in Coq.setoid_ring.InitialRing]

gen_phiZ_ext [lemma, in Coq.setoid_ring.InitialRing]

gen_phiZ_mul [lemma, in Coq.setoid_ring.InitialRing]

gen_phiZ_add [lemma, in Coq.setoid_ring.InitialRing]

gen_phiZ1_pos_sub [lemma, in Coq.setoid_ring.InitialRing]

gen_Zeqb_ok [lemma, in Coq.setoid_ring.InitialRing]

gen_phiZ [definition, in Coq.setoid_ring.InitialRing]

gen_phiZ1 [definition, in Coq.setoid_ring.InitialRing]

gen_phiPOS [definition, in Coq.setoid_ring.InitialRing]

gen_phiPOS1 [definition, in Coq.setoid_ring.InitialRing]

gen_st [definition, in Coq.Setoids.Setoid]

gen_order_phi_Z [definition, in Coq.micromega.ZCoeff]

GeoCvZero [lemma, in Coq.Reals.Abstract.ConstructivePower]

GeoFiniteSum [lemma, in Coq.Reals.Abstract.ConstructivePower]

GeoHalfBelowTwo [lemma, in Coq.Reals.Abstract.ConstructivePower]

GeoHalfTwo [lemma, in Coq.Reals.Abstract.ConstructivePower]

get [definition, in Coq.Strings.String]

get [axiom, in Coq.Array.PArray]

get [definition, in Coq.rtauto.Bintree]

get_signZ [definition, in Coq.setoid_ring.Ncring_initial]

get_PEopp [definition, in Coq.setoid_ring.Ring_polynom]

get_sign [definition, in Coq.Floats.PrimFloat]

get_correct [lemma, in Coq.Strings.String]

get_PEopp [definition, in Coq.micromega.EnvRing]

get_signZ_th [lemma, in Coq.setoid_ring.InitialRing]

get_signZ [definition, in Coq.setoid_ring.InitialRing]

get_not_default_lt [lemma, in Coq.Array.PArray]

get_set_same_default [lemma, in Coq.Array.PArray]

get_copy [axiom, in Coq.Array.PArray]

get_make [axiom, in Coq.Array.PArray]

get_set_other [axiom, in Coq.Array.PArray]

get_set_same [axiom, in Coq.Array.PArray]

get_out_of_bounds [axiom, in Coq.Array.PArray]

get_map [lemma, in Coq.rtauto.Bintree]

get_In [lemma, in Coq.rtauto.Bintree]

get_push_Full [lemma, in Coq.rtauto.Bintree]

get_Full_Eq [lemma, in Coq.rtauto.Bintree]

get_Full_Gt [lemma, in Coq.rtauto.Bintree]

get_empty [lemma, in Coq.rtauto.Bintree]

get_sign_None_th [lemma, in Coq.setoid_ring.Ring_theory]

get_sign_None [definition, in Coq.setoid_ring.Ring_theory]

get_digit [definition, in Coq.Numbers.Cyclic.Int63.Uint63]

ge_bool_cases [lemma, in Coq.micromega.RingMicromega]

ge_bool [definition, in Coq.micromega.RingMicromega]

ge_dec [lemma, in Coq.Arith.Compare_dec]

GFormula [inductive, in Coq.micromega.Tauto]

gf_id:36 [binder, in Coq.Logic.Adjointification]

gf_id:15 [binder, in Coq.Logic.Adjointification]

Glb [inductive, in Coq.Sets.Cpo]

glb [definition, in Coq.Reals.SeqProp]

glb_dec_Q [lemma, in Coq.Reals.Abstract.ConstructiveLUB]

Glb_definition [constructor, in Coq.Sets.Cpo]

gl:64 [binder, in Coq.rtauto.Rtauto]

gl:75 [binder, in Coq.rtauto.Rtauto]

gl:76 [binder, in Coq.rtauto.Rtauto]

gmax [definition, in Coq.Structures.GenericMinMax]

gmin [definition, in Coq.Structures.GenericMinMax]

goal:117 [binder, in Coq.ssr.ssrbool]

goal:4 [binder, in Coq.micromega.Refl]

GodelDummett [definition, in Coq.Logic.ClassicalFacts]

Godel_Dummett_weak_excluded_middle [lemma, in Coq.Logic.ClassicalFacts]

Godel_Dummett_iff_right_distr_implication_over_disjunction [lemma, in Coq.Logic.ClassicalFacts]

GP_finite [lemma, in Coq.Reals.Rfunctions]

GP_infinite [lemma, in Coq.Reals.Rseries]

growing_prop [lemma, in Coq.Reals.Rseries]

growing_ineq [lemma, in Coq.Reals.Abstract.ConstructiveLimits]

growing_ineq [lemma, in Coq.Reals.SeqProp]

growing_cv [lemma, in Coq.Reals.SeqProp]

gt [definition, in Coq.Init.Peano]

GT [record, in Coq.micromega.DeclConstant]

GT [constructor, in Coq.Structures.OrderedType]

Gt [constructor, in Coq.Init.Datatypes]

Gt [library]

gtof [definition, in Coq.Arith.Wf_nat]

gt_le_trans_stt [definition, in Coq.Arith.Arith_prebase]

gt_trans_S_stt [definition, in Coq.Arith.Arith_prebase]

gt_le_S_stt [definition, in Coq.Arith.Arith_prebase]

gt_S_le_stt [definition, in Coq.Arith.Arith_prebase]

gt_not_le_stt [definition, in Coq.Arith.Arith_prebase]

gt_asym_stt [definition, in Coq.Arith.Arith_prebase]

gt_irrefl_stt [definition, in Coq.Arith.Arith_prebase]

gt_pred_stt [definition, in Coq.Arith.Arith_prebase]

gt_S_n_stt [definition, in Coq.Arith.Arith_prebase]

gt_n_S_stt [definition, in Coq.Arith.Arith_prebase]

gt_Sn_n_stt [definition, in Coq.Arith.Arith_prebase]

gt_Sn_O_stt [definition, in Coq.Arith.Arith_prebase]

gt_dec [lemma, in Coq.Arith.Compare_dec]

gt_eq_gt_dec [definition, in Coq.Arith.Compare_dec]

gt_wf_ind [lemma, in Coq.Arith.Wf_nat]

gt_wf_rec [lemma, in Coq.Arith.Wf_nat]

gt_wf_rect [lemma, in Coq.Arith.Wf_nat]

gt_tree0:537 [binder, in Coq.MSets.MSetAVL]

gt_tree0:516 [binder, in Coq.MSets.MSetAVL]

gt_tree0:505 [binder, in Coq.MSets.MSetAVL]

Gt_Psucc [lemma, in Coq.rtauto.Bintree]

gt_tree0:342 [binder, in Coq.MSets.MSetRBT]

gt_tree0:331 [binder, in Coq.MSets.MSetRBT]

gt_tree0:304 [binder, in Coq.MSets.MSetRBT]

gt_tree0:293 [binder, in Coq.MSets.MSetRBT]

gt_tree0:282 [binder, in Coq.MSets.MSetRBT]

GT_APP2 [instance, in Coq.micromega.DeclConstant]

GT_APP1 [instance, in Coq.micromega.DeclConstant]

GT_O [instance, in Coq.micromega.DeclConstant]

gt_O_eq [abbreviation, in Coq.Arith.Gt]

gt_0_eq [abbreviation, in Coq.Arith.Gt]

gt_0_eq_stt [definition, in Coq.Arith.Gt]

gt_trans_S [abbreviation, in Coq.Arith.Gt]

gt_trans [abbreviation, in Coq.Arith.Gt]

gt_trans_stt [definition, in Coq.Arith.Gt]

gt_le_trans [abbreviation, in Coq.Arith.Gt]

gt_le_S [abbreviation, in Coq.Arith.Gt]

gt_S_le [abbreviation, in Coq.Arith.Gt]

gt_not_le [abbreviation, in Coq.Arith.Gt]

gt_asym [abbreviation, in Coq.Arith.Gt]

gt_irrefl [abbreviation, in Coq.Arith.Gt]

gt_pred [abbreviation, in Coq.Arith.Gt]

gt_S [abbreviation, in Coq.Arith.Gt]

gt_S_stt [definition, in Coq.Arith.Gt]

gt_S_n [abbreviation, in Coq.Arith.Gt]

gt_n_S [abbreviation, in Coq.Arith.Gt]

gt_Sn_n [abbreviation, in Coq.Arith.Gt]

gt_Sn_O [abbreviation, in Coq.Arith.Gt]

GuardedFunctionalChoice [abbreviation, in Coq.Logic.ChoiceFacts]

GuardedFunctionalChoice_on [definition, in Coq.Logic.ChoiceFacts]

GuardedFunctionalRelReification [abbreviation, in Coq.Logic.ChoiceFacts]

GuardedFunctionalRelReification_on [definition, in Coq.Logic.ChoiceFacts]

GuardedRelationalChoice [abbreviation, in Coq.Logic.ChoiceFacts]

GuardedRelationalChoice_on [definition, in Coq.Logic.ChoiceFacts]

guarded_iff_omniscient_fun_choice [lemma, in Coq.Logic.ChoiceFacts]

guarded_fun_choice_imp_fun_choice [lemma, in Coq.Logic.ChoiceFacts]

guarded_fun_choice_imp_indep_of_general_premises [lemma, in Coq.Logic.ChoiceFacts]

guarded_iff_omniscient_rel_choice [lemma, in Coq.Logic.ChoiceFacts]

guarded_rel_choice_imp_rel_choice [lemma, in Coq.Logic.ChoiceFacts]

guarded_rel_choice [lemma, in Coq.Logic.Diaconescu]

guard:112 [binder, in Coq.Numbers.Cyclic.Int31.Int31]

guard:197 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

G_aux [lemma, in Coq.Sets.Finite_sets_facts]

g_wf:419 [binder, in Coq.Reals.Ranalysis5]

g_wf:402 [binder, in Coq.Reals.Ranalysis5]

g_wf:350 [binder, in Coq.Reals.Ranalysis5]

g_wf:332 [binder, in Coq.Reals.Ranalysis5]

g_adjoint [definition, in Coq.Logic.Adjointification]

g':157 [binder, in Coq.Reals.PSeries_reg]

g':320 [binder, in Coq.ssr.ssrfun]

g':97 [binder, in Coq.ssr.ssrfun]

g1:149 [binder, in Coq.Reals.PSeries_reg]

g1:173 [binder, in Coq.Reals.MVT]

g1:208 [binder, in Coq.micromega.ZMicromega]

g1:27 [binder, in Coq.Logic.ExtensionalityFacts]

g2:150 [binder, in Coq.Reals.PSeries_reg]

g2:174 [binder, in Coq.Reals.MVT]

g2:210 [binder, in Coq.micromega.ZMicromega]

g2:28 [binder, in Coq.Logic.ExtensionalityFacts]

g:10 [binder, in Coq.Logic.FunctionalExtensionality]

g:101 [binder, in Coq.MSets.MSetEqProperties]

g:101 [binder, in Coq.FSets.FSetEqProperties]

g:103 [binder, in Coq.ssr.ssrfun]

g:108 [binder, in Coq.Logic.FunctionalExtensionality]

g:108 [binder, in Coq.Logic.ClassicalFacts]

g:11 [binder, in Coq.Numbers.Natural.Abstract.NLcm]

g:111 [binder, in Coq.Reals.Rlimit]

g:115 [binder, in Coq.Logic.ClassicalFacts]

g:115 [binder, in Coq.PArith.BinPosDef]

g:116 [binder, in Coq.Reals.Rderiv]

g:117 [binder, in Coq.FSets.FSetDecide]

g:117 [binder, in Coq.MSets.MSetDecide]

g:12 [binder, in Coq.Program.Combinators]

g:122 [binder, in Coq.Reals.Rpower]

g:123 [binder, in Coq.FSets.FSetDecide]

g:123 [binder, in Coq.MSets.MSetDecide]

g:127 [binder, in Coq.MSets.MSetEqProperties]

g:127 [binder, in Coq.FSets.FSetEqProperties]

g:128 [binder, in Coq.Reals.Rpower]

g:13 [binder, in Coq.Logic.Adjointification]

g:132 [binder, in Coq.Vectors.VectorSpec]

g:132 [binder, in Coq.Reals.Ranalysis1]

g:133 [binder, in Coq.MSets.MSetEqProperties]

g:133 [binder, in Coq.FSets.FSetEqProperties]

G:134 [binder, in Coq.Structures.OrderedTypeEx]

g:139 [binder, in Coq.Vectors.VectorSpec]

g:14 [binder, in Coq.Logic.FinFun]

g:143 [binder, in Coq.Reals.PSeries_reg]

g:146 [binder, in Coq.Reals.Rderiv]

g:146 [binder, in Coq.Vectors.VectorSpec]

g:147 [binder, in Coq.Reals.MVT]

g:149 [binder, in Coq.Logic.ClassicalFacts]

g:149 [binder, in Coq.Logic.FinFun]

g:156 [binder, in Coq.Reals.PSeries_reg]

g:156 [binder, in Coq.Logic.ClassicalFacts]

g:16 [binder, in Coq.Logic.FunctionalExtensionality]

g:172 [binder, in Coq.ZArith.Znumtheory]

g:176 [binder, in Coq.Init.Logic]

g:177 [binder, in Coq.Reals.RiemannInt_SF]

g:178 [binder, in Coq.PArith.BinPos]

g:179 [binder, in Coq.MSets.MSetRBT]

g:179 [binder, in Coq.Reals.Ranalysis5]

g:18 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

g:184 [binder, in Coq.MSets.MSetRBT]

g:188 [binder, in Coq.Reals.RiemannInt]

g:189 [binder, in Coq.Reals.RiemannInt_SF]

g:19 [binder, in Coq.Program.Wf]

g:19 [binder, in Coq.Reals.Ranalysis5]

g:190 [binder, in Coq.Reals.Ranalysis1]

g:193 [binder, in Coq.MSets.MSetRBT]

g:193 [binder, in Coq.Logic.ClassicalFacts]

g:195 [binder, in Coq.Reals.Ranalysis1]

g:197 [binder, in Coq.Init.Specif]

g:197 [binder, in Coq.MSets.MSetRBT]

g:199 [binder, in Coq.Logic.ChoiceFacts]

g:199 [binder, in Coq.Logic.ClassicalFacts]

g:2 [binder, in Coq.Reals.MVT]

g:2 [binder, in Coq.Reals.Ranalysis5]

g:202 [binder, in Coq.MSets.MSetRBT]

g:205 [binder, in Coq.Reals.RiemannInt_SF]

g:208 [binder, in Coq.Vectors.VectorDef]

g:21 [binder, in Coq.Numbers.NaryFunctions]

g:21 [binder, in Coq.Logic.ExtensionalityFacts]

g:211 [binder, in Coq.Reals.RiemannInt_SF]

g:218 [binder, in Coq.MSets.MSetRBT]

g:22 [binder, in Coq.Logic.FunctionalExtensionality]

g:221 [binder, in Coq.Reals.Rtopology]

g:222 [binder, in Coq.MSets.MSetRBT]

g:227 [binder, in Coq.Sorting.Permutation]

g:227 [binder, in Coq.MSets.MSetRBT]

g:227 [binder, in Coq.Reals.RiemannInt_SF]

g:231 [binder, in Coq.Reals.Rtopology]

g:233 [binder, in Coq.Reals.Rtopology]

g:234 [binder, in Coq.Reals.RiemannInt_SF]

g:235 [binder, in Coq.Reals.RiemannInt]

g:236 [binder, in Coq.Vectors.VectorDef]

g:242 [binder, in Coq.micromega.ZMicromega]

g:243 [binder, in Coq.Reals.Ranalysis5]

g:245 [binder, in Coq.Reals.RiemannInt_SF]

g:246 [binder, in Coq.micromega.ZMicromega]

g:249 [binder, in Coq.micromega.ZMicromega]

g:250 [binder, in Coq.Init.Logic]

g:253 [binder, in Coq.Reals.RiemannInt_SF]

g:255 [binder, in Coq.micromega.ZMicromega]

g:256 [binder, in Coq.Reals.RiemannInt]

g:256 [binder, in Coq.Reals.Ranalysis5]

g:262 [binder, in Coq.Reals.RiemannInt_SF]

g:266 [binder, in Coq.NArith.BinNat]

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

g:28 [binder, in Coq.Classes.CMorphisms]

g:280 [binder, in Coq.ssr.ssrfun]

g:282 [binder, in Coq.ssr.ssrfun]

g:285 [binder, in Coq.ssr.ssrfun]

g:287 [binder, in Coq.ssr.ssrfun]

g:288 [binder, in Coq.ssr.ssrfun]

g:289 [binder, in Coq.ssr.ssrfun]

G:29 [binder, in Coq.rtauto.Rtauto]

g:290 [binder, in Coq.Reals.RiemannInt_SF]

g:292 [binder, in Coq.ssr.ssrfun]

g:295 [binder, in Coq.Reals.RiemannInt_SF]

g:299 [binder, in Coq.Reals.RiemannInt]

g:30 [binder, in Coq.Classes.CEquivalence]

g:30 [binder, in Coq.micromega.Refl]

G:30 [binder, in Coq.Sorting.Heap]

g:30 [binder, in Coq.Classes.Equivalence]

g:300 [binder, in Coq.Reals.Ranalysis5]

g:301 [binder, in Coq.Reals.RiemannInt_SF]

g:307 [binder, in Coq.Reals.RiemannInt_SF]

g:309 [binder, in Coq.Reals.Ranalysis5]

g:31 [binder, in Coq.Reals.NewtonInt]

G:316 [binder, in Coq.Reals.Rtopology]

g:316 [binder, in Coq.Reals.Ranalysis5]

g:317 [binder, in Coq.Init.Logic]

g:32 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]

g:323 [binder, in Coq.Reals.Ranalysis5]

g:327 [binder, in Coq.ssr.ssrfun]

g:327 [binder, in Coq.Reals.Rtopology]

g:328 [binder, in Coq.FSets.FMapPositive]

g:335 [binder, in Coq.FSets.FMapPositive]

g:337 [binder, in Coq.ssr.ssrfun]

g:341 [binder, in Coq.Reals.Ranalysis5]

g:346 [binder, in Coq.FSets.FMapFacts]

g:35 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]

g:357 [binder, in Coq.Reals.Ranalysis5]

g:365 [binder, in Coq.Reals.Ranalysis5]

g:367 [binder, in Coq.Logic.ChoiceFacts]

g:370 [binder, in Coq.Logic.ChoiceFacts]

g:374 [binder, in Coq.Reals.Ranalysis5]

g:378 [binder, in Coq.Reals.RiemannInt]

g:38 [binder, in Coq.Classes.Morphisms]

g:38 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]

g:383 [binder, in Coq.Reals.Ranalysis5]

g:39 [binder, in Coq.Logic.ExtensionalityFacts]

g:39 [binder, in Coq.Numbers.Natural.Abstract.NGcd]

g:392 [binder, in Coq.Reals.Ranalysis5]

g:4 [binder, in Coq.Reals.Ranalysis4]

g:4 [binder, in Coq.Logic.ExtensionalityFacts]

g:4 [binder, in Coq.Logic.FunctionalExtensionality]

g:4 [binder, in Coq.Reals.NewtonInt]

g:4 [binder, in Coq.Program.Basics]

g:405 [binder, in Coq.MSets.MSetRBT]

g:409 [binder, in Coq.Reals.Ranalysis5]

g:417 [binder, in Coq.Reals.RiemannInt]

g:42 [binder, in Coq.Classes.CMorphisms]

g:426 [binder, in Coq.Lists.List]

g:432 [binder, in Coq.Lists.List]

g:436 [binder, in Coq.Reals.Ranalysis5]

g:438 [binder, in Coq.Lists.List]

g:44 [binder, in Coq.Init.Wf]

g:44 [binder, in Coq.Reals.Ratan]

g:444 [binder, in Coq.Lists.List]

g:450 [binder, in Coq.Lists.List]

g:456 [binder, in Coq.Lists.List]

g:46 [binder, in Coq.Classes.SetoidDec]

g:47 [binder, in Coq.Classes.Morphisms]

g:47 [binder, in Coq.Classes.CMorphisms]

g:47 [binder, in Coq.Reals.NewtonInt]

g:49 [binder, in Coq.Logic.FunctionalExtensionality]

G:49 [binder, in Coq.Reals.NewtonInt]

g:49 [binder, in Coq.ZArith.Znumtheory]

g:5 [binder, in Coq.Numbers.Natural.Abstract.NLcm0]

G:53 [binder, in Coq.rtauto.Rtauto]

g:536 [binder, in Coq.Reals.RiemannInt]

g:554 [binder, in Coq.PArith.BinPos]

g:555 [binder, in Coq.Lists.List]

g:56 [binder, in Coq.Reals.Ranalysis1]

g:56 [binder, in Coq.rtauto.Rtauto]

g:575 [binder, in Coq.Lists.List]

g:579 [binder, in Coq.Lists.List]

g:58 [binder, in Coq.Reals.NewtonInt]

g:583 [binder, in Coq.Lists.List]

g:587 [binder, in Coq.Lists.List]

g:59 [binder, in Coq.Logic.FunctionalExtensionality]

g:590 [binder, in Coq.Lists.List]

g:6 [binder, in Coq.Logic.ExtensionalFunctionRepresentative]

g:60 [binder, in Coq.Vectors.Fin]

g:60 [binder, in Coq.rtauto.Rtauto]

g:62 [binder, in Coq.Reals.Ranalysis2]

g:63 [binder, in Coq.Logic.FunctionalExtensionality]

g:63 [binder, in Coq.Classes.EquivDec]

g:63 [binder, in Coq.NArith.Ndigits]

g:63 [binder, in Coq.Reals.Rlimit]

g:63 [binder, in Coq.Logic.FinFun]

g:636 [binder, in Coq.ssr.ssrbool]

g:637 [binder, in Coq.ssr.ssrbool]

g:642 [binder, in Coq.ssr.ssrbool]

g:643 [binder, in Coq.ssr.ssrbool]

g:65 [binder, in Coq.Reals.Rderiv]

g:66 [binder, in Coq.Classes.Morphisms]

g:66 [binder, in Coq.Logic.FunctionalExtensionality]

g:67 [binder, in Coq.MSets.MSetEqProperties]

g:67 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]

g:67 [binder, in Coq.FSets.FSetEqProperties]

g:67 [binder, in Coq.Reals.Ranalysis5]

g:67 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]

g:681 [binder, in Coq.MSets.MSetRBT]

g:69 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]

g:70 [binder, in Coq.ssr.ssrfun]

g:717 [binder, in Coq.ssr.ssrbool]

g:723 [binder, in Coq.ssr.ssrbool]

g:73 [binder, in Coq.Numbers.Natural.Abstract.NBits]

g:75 [binder, in Coq.Reals.RiemannInt]

g:75 [binder, in Coq.Reals.Rlimit]

g:77 [binder, in Coq.Reals.Rderiv]

g:77 [binder, in Coq.Reals.Ranalysis5]

g:78 [binder, in Coq.ssr.ssrfun]

g:79 [binder, in Coq.Logic.FunctionalExtensionality]

g:80 [binder, in Coq.ssr.ssrfun]

g:82 [binder, in Coq.MSets.MSetRBT]

g:83 [binder, in Coq.MSets.MSetProperties]

g:83 [binder, in Coq.FSets.FSetProperties]

g:84 [binder, in Coq.Program.Wf]

g:84 [binder, in Coq.Logic.FunctionalExtensionality]

g:86 [binder, in Coq.Logic.FunctionalExtensionality]

g:87 [binder, in Coq.ssr.ssrfun]

g:87 [binder, in Coq.PArith.BinPosDef]

g:89 [binder, in Coq.ssr.ssrfun]

g:89 [binder, in Coq.Reals.Rlimit]

g:9 [binder, in Coq.Reals.Ranalysis4]

g:9 [binder, in Coq.Reals.NewtonInt]

g:91 [binder, in Coq.Reals.Rpower]

g:92 [binder, in Coq.ssr.ssrfun]

G:93 [binder, in Coq.Structures.OrderedTypeEx]

g:93 [binder, in Coq.Numbers.Integer.Abstract.ZBits]

g:95 [binder, in Coq.Logic.FunctionalExtensionality]

g:96 [binder, in Coq.ssr.ssrfun]

g:981 [binder, in Coq.Lists.List]

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

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

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

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

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

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

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

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

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

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