Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (68863 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (985 entries)
Binder Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (44709 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (761 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1497 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (570 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11380 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (976 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (603 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (298 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (460 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (476 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (811 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1157 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4018 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (162 entries)

B

B [definition, in Coq.Wellfounded.Well_Ordering]
BackportEq [module, in Coq.Structures.Equalities]
BackportEq.eq_trans [definition, in Coq.Structures.Equalities]
BackportEq.eq_sym [definition, in Coq.Structures.Equalities]
BackportEq.eq_refl [definition, in Coq.Structures.Equalities]
Backport_OT.compare [definition, in Coq.Structures.OrdersAlt]
Backport_OT.lt_trans [lemma, in Coq.Structures.OrdersAlt]
Backport_OT.lt_not_eq [lemma, in Coq.Structures.OrdersAlt]
Backport_OT.lt [definition, in Coq.Structures.OrdersAlt]
Backport_OT [module, in Coq.Structures.OrdersAlt]
Backport_DT [module, in Coq.Structures.Equalities]
Backport_ET [module, in Coq.Structures.Equalities]
Backport_Sets.E [module, in Coq.FSets.FSetCompat]
Backport_Sets.compare [definition, in Coq.FSets.FSetCompat]
Backport_Sets.lt_not_eq [lemma, in Coq.FSets.FSetCompat]
Backport_Sets.lt_trans [definition, in Coq.FSets.FSetCompat]
Backport_Sets.choose_3 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.elements_3 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.max_elt_3 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.max_elt_2 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.max_elt_1 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.min_elt_3 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.min_elt_2 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.min_elt_1 [definition, in Coq.FSets.FSetCompat]
Backport_Sets.max_elt [definition, in Coq.FSets.FSetCompat]
Backport_Sets.min_elt [definition, in Coq.FSets.FSetCompat]
Backport_Sets.lt [definition, in Coq.FSets.FSetCompat]
Backport_Sets [module, in Coq.FSets.FSetCompat]
Backport_WSets.elements_3w [definition, in Coq.FSets.FSetCompat]
Backport_WSets.elements_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.elements_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.choose_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.choose_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.partition_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.partition_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.exists_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.exists_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.for_all_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.for_all_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.filter_3 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.filter_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.filter_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.cardinal_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.fold_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.singleton_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.singleton_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.diff_3 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.diff_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.diff_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.inter_3 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.inter_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.inter_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.union_3 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.union_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.union_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.remove_3 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.remove_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.remove_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.add_3 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.add_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.add_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.is_empty_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.is_empty_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.empty_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.subset_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.subset_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.equal_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.equal_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.mem_2 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.mem_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.eq_trans [definition, in Coq.FSets.FSetCompat]
Backport_WSets.eq_sym [definition, in Coq.FSets.FSetCompat]
Backport_WSets.eq_refl [definition, in Coq.FSets.FSetCompat]
Backport_WSets.In_1 [definition, in Coq.FSets.FSetCompat]
Backport_WSets.MF [module, in Coq.FSets.FSetCompat]
Backport_WSets.choose [definition, in Coq.FSets.FSetCompat]
Backport_WSets.elements [definition, in Coq.FSets.FSetCompat]
Backport_WSets.cardinal [definition, in Coq.FSets.FSetCompat]
Backport_WSets.partition [definition, in Coq.FSets.FSetCompat]
Backport_WSets.filter [definition, in Coq.FSets.FSetCompat]
Backport_WSets.exists_ [definition, in Coq.FSets.FSetCompat]
Backport_WSets.for_all [definition, in Coq.FSets.FSetCompat]
Backport_WSets.fold [definition, in Coq.FSets.FSetCompat]
Backport_WSets.subset [definition, in Coq.FSets.FSetCompat]
Backport_WSets.equal [definition, in Coq.FSets.FSetCompat]
Backport_WSets.eq_dec [definition, in Coq.FSets.FSetCompat]
Backport_WSets.eq [definition, in Coq.FSets.FSetCompat]
Backport_WSets.diff [definition, in Coq.FSets.FSetCompat]
Backport_WSets.inter [definition, in Coq.FSets.FSetCompat]
Backport_WSets.union [definition, in Coq.FSets.FSetCompat]
Backport_WSets.remove [definition, in Coq.FSets.FSetCompat]
Backport_WSets.singleton [definition, in Coq.FSets.FSetCompat]
Backport_WSets.add [definition, in Coq.FSets.FSetCompat]
Backport_WSets.mem [definition, in Coq.FSets.FSetCompat]
Backport_WSets.is_empty [definition, in Coq.FSets.FSetCompat]
Backport_WSets.empty [definition, in Coq.FSets.FSetCompat]
Backport_WSets.Exists [definition, in Coq.FSets.FSetCompat]
Backport_WSets.For_all [definition, in Coq.FSets.FSetCompat]
Backport_WSets.Empty [definition, in Coq.FSets.FSetCompat]
Backport_WSets.Subset [definition, in Coq.FSets.FSetCompat]
Backport_WSets.Equal [definition, in Coq.FSets.FSetCompat]
Backport_WSets.In [definition, in Coq.FSets.FSetCompat]
Backport_WSets.t [definition, in Coq.FSets.FSetCompat]
Backport_WSets.elt [definition, in Coq.FSets.FSetCompat]
Backport_WSets [module, in Coq.FSets.FSetCompat]
Bag [constructor, in Coq.Sets.Multiset]
BalanceProps [module, in Coq.MSets.MSetRBT]
BalanceProps.add_rb [instance, in Coq.MSets.MSetRBT]
BalanceProps.append_arb_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.arbt [inductive, in Coq.MSets.MSetRBT]
BalanceProps.arb_nr_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.arb_nrr_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.ARB_RR [constructor, in Coq.MSets.MSetRBT]
BalanceProps.ARB_RB [constructor, in Coq.MSets.MSetRBT]
BalanceProps.Bk [abbreviation, in Coq.MSets.MSetRBT]
BalanceProps.del_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.del_arb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.diff_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.filter_rb [instance, in Coq.MSets.MSetRBT]
BalanceProps.fold_remove_rb [instance, in Coq.MSets.MSetRBT]
BalanceProps.fold_add_rb [instance, in Coq.MSets.MSetRBT]
BalanceProps.ifred [definition, in Coq.MSets.MSetRBT]
BalanceProps.ifred_or [lemma, in Coq.MSets.MSetRBT]
BalanceProps.ifred_notred [lemma, in Coq.MSets.MSetRBT]
BalanceProps.ins_arb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.ins_rr_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.inter_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.lbalS_arb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.lbalS_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.lbal_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.makeBlack_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.makeRed_rr [lemma, in Coq.MSets.MSetRBT]
BalanceProps.maxdepth_lowerbound [lemma, in Coq.MSets.MSetRBT]
BalanceProps.maxdepth_upperbound [lemma, in Coq.MSets.MSetRBT]
BalanceProps.partition_rb2 [instance, in Coq.MSets.MSetRBT]
BalanceProps.partition_rb1 [instance, in Coq.MSets.MSetRBT]
BalanceProps.rbalS_arb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.rbalS_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.rbal_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.rbal'_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.RBT [projection, in Coq.MSets.MSetRBT]
BalanceProps.Rbt [record, in Coq.MSets.MSetRBT]
BalanceProps.RBT [constructor, in Coq.MSets.MSetRBT]
BalanceProps.Rbt [inductive, in Coq.MSets.MSetRBT]
BalanceProps.rbt [inductive, in Coq.MSets.MSetRBT]
BalanceProps.rbt_ind [definition, in Coq.MSets.MSetRBT]
BalanceProps.rb_mindepth [lemma, in Coq.MSets.MSetRBT]
BalanceProps.rb_maxdepth [lemma, in Coq.MSets.MSetRBT]
BalanceProps.RB_Bk [constructor, in Coq.MSets.MSetRBT]
BalanceProps.RB_Rd [constructor, in Coq.MSets.MSetRBT]
BalanceProps.RB_Leaf [constructor, in Coq.MSets.MSetRBT]
BalanceProps.Rd [abbreviation, in Coq.MSets.MSetRBT]
BalanceProps.redcarac [definition, in Coq.MSets.MSetRBT]
BalanceProps.remove_rb [instance, in Coq.MSets.MSetRBT]
BalanceProps.rrt [inductive, in Coq.MSets.MSetRBT]
BalanceProps.rr_nrr_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.RR_Rd [constructor, in Coq.MSets.MSetRBT]
BalanceProps.singleton_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.treeify_rb [instance, in Coq.MSets.MSetRBT]
BalanceProps.treeify_aux_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.treeify_cont_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.treeify_one_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.treeify_zero_rb [lemma, in Coq.MSets.MSetRBT]
BalanceProps.treeify_rb_invariant [definition, in Coq.MSets.MSetRBT]
BalanceProps.union_rb [lemma, in Coq.MSets.MSetRBT]
Ball_in_inter [lemma, in Coq.Reals.PSeries_reg]
barred [definition, in Coq.Logic.WeakFan]
base [definition, in Coq.Numbers.Cyclic.Abstract.DoubleType]
base [definition, in Coq.Numbers.Cyclic.Int31.Int31]
Base [projection, in Coq.Reals.Rlimit]
BASES [section, in Coq.Vectors.VectorDef]
_ ++ _ [notation, in Coq.Vectors.VectorDef]
base_Int_part [lemma, in Coq.Reals.R_Ifp]
base_fp [lemma, in Coq.Reals.R_Ifp]
base:142 [binder, in Coq.micromega.RingMicromega]
base:16 [binder, in Coq.Strings.OctalString]
base:16 [binder, in Coq.Strings.HexString]
base:16 [binder, in Coq.Strings.BinaryString]
base:19 [binder, in Coq.MSets.MSetGenTree]
base:406 [binder, in Coq.micromega.ZMicromega]
Basics [section, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics [library]
Basics.EqShiftL [section, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Incr [section, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Incr.Incr [variable, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Phi [section, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Phi.Phi [variable, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Recr [section, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Recr.A [variable, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Recr.caserec [variable, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Recr.case0 [variable, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Basics.Recr.case0_caserec [variable, in Coq.Numbers.Cyclic.Int31.Cyclic31]
bas:10 [binder, in Coq.Vectors.VectorDef]
bas:54 [binder, in Coq.Vectors.VectorDef]
bb:602 [binder, in Coq.PArith.BinPos]
Bcons [definition, in Coq.Bool.Bvector]
bdepth [definition, in Coq.micromega.ZMicromega]
Beep [definition, in Coq.Strings.Ascii]
before_witness [inductive, in Coq.Logic.ConstructiveEpsilon]
belowMultiple [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
BEQ [section, in Coq.Vectors.VectorEq]
beq_poly [definition, in Coq.btauto.Algebra]
beq_nat_eq [definition, in Coq.Arith.EqNat]
beq_nat_false [lemma, in Coq.Arith.EqNat]
beq_nat_true [lemma, in Coq.Arith.EqNat]
beq_nat_refl [lemma, in Coq.Arith.EqNat]
beq_nat_false_iff [abbreviation, in Coq.Arith.EqNat]
beq_nat_true_iff [abbreviation, in Coq.Arith.EqNat]
beq_nat [abbreviation, in Coq.Arith.EqNat]
beq_false_not_eq [definition, in Coq.Bool.BoolEq]
beq_eq_not_false [definition, in Coq.Bool.BoolEq]
beq_eq_true [definition, in Coq.Bool.BoolEq]
BEQ.A [variable, in Coq.Vectors.VectorEq]
BEQ.A_eqb_eq [variable, in Coq.Vectors.VectorEq]
BEQ.A_beq [variable, in Coq.Vectors.VectorEq]
Berardi [library]
Berardis_paradox.Retracts.B [variable, in Coq.Logic.Berardi]
Berardis_paradox.Retracts.A [variable, in Coq.Logic.Berardi]
Berardis_paradox.Retracts [section, in Coq.Logic.Berardi]
Berardis_paradox.F [variable, in Coq.Logic.Berardi]
Berardis_paradox.T [variable, in Coq.Logic.Berardi]
Berardis_paradox.Bool [variable, in Coq.Logic.Berardi]
Berardis_paradox.EM [variable, in Coq.Logic.Berardi]
Berardis_paradox [section, in Coq.Logic.Berardi]
between [inductive, in Coq.Arith.Between]
Between [section, in Coq.Arith.Between]
Between [library]
between_not_exists [lemma, in Coq.Arith.Between]
between_or_exists [lemma, in Coq.Arith.Between]
between_in_int [lemma, in Coq.Arith.Between]
between_restr [lemma, in Coq.Arith.Between]
between_Sk_l [lemma, in Coq.Arith.Between]
between_le [lemma, in Coq.Arith.Between]
Between.P [variable, in Coq.Arith.Between]
Between.Q [variable, in Coq.Arith.Between]
bet_eq [lemma, in Coq.Arith.Between]
bet_S [constructor, in Coq.Arith.Between]
bet_emp [constructor, in Coq.Arith.Between]
Bezout [inductive, in Coq.ZArith.Znumtheory]
bezout_rel_prime [lemma, in Coq.ZArith.Znumtheory]
Bezout_intro [constructor, in Coq.ZArith.Znumtheory]
be:36 [binder, in Coq.setoid_ring.Ncring_initial]
BFormula [definition, in Coq.micromega.Tauto]
bFun [definition, in Coq.Logic.FinFun]
bg:38 [binder, in Coq.setoid_ring.Ncring_initial]
Bhigh [definition, in Coq.Bool.Bvector]
bigint [axiom, in Coq.extraction.ExtrOcamlBigIntConv]
bigint_zlike_case [axiom, in Coq.extraction.ExtrOcamlBigIntConv]
bigint_poslike_rec [axiom, in Coq.extraction.ExtrOcamlBigIntConv]
bigint_natlike_rec [axiom, in Coq.extraction.ExtrOcamlBigIntConv]
bigint_of_n [definition, in Coq.extraction.ExtrOcamlBigIntConv]
bigint_of_z [definition, in Coq.extraction.ExtrOcamlBigIntConv]
bigint_of_pos [definition, in Coq.extraction.ExtrOcamlBigIntConv]
bigint_of_nat [definition, in Coq.extraction.ExtrOcamlBigIntConv]
bigint_twice [axiom, in Coq.extraction.ExtrOcamlBigIntConv]
bigint_opp [axiom, in Coq.extraction.ExtrOcamlBigIntConv]
bigint_succ [axiom, in Coq.extraction.ExtrOcamlBigIntConv]
bigint_zero [axiom, in Coq.extraction.ExtrOcamlBigIntConv]
BijComp_FunctExt [lemma, in Coq.Logic.ExtensionalityFacts]
Bijections [section, in Coq.ssr.ssrfun]
BijectionsTheory [section, in Coq.ssr.ssrfun]
BijectionsTheory.A [variable, in Coq.ssr.ssrfun]
BijectionsTheory.B [variable, in Coq.ssr.ssrfun]
BijectionsTheory.C [variable, in Coq.ssr.ssrfun]
BijectionsTheory.f [variable, in Coq.ssr.ssrfun]
BijectionsTheory.h [variable, in Coq.ssr.ssrfun]
Bijections.A [variable, in Coq.ssr.ssrfun]
Bijections.B [variable, in Coq.ssr.ssrfun]
Bijections.bijf [variable, in Coq.ssr.ssrfun]
Bijections.f [variable, in Coq.ssr.ssrfun]
Bijective [constructor, in Coq.ssr.ssrfun]
bijective [inductive, in Coq.ssr.ssrfun]
Bijective [definition, in Coq.Logic.FinFun]
bijective_on [definition, in Coq.ssr.ssrbool]
bijective_in [definition, in Coq.ssr.ssrbool]
BijectivityBijectiveComp [abbreviation, in Coq.Logic.ExtensionalityFacts]
bij_can_bij [lemma, in Coq.ssr.ssrfun]
bij_comp [lemma, in Coq.ssr.ssrfun]
bij_can_eq [lemma, in Coq.ssr.ssrfun]
bij_can_sym [lemma, in Coq.ssr.ssrfun]
bij_inj [lemma, in Coq.ssr.ssrfun]
Binary [section, in Coq.Classes.RelationClasses]
Binary [section, in Coq.Classes.CRelationClasses]
BinaryString [library]
binary_relation [definition, in Coq.Classes.RelationClasses]
binary_operation [definition, in Coq.Classes.RelationClasses]
binary_normalize [definition, in Coq.Floats.SpecFloat]
binary_round [definition, in Coq.Floats.SpecFloat]
binary_round_aux [definition, in Coq.Floats.SpecFloat]
binary_to_Z_to_binary [lemma, in Coq.ZArith.Zdigits]
binary_value_pos [lemma, in Coq.ZArith.Zdigits]
binary_value_Sn [lemma, in Coq.ZArith.Zdigits]
binary_value [lemma, in Coq.ZArith.Zdigits]
Binder [module, in Ltac2.Constr]
bind_unless [lemma, in Coq.ssr.ssrbool]
BinInt [library]
BinIntDef [library]
bInjective [definition, in Coq.Logic.FinFun]
bInjective_bSurjective [lemma, in Coq.Logic.FinFun]
BinList [library]
BinNat [library]
BinNatDef [library]
BinNums [library]
binomial [lemma, in Coq.Reals.Binomial]
Binomial [library]
BinOp [record, in Coq.micromega.ZifyClasses]
BinOpSpec [record, in Coq.micromega.ZifyClasses]
BinOp_Zcompare [instance, in Coq.micromega.ZifyComparison]
BinPos [library]
BinPosDef [library]
BinRel [record, in Coq.micromega.ZifyClasses]
Bintree [library]
bit [definition, in Coq.Numbers.Cyclic.Int63.Int63]
bitE [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
Bits [module, in Coq.Numbers.NatInt.NZBits]
BitsNotation [module, in Coq.Numbers.NatInt.NZBits]
_ << _ [notation, in Coq.Numbers.NatInt.NZBits]
_ >> _ [notation, in Coq.Numbers.NatInt.NZBits]
_ .[ _ ] [notation, in Coq.Numbers.NatInt.NZBits]
Bits' [module, in Coq.Numbers.NatInt.NZBits]
Bits.div2 [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.land [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.ldiff [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.lor [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.lxor [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.shiftl [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.shiftr [axiom, in Coq.Numbers.NatInt.NZBits]
Bits.testbit [axiom, in Coq.Numbers.NatInt.NZBits]
bitwise [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
bitwise [definition, in Coq.Init.Nat]
bit_add_or [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
bit_0 [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
bit_lsl [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
bit_ext [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
bit_half [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
bit_M [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
bit_1 [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
bit_b2i [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
bit_lsr [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
bit_split [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
bit_0_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
bit_value [definition, in Coq.ZArith.Zdigits]
Black [constructor, in Coq.MSets.MSetRBT]
block [definition, in Coq.Program.Equality]
Blow [definition, in Coq.Bool.Bvector]
bl:37 [binder, in Coq.setoid_ring.Ncring_initial]
Bneg [definition, in Coq.Bool.Bvector]
Bnil [definition, in Coq.Bool.Bvector]
Bnth [abbreviation, in Coq.NArith.Ndigits]
Bnth_Nbit [lemma, in Coq.NArith.Ndigits]
Bn:104 [binder, in Coq.Reals.SeqSeries]
Bn:16 [binder, in Coq.Reals.Rprod]
Bn:179 [binder, in Coq.Reals.SeqProp]
Bn:201 [binder, in Coq.Reals.SeqProp]
Bn:225 [binder, in Coq.Reals.SeqProp]
Bn:35 [binder, in Coq.Reals.PartSum]
Bn:4 [binder, in Coq.Reals.Cauchy_prod]
Bn:52 [binder, in Coq.Reals.PartSum]
Bn:55 [binder, in Coq.Reals.Abstract.ConstructiveLimits]
Bn:56 [binder, in Coq.Reals.PartSum]
Bn:63 [binder, in Coq.Reals.PartSum]
Bn:74 [binder, in Coq.Reals.PartSum]
Bn:8 [binder, in Coq.Reals.Cauchy_prod]
Bn:8 [binder, in Coq.Reals.Abstract.ConstructiveSum]
Bn:83 [binder, in Coq.Reals.PartSum]
Bn:97 [binder, in Coq.Reals.SeqSeries]
Bolzano_Weierstrass [lemma, in Coq.Reals.Rtopology]
Bool [section, in Coq.Lists.List]
bool [inductive, in Coq.Init.Datatypes]
Bool [section, in Coq.btauto.Reflect]
Bool [library]
Bool [library]
BooleanDecidableType [module, in Coq.Structures.Equalities]
BooleanDecidableType' [module, in Coq.Structures.Equalities]
BooleanEqualityType [module, in Coq.Structures.Equalities]
BooleanEqualityType' [module, in Coq.Structures.Equalities]
BOOLEAN_VECTORS [section, in Coq.Bool.Bvector]
boolean_witness_nonzero [lemma, in Coq.btauto.Reflect]
boolean_witness [definition, in Coq.btauto.Reflect]
BoolEq [library]
BoolEqualityFacts [module, in Coq.Structures.Equalities]
BoolEqualityFacts.eqb_sym [lemma, in Coq.Structures.Equalities]
BoolEqualityFacts.eqb_refl [lemma, in Coq.Structures.Equalities]
BoolEqualityFacts.eqb_neq [lemma, in Coq.Structures.Equalities]
BoolEqualityFacts.eqb_spec [lemma, in Coq.Structures.Equalities]
BoolEqualityFacts.eqb_compat [instance, in Coq.Structures.Equalities]
boolfunPredType [definition, in Coq.ssr.ssrbool]
BoolIf [section, in Coq.ssr.ssrbool]
BoolIf.A [variable, in Coq.ssr.ssrbool]
BoolIf.b [variable, in Coq.ssr.ssrbool]
BoolIf.B [variable, in Coq.ssr.ssrbool]
BoolIf.f [variable, in Coq.ssr.ssrbool]
BoolIf.vF [variable, in Coq.ssr.ssrbool]
BoolIf.vT [variable, in Coq.ssr.ssrbool]
BoolIf.x [variable, in Coq.ssr.ssrbool]
BoolNotations [module, in Coq.Bool.Bool]
_ =? _ (bool_scope) [notation, in Coq.Bool.Bool]
_ ?= _ (bool_scope) [notation, in Coq.Bool.Bool]
_ < _ (bool_scope) [notation, in Coq.Bool.Bool]
_ <= _ (bool_scope) [notation, in Coq.Bool.Bool]
BoolOrd [module, in Coq.Bool.BoolOrder]
BoolOrder [library]
BoolOrderFacts [module, in Coq.Structures.OrdersFacts]
BoolOrderFacts.eqb_compare [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_compare [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_antisym [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_refl [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_gt [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_nle [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_spec [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.leb_spec0 [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_compare [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_antisym [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_irrefl [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_ge [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_nlt [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_spec [lemma, in Coq.Structures.OrdersFacts]
BoolOrderFacts.ltb_spec0 [lemma, in Coq.Structures.OrdersFacts]
BoolOrdSpecs [module, in Coq.Structures.Orders]
BoolOrd.compare [definition, in Coq.Bool.BoolOrder]
BoolOrd.compare_spec [definition, in Coq.Bool.BoolOrder]
BoolOrd.eq [definition, in Coq.Bool.BoolOrder]
BoolOrd.eqb [definition, in Coq.Bool.BoolOrder]
BoolOrd.eqb_eq [definition, in Coq.Bool.BoolOrder]
BoolOrd.eq_trans [definition, in Coq.Bool.BoolOrder]
BoolOrd.eq_sym [definition, in Coq.Bool.BoolOrder]
BoolOrd.eq_refl [definition, in Coq.Bool.BoolOrder]
BoolOrd.eq_dec [definition, in Coq.Bool.BoolOrder]
BoolOrd.eq_equiv [definition, in Coq.Bool.BoolOrder]
BoolOrd.le [definition, in Coq.Bool.BoolOrder]
BoolOrd.le_lteq [definition, in Coq.Bool.BoolOrder]
BoolOrd.lt [definition, in Coq.Bool.BoolOrder]
BoolOrd.lt_total [definition, in Coq.Bool.BoolOrder]
BoolOrd.lt_compat [definition, in Coq.Bool.BoolOrder]
BoolOrd.lt_strorder [definition, in Coq.Bool.BoolOrder]
BoolOrd.t [definition, in Coq.Bool.BoolOrder]
boolP [lemma, in Coq.ssr.ssrbool]
boolP [inductive, in Coq.Logic.ClassicalFacts]
BoolP [definition, in Coq.Logic.ClassicalFacts]
boolP_indd [definition, in Coq.Logic.ClassicalFacts]
boolP_elim_redr [definition, in Coq.Logic.ClassicalFacts]
boolP_elim_redl [definition, in Coq.Logic.ClassicalFacts]
BoolP_dep_induction [definition, in Coq.Logic.ClassicalFacts]
BoolP_elim_redr [definition, in Coq.Logic.ClassicalFacts]
BoolP_elim_redl [definition, in Coq.Logic.ClassicalFacts]
BoolP_elim [definition, in Coq.Logic.ClassicalFacts]
BoolSpec [inductive, in Coq.Init.Datatypes]
BoolSpecF [constructor, in Coq.Init.Datatypes]
BoolSpecT [constructor, in Coq.Init.Datatypes]
BoolTheory [lemma, in Coq.setoid_ring.Ring]
bool_eq_ok [lemma, in Coq.setoid_ring.Ring]
bool_eq [definition, in Coq.setoid_ring.Ring]
Bool_as_DT [module, in Coq.Structures.OrdersEx]
Bool_as_OT [module, in Coq.Structures.OrdersEx]
bool_choice [lemma, in Coq.Init.Specif]
bool_of_Z [definition, in Coq.micromega.ZifyBool]
bool_6 [abbreviation, in Coq.Bool.Bool]
bool_3 [abbreviation, in Coq.Bool.Bool]
bool_1 [abbreviation, in Coq.Bool.Bool]
bool_dec [lemma, in Coq.Bool.Bool]
bool_function_eqdec [instance, in Coq.Classes.EquivDec]
bool_eqdec [instance, in Coq.Classes.EquivDec]
Bool_eq_dec.beq_eq [variable, in Coq.Bool.BoolEq]
Bool_eq_dec.beq_refl [variable, in Coq.Bool.BoolEq]
Bool_eq_dec.beq [variable, in Coq.Bool.BoolEq]
Bool_eq_dec.A [variable, in Coq.Bool.BoolEq]
Bool_eq_dec [section, in Coq.Bool.BoolEq]
bool_function_eqdec [instance, in Coq.Classes.SetoidDec]
bool_eqdec [instance, in Coq.Classes.SetoidDec]
bool_of_sumbool [definition, in Coq.Bool.Sumbool]
bool_eq_ind [definition, in Coq.Bool.Sumbool]
bool_eq_rec [definition, in Coq.Bool.Sumbool]
Bool_nat [library]
Bool.A [variable, in Coq.Lists.List]
Bool.f [variable, in Coq.Lists.List]
Bool2Dec [module, in Coq.Structures.Equalities]
Bot [constructor, in Coq.rtauto.Rtauto]
Bottom [inductive, in Coq.Sets.Cpo]
Bottom_definition [constructor, in Coq.Sets.Cpo]
bot:23 [binder, in Coq.Sets.Cpo]
bot:45 [binder, in Coq.Sets.Cpo]
Boule [definition, in Coq.Reals.PSeries_reg]
Boule_center [lemma, in Coq.Reals.PSeries_reg]
boule_in_interval [definition, in Coq.Reals.PSeries_reg]
boule_of_interval [definition, in Coq.Reals.PSeries_reg]
Boule_convex [lemma, in Coq.Reals.PSeries_reg]
Boule_lt [lemma, in Coq.Reals.Ratan]
Boule_half_to_interval [lemma, in Coq.Reals.Ratan]
bound [definition, in Coq.Reals.Raxioms]
bounded [definition, in Coq.Floats.SpecFloat]
bounded [definition, in Coq.Reals.Rtopology]
Bounds [section, in Coq.Sets.Cpo]
Bounds.C [variable, in Coq.Sets.Cpo]
Bounds.D [variable, in Coq.Sets.Cpo]
Bounds.R [variable, in Coq.Sets.Cpo]
Bounds.U [variable, in Coq.Sets.Cpo]
bound_var [definition, in Coq.micromega.ZMicromega]
Box [record, in Coq.Logic.StrictProp]
box [constructor, in Coq.Logic.StrictProp]
BPred [projection, in Coq.micromega.ZifyClasses]
bracket [projection, in Coq.setoid_ring.Algebra_syntax]
Bracket [record, in Coq.setoid_ring.Algebra_syntax]
bracket [constructor, in Coq.setoid_ring.Algebra_syntax]
Bracket [inductive, in Coq.setoid_ring.Algebra_syntax]
Branch [constructor, in Coq.micromega.VarMap]
Branch0 [constructor, in Coq.rtauto.Bintree]
Branch1 [constructor, in Coq.rtauto.Bintree]
BshiftL [definition, in Coq.Bool.Bvector]
BshiftL_iter [definition, in Coq.Bool.Bvector]
BshiftRa [definition, in Coq.Bool.Bvector]
BshiftRa_iter [definition, in Coq.Bool.Bvector]
BshiftRl [definition, in Coq.Bool.Bvector]
BshiftRl_iter [definition, in Coq.Bool.Bvector]
Bsign [definition, in Coq.Bool.Bvector]
BSpec [projection, in Coq.micromega.ZifyClasses]
bsup:44 [binder, in Coq.Sets.Cpo]
bsup:49 [binder, in Coq.Sets.Cpo]
bSurjective [definition, in Coq.Logic.FinFun]
bSurjective_bBijective [lemma, in Coq.Logic.FinFun]
Btauto [library]
Build_Formula [constructor, in Coq.micromega.RingMicromega]
Build_Setoid_Theory [definition, in Coq.Setoids.Setoid]
build_heap [inductive, in Coq.Sorting.Heap]
BVand [definition, in Coq.Bool.Bvector]
Bvector [definition, in Coq.Bool.Bvector]
Bvector [library]
BvectorNotations [module, in Coq.Bool.Bvector]
_ =? _ (Bvector_scope) [notation, in Coq.Bool.Bvector]
_ ^| _ (Bvector_scope) [notation, in Coq.Bool.Bvector]
_ ^⊕ _ (Bvector_scope) [notation, in Coq.Bool.Bvector]
_ ^& _ (Bvector_scope) [notation, in Coq.Bool.Bvector]
^~ _ (Bvector_scope) [notation, in Coq.Bool.Bvector]
Bvect_false [definition, in Coq.Bool.Bvector]
Bvect_true [definition, in Coq.Bool.Bvector]
BVeq [definition, in Coq.Bool.Bvector]
BVor [definition, in Coq.Bool.Bvector]
BVxor [definition, in Coq.Bool.Bvector]
bv':176 [binder, in Coq.NArith.Ndigits]
bv':179 [binder, in Coq.NArith.Ndigits]
Bv2N [definition, in Coq.NArith.Ndigits]
Bv2N_upper_bound [lemma, in Coq.NArith.Ndigits]
Bv2N_Nsize_1 [lemma, in Coq.NArith.Ndigits]
Bv2N_Nsize [lemma, in Coq.NArith.Ndigits]
Bv2N_N2Bv [lemma, in Coq.NArith.Ndigits]
bv:10 [binder, in Coq.Bool.Bvector]
bv:12 [binder, in Coq.Bool.Bvector]
bv:14 [binder, in Coq.ZArith.Zdigits]
bv:140 [binder, in Coq.NArith.Ndigits]
bv:146 [binder, in Coq.NArith.Ndigits]
bv:148 [binder, in Coq.NArith.Ndigits]
bv:150 [binder, in Coq.NArith.Ndigits]
bv:162 [binder, in Coq.NArith.Ndigits]
bv:164 [binder, in Coq.NArith.Ndigits]
bv:166 [binder, in Coq.NArith.Ndigits]
bv:17 [binder, in Coq.Bool.Bvector]
bv:175 [binder, in Coq.NArith.Ndigits]
bv:178 [binder, in Coq.NArith.Ndigits]
bv:19 [binder, in Coq.ZArith.Zdigits]
bv:21 [binder, in Coq.ZArith.Zdigits]
bv:22 [binder, in Coq.Bool.Bvector]
bv:4 [binder, in Coq.Bool.Bvector]
bv:41 [binder, in Coq.ZArith.Zdigits]
bv:43 [binder, in Coq.ZArith.Zdigits]
bv:7 [binder, in Coq.Bool.Bvector]
byte [inductive, in Coq.Init.Byte]
Byte [library]
Byte [library]
ByteNil [definition, in Coq.Strings.ByteVector]
ByteNotations [module, in Coq.Strings.Byte]
_ =? _ (byte_scope) [notation, in Coq.Strings.Byte]
ByteSyntaxNotations [module, in Coq.Init.Byte]
ByteVector [definition, in Coq.Strings.ByteVector]
ByteVector [library]
ByteV2N [definition, in Coq.NArith.Ndigits]
ByteV2N_upper_bound [lemma, in Coq.NArith.Ndigits]
byte_of_byte [definition, in Coq.Init.Byte]
byte_of_ascii_via_nat [lemma, in Coq.Strings.Ascii]
byte_of_ascii_via_N [lemma, in Coq.Strings.Ascii]
byte_of_ascii_of_byte [lemma, in Coq.Strings.Ascii]
byte_of_ascii [definition, in Coq.Strings.Ascii]
byte_eq_dec [definition, in Coq.Strings.Byte]
byte_dec_bl [lemma, in Coq.Strings.Byte]
byte_dec_lb [lemma, in Coq.Strings.Byte]
b'':163 [binder, in Coq.Bool.Bool]
b'':168 [binder, in Coq.Bool.Bool]
b'':171 [binder, in Coq.Bool.Bool]
b'':174 [binder, in Coq.Bool.Bool]
b'':177 [binder, in Coq.Bool.Bool]
b':105 [binder, in Coq.Sorting.PermutSetoid]
b':14 [binder, in Coq.Logic.Diaconescu]
b':154 [binder, in Coq.Init.Nat]
b':160 [binder, in Coq.Bool.Bool]
b':160 [binder, in Coq.MSets.MSetPositive]
b':162 [binder, in Coq.Bool.Bool]
b':165 [binder, in Coq.Bool.Bool]
b':167 [binder, in Coq.Bool.Bool]
b':170 [binder, in Coq.Bool.Bool]
B':170 [binder, in Coq.Init.Logic]
b':173 [binder, in Coq.Bool.Bool]
b':176 [binder, in Coq.Bool.Bool]
b':179 [binder, in Coq.Bool.Bool]
b':181 [binder, in Coq.Bool.Bool]
b':183 [binder, in Coq.Bool.Bool]
b':184 [binder, in Coq.FSets.FSetPositive]
b':191 [binder, in Coq.Bool.Bool]
b':226 [binder, in Coq.Bool.Bool]
b':245 [binder, in Coq.Bool.Bool]
b':3 [binder, in Coq.ssr.ssrbool]
b':4 [binder, in Coq.FSets.FMapFacts]
b':48 [binder, in Coq.Structures.OrdersFacts]
b':49 [binder, in Coq.Bool.Bool]
b':67 [binder, in Coq.Sorting.PermutSetoid]
b':72 [binder, in Coq.Vectors.Fin]
b':84 [binder, in Coq.Sorting.PermutSetoid]
b':88 [binder, in Coq.Sorting.PermutSetoid]
b':91 [binder, in Coq.Sorting.PermutSetoid]
b':99 [binder, in Coq.Sorting.PermutSetoid]
b0:16 [binder, in Coq.Strings.ByteVector]
b0:29 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b0:29 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b0:338 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b0:402 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b0:51 [binder, in Coq.Strings.Ascii]
B1 [definition, in Coq.Reals.Cos_rel]
B1_cvg [lemma, in Coq.Reals.Cos_rel]
b1:10 [binder, in Coq.Bool.Bool]
b1:100 [binder, in Coq.Bool.Bool]
b1:104 [binder, in Coq.Bool.Bool]
b1:106 [binder, in Coq.Bool.Bool]
b1:109 [binder, in Coq.Bool.Bool]
b1:11 [binder, in Coq.Bool.BoolOrder]
b1:11 [binder, in Coq.Init.Datatypes]
b1:112 [binder, in Coq.Bool.Bool]
b1:115 [binder, in Coq.Bool.Bool]
b1:118 [binder, in Coq.Bool.Bool]
b1:121 [binder, in Coq.Bool.Bool]
b1:123 [binder, in Coq.Bool.Bool]
b1:125 [binder, in Coq.Sorting.PermutSetoid]
b1:125 [binder, in Coq.Bool.Bool]
b1:127 [binder, in Coq.Bool.Bool]
b1:129 [binder, in Coq.Bool.Bool]
b1:13 [binder, in Coq.Bool.BoolOrder]
b1:13 [binder, in Coq.Bool.Bool]
b1:13 [binder, in Coq.Init.Datatypes]
b1:131 [binder, in Coq.Bool.Bool]
b1:138 [binder, in Coq.Bool.Bool]
b1:140 [binder, in Coq.Bool.Bool]
b1:142 [binder, in Coq.Bool.Bool]
b1:145 [binder, in Coq.Bool.Bool]
b1:148 [binder, in Coq.Bool.Bool]
b1:15 [binder, in Coq.Bool.BoolOrder]
b1:15 [binder, in Coq.Bool.Bool]
b1:150 [binder, in Coq.Sorting.Permutation]
b1:151 [binder, in Coq.Bool.Bool]
b1:165 [binder, in Coq.MSets.MSetPositive]
b1:17 [binder, in Coq.Bool.BoolOrder]
b1:18 [binder, in Coq.Bool.Bool]
b1:18 [binder, in Coq.Strings.ByteVector]
b1:184 [binder, in Coq.Bool.Bool]
b1:186 [binder, in Coq.Bool.Bool]
b1:189 [binder, in Coq.FSets.FSetPositive]
b1:19 [binder, in Coq.Bool.BoolOrder]
b1:2 [binder, in Coq.Bool.BoolOrder]
b1:2 [binder, in Coq.setoid_ring.Ring]
b1:20 [binder, in Coq.Init.Datatypes]
b1:202 [binder, in Coq.Logic.ClassicalFacts]
b1:206 [binder, in Coq.Bool.Bool]
b1:207 [binder, in Coq.Logic.ClassicalFacts]
b1:208 [binder, in Coq.Bool.Bool]
b1:214 [binder, in Coq.Bool.Bool]
b1:216 [binder, in Coq.Bool.Bool]
b1:22 [binder, in Coq.Bool.Bool]
b1:24 [binder, in Coq.Bool.Bool]
b1:261 [binder, in Coq.Logic.ClassicalFacts]
b1:263 [binder, in Coq.Logic.ClassicalFacts]
b1:28 [binder, in Coq.Sorting.PermutEq]
b1:29 [binder, in Coq.Bool.Bool]
b1:3 [binder, in Coq.Bool.Bool]
b1:38 [binder, in Coq.Bool.Bool]
b1:385 [binder, in Coq.micromega.ZMicromega]
b1:4 [binder, in Coq.setoid_ring.Ring]
b1:42 [binder, in Coq.Bool.Bool]
b1:44 [binder, in Coq.Bool.Bool]
b1:52 [binder, in Coq.Strings.Ascii]
b1:55 [binder, in Coq.Sorting.CPermutation]
b1:59 [binder, in Coq.Bool.Bool]
b1:61 [binder, in Coq.Bool.Bool]
b1:63 [binder, in Coq.Bool.Bool]
b1:67 [binder, in Coq.Bool.Bool]
b1:69 [binder, in Coq.Bool.Bool]
b1:7 [binder, in Coq.Init.Datatypes]
b1:70 [binder, in Coq.Init.Datatypes]
b1:71 [binder, in Coq.Bool.Bool]
b1:8 [binder, in Coq.Bool.BoolOrder]
b1:80 [binder, in Coq.Bool.Bool]
b1:82 [binder, in Coq.Bool.Bool]
b1:85 [binder, in Coq.Bool.Bool]
b1:87 [binder, in Coq.Bool.Bool]
b1:9 [binder, in Coq.Init.Datatypes]
b1:91 [binder, in Coq.Bool.Bool]
b1:93 [binder, in Coq.Bool.Bool]
b2i [definition, in Coq.Numbers.Cyclic.Int63.Int63]
b2:10 [binder, in Coq.Init.Datatypes]
b2:101 [binder, in Coq.Bool.Bool]
b2:105 [binder, in Coq.Bool.Bool]
b2:107 [binder, in Coq.Bool.Bool]
b2:11 [binder, in Coq.Bool.Bool]
b2:110 [binder, in Coq.Bool.Bool]
b2:113 [binder, in Coq.Bool.Bool]
b2:116 [binder, in Coq.Bool.Bool]
b2:119 [binder, in Coq.Bool.Bool]
b2:12 [binder, in Coq.Bool.BoolOrder]
b2:12 [binder, in Coq.Init.Datatypes]
b2:122 [binder, in Coq.Bool.Bool]
b2:124 [binder, in Coq.Bool.Bool]
b2:126 [binder, in Coq.Bool.Bool]
b2:127 [binder, in Coq.Sorting.PermutSetoid]
b2:128 [binder, in Coq.Bool.Bool]
b2:130 [binder, in Coq.Bool.Bool]
b2:132 [binder, in Coq.Bool.Bool]
b2:139 [binder, in Coq.Bool.Bool]
b2:14 [binder, in Coq.Bool.BoolOrder]
b2:14 [binder, in Coq.Bool.Bool]
b2:14 [binder, in Coq.Init.Datatypes]
b2:141 [binder, in Coq.Bool.Bool]
b2:143 [binder, in Coq.Bool.Bool]
b2:146 [binder, in Coq.Bool.Bool]
b2:149 [binder, in Coq.Bool.Bool]
b2:151 [binder, in Coq.Sorting.Permutation]
b2:152 [binder, in Coq.Bool.Bool]
b2:16 [binder, in Coq.Bool.BoolOrder]
b2:16 [binder, in Coq.Bool.Bool]
b2:166 [binder, in Coq.MSets.MSetPositive]
b2:18 [binder, in Coq.Bool.BoolOrder]
b2:185 [binder, in Coq.Bool.Bool]
b2:187 [binder, in Coq.Bool.Bool]
b2:19 [binder, in Coq.Bool.Bool]
b2:190 [binder, in Coq.FSets.FSetPositive]
b2:20 [binder, in Coq.Bool.BoolOrder]
b2:20 [binder, in Coq.Strings.ByteVector]
b2:203 [binder, in Coq.Logic.ClassicalFacts]
b2:207 [binder, in Coq.Bool.Bool]
b2:208 [binder, in Coq.Logic.ClassicalFacts]
b2:209 [binder, in Coq.Bool.Bool]
b2:21 [binder, in Coq.Init.Datatypes]
b2:215 [binder, in Coq.Bool.Bool]
b2:217 [binder, in Coq.Bool.Bool]
b2:23 [binder, in Coq.Bool.Bool]
b2:25 [binder, in Coq.Bool.Bool]
b2:262 [binder, in Coq.Logic.ClassicalFacts]
b2:264 [binder, in Coq.Logic.ClassicalFacts]
b2:3 [binder, in Coq.Bool.BoolOrder]
b2:3 [binder, in Coq.setoid_ring.Ring]
b2:30 [binder, in Coq.Sorting.PermutEq]
b2:30 [binder, in Coq.Bool.Bool]
b2:386 [binder, in Coq.micromega.ZMicromega]
b2:39 [binder, in Coq.Bool.Bool]
b2:4 [binder, in Coq.Bool.Bool]
b2:43 [binder, in Coq.Bool.Bool]
b2:45 [binder, in Coq.Bool.Bool]
b2:5 [binder, in Coq.setoid_ring.Ring]
b2:53 [binder, in Coq.Strings.Ascii]
b2:56 [binder, in Coq.Sorting.CPermutation]
b2:60 [binder, in Coq.Bool.Bool]
b2:62 [binder, in Coq.Bool.Bool]
b2:64 [binder, in Coq.Bool.Bool]
b2:68 [binder, in Coq.Bool.Bool]
b2:70 [binder, in Coq.Bool.Bool]
b2:71 [binder, in Coq.Init.Datatypes]
b2:72 [binder, in Coq.Bool.Bool]
b2:8 [binder, in Coq.Init.Datatypes]
b2:81 [binder, in Coq.Bool.Bool]
b2:83 [binder, in Coq.Bool.Bool]
b2:86 [binder, in Coq.Bool.Bool]
b2:88 [binder, in Coq.Bool.Bool]
b2:9 [binder, in Coq.Bool.BoolOrder]
b2:92 [binder, in Coq.Bool.Bool]
b2:94 [binder, in Coq.Bool.Bool]
b3:10 [binder, in Coq.Bool.BoolOrder]
b3:108 [binder, in Coq.Bool.Bool]
b3:111 [binder, in Coq.Bool.Bool]
b3:114 [binder, in Coq.Bool.Bool]
b3:117 [binder, in Coq.Bool.Bool]
b3:120 [binder, in Coq.Bool.Bool]
b3:144 [binder, in Coq.Bool.Bool]
b3:147 [binder, in Coq.Bool.Bool]
b3:150 [binder, in Coq.Bool.Bool]
b3:153 [binder, in Coq.Bool.Bool]
b3:22 [binder, in Coq.Strings.ByteVector]
b3:4 [binder, in Coq.Bool.BoolOrder]
b3:40 [binder, in Coq.Bool.Bool]
b3:54 [binder, in Coq.Strings.Ascii]
b3:84 [binder, in Coq.Bool.Bool]
b4:24 [binder, in Coq.Strings.ByteVector]
b4:55 [binder, in Coq.Strings.Ascii]
b5:26 [binder, in Coq.Strings.ByteVector]
b5:56 [binder, in Coq.Strings.Ascii]
b6:28 [binder, in Coq.Strings.ByteVector]
b6:57 [binder, in Coq.Strings.Ascii]
b7:30 [binder, in Coq.Strings.ByteVector]
b7:58 [binder, in Coq.Strings.Ascii]
b:1 [binder, in Coq.Bool.BoolOrder]
b:1 [binder, in Coq.setoid_ring.Ring]
b:1 [binder, in Coq.ssr.ssrbool]
b:1 [binder, in Coq.micromega.ZifyBool]
b:1 [binder, in Coq.ZArith.Zdigits]
b:1 [binder, in Coq.ZArith.Zdiv]
b:1 [binder, in Coq.Bool.Bool]
b:1 [binder, in Coq.Bool.Sumbool]
b:10 [binder, in Coq.Logic.ConstructiveEpsilon]
b:10 [binder, in Coq.Bool.IfProp]
b:10 [binder, in Coq.ZArith.Zpow_facts]
B:10 [binder, in Coq.Logic.JMeq]
b:10 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
b:10 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:10 [binder, in Coq.Numbers.Natural.Abstract.NSqrt]
b:10 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:10 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:10 [binder, in Coq.ZArith.Zdiv]
b:10 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:10 [binder, in Coq.Numbers.Integer.Abstract.ZPow]
B:10 [binder, in Coq.Program.Basics]
b:10 [binder, in Coq.ZArith.Znumtheory]
b:10 [binder, in Coq.ZArith.Zeuclid]
b:100 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:100 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:100 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:100 [binder, in Coq.setoid_ring.Field_theory]
b:100 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:100 [binder, in Coq.Numbers.NatInt.NZDiv]
b:100 [binder, in Coq.Reals.RiemannInt_SF]
b:100 [binder, in Coq.NArith.Ndec]
B:1001 [binder, in Coq.Lists.List]
B:1007 [binder, in Coq.Lists.List]
b:101 [binder, in Coq.ZArith.BinIntDef]
b:101 [binder, in Coq.ZArith.Zdiv]
b:101 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:101 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:101 [binder, in Coq.Logic.ClassicalFacts]
b:101 [binder, in Coq.PArith.BinPosDef]
b:102 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
B:102 [binder, in Coq.Logic.FunctionalExtensionality]
b:102 [binder, in Coq.setoid_ring.Field_theory]
b:102 [binder, in Coq.Bool.Bool]
b:102 [binder, in Coq.ZArith.Zquot]
b:103 [binder, in Coq.Vectors.VectorSpec]
b:103 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
B:103 [binder, in Coq.Sorting.PermutSetoid]
b:103 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:103 [binder, in Coq.ssr.ssrbool]
b:103 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:103 [binder, in Coq.ZArith.Zdiv]
b:103 [binder, in Coq.Bool.Bool]
b:103 [binder, in Coq.Numbers.NatInt.NZDiv]
b:103 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:103 [binder, in Coq.NArith.Ndec]
b:1039 [binder, in Coq.Lists.List]
b:104 [binder, in Coq.Sorting.PermutSetoid]
b:104 [binder, in Coq.Reals.RiemannInt]
b:104 [binder, in Coq.Reals.NewtonInt]
b:104 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:104 [binder, in Coq.ZArith.Znumtheory]
b:105 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
B:105 [binder, in Coq.ssr.ssreflect]
b:105 [binder, in Coq.ZArith.Zdiv]
b:105 [binder, in Coq.Arith.PeanoNat]
b:105 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:105 [binder, in Coq.Logic.ClassicalFacts]
b:106 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:106 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:106 [binder, in Coq.ssr.ssrbool]
b:106 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:107 [binder, in Coq.Arith.PeanoNat]
b:107 [binder, in Coq.Reals.Rbasic_fun]
b:107 [binder, in Coq.ZArith.Zquot]
b:107 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:107 [binder, in Coq.PArith.BinPosDef]
b:107 [binder, in Coq.ZArith.Znumtheory]
b:107 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:108 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:108 [binder, in Coq.FSets.FMapFacts]
b:108 [binder, in Coq.Init.Nat]
B:108 [binder, in Coq.ssr.ssreflect]
b:108 [binder, in Coq.ZArith.Zdiv]
b:108 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:108 [binder, in Coq.Numbers.NatInt.NZDiv]
B:108 [binder, in Coq.Init.Logic]
b:108 [binder, in Coq.Reals.RiemannInt_SF]
b:109 [binder, in Coq.Vectors.VectorSpec]
b:109 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:109 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:109 [binder, in Coq.Reals.RiemannInt]
b:109 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:109 [binder, in Coq.Arith.PeanoNat]
b:109 [binder, in Coq.Reals.Rbasic_fun]
b:109 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:109 [binder, in Coq.Numbers.NatInt.NZMulOrder]
B:11 [binder, in Coq.Logic.Decidable]
b:11 [binder, in Coq.Logic.ConstructiveEpsilon]
b:11 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:11 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:11 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]
b:11 [binder, in Coq.Reals.RiemannInt]
B:11 [binder, in Coq.Program.Subset]
b:11 [binder, in Coq.ssr.ssrbool]
b:11 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:11 [binder, in Coq.setoid_ring.Algebra_syntax]
B:11 [binder, in Coq.Logic.ClassicalChoice]
B:11 [binder, in Coq.Logic.IndefiniteDescription]
B:11 [binder, in Coq.rtauto.Bintree]
B:11 [binder, in Coq.Classes.CRelationClasses]
b:11 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
b:11 [binder, in Coq.ZArith.Zquot]
b:11 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:11 [binder, in Coq.micromega.Refl]
b:110 [binder, in Coq.Reals.NewtonInt]
b:110 [binder, in Coq.ZArith.Zquot]
b:110 [binder, in Coq.PArith.BinPosDef]
b:111 [binder, in Coq.ZArith.Zdiv]
b:111 [binder, in Coq.Arith.PeanoNat]
b:111 [binder, in Coq.Reals.Rbasic_fun]
b:111 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:111 [binder, in Coq.Numbers.NatInt.NZDiv]
b:111 [binder, in Coq.Numbers.NatInt.NZMulOrder]
b:111 [binder, in Coq.ZArith.Znumtheory]
b:112 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:112 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:112 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:112 [binder, in Coq.Structures.OrderedTypeEx]
b:112 [binder, in Coq.Reals.Abstract.ConstructiveLimits]
b:112 [binder, in Coq.MSets.MSetPositive]
b:112 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:112 [binder, in Coq.Logic.ClassicalFacts]
b:112 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
b:112 [binder, in Coq.Reals.RiemannInt_SF]
b:112 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:113 [binder, in Coq.ZArith.BinIntDef]
b:113 [binder, in Coq.Reals.Rbasic_fun]
b:113 [binder, in Coq.ZArith.Zquot]
b:113 [binder, in Coq.Numbers.NatInt.NZMulOrder]
b:113 [binder, in Coq.ZArith.Znumtheory]
b:114 [binder, in Coq.Reals.RiemannInt]
b:114 [binder, in Coq.Arith.PeanoNat]
b:114 [binder, in Coq.Numbers.NatInt.NZDiv]
b:115 [binder, in Coq.Vectors.VectorSpec]
b:115 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:115 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:115 [binder, in Coq.FSets.FSetPositive]
b:115 [binder, in Coq.Reals.Rbasic_fun]
b:115 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:115 [binder, in Coq.ZArith.Znumtheory]
b:116 [binder, in Coq.ZArith.BinIntDef]
b:116 [binder, in Coq.Structures.OrderedTypeEx]
b:116 [binder, in Coq.ZArith.Zquot]
b:116 [binder, in Coq.Numbers.NatInt.NZMulOrder]
b:116 [binder, in Coq.Logic.ClassicalFacts]
b:116 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
b:117 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:117 [binder, in Coq.Reals.MVT]
b:117 [binder, in Coq.ZArith.Zdiv]
b:117 [binder, in Coq.Numbers.NatInt.NZDiv]
b:117 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
b:117 [binder, in Coq.ZArith.Znumtheory]
b:118 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:118 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:118 [binder, in Coq.Numbers.NatInt.NZMulOrder]
b:118 [binder, in Coq.PArith.BinPosDef]
b:119 [binder, in Coq.ZArith.BinIntDef]
b:119 [binder, in Coq.ZArith.Zdiv]
b:119 [binder, in Coq.ZArith.Zquot]
B:119 [binder, in Coq.Logic.ClassicalFacts]
b:12 [binder, in Coq.Reals.Runcountable]
b:12 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:12 [binder, in Coq.Bool.IfProp]
b:12 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:12 [binder, in Coq.Numbers.Natural.Abstract.NSqrt]
b:12 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:12 [binder, in Coq.Numbers.NatInt.NZLog]
b:12 [binder, in Coq.ZArith.Zdiv]
b:12 [binder, in Coq.Sorting.Sorted]
B:12 [binder, in Coq.Logic.ClassicalUniqueChoice]
b:12 [binder, in Coq.Reals.NewtonInt]
b:12 [binder, in Coq.ZArith.Zgcd_alt]
b:12 [binder, in Coq.ZArith.Zpow_alt]
b:12 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:12 [binder, in Coq.Numbers.Integer.Abstract.ZPow]
B:12 [binder, in Coq.Program.Basics]
b:12 [binder, in Coq.ZArith.Znumtheory]
b:12 [binder, in Coq.QArith.Qpower]
B:12 [binder, in Coq.Logic.FinFun]
b:120 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:120 [binder, in Coq.Numbers.NatInt.NZDiv]
b:120 [binder, in Coq.Numbers.NatInt.NZMulOrder]
b:120 [binder, in Coq.ZArith.Znumtheory]
b:121 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:121 [binder, in Coq.setoid_ring.Field_theory]
b:121 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:121 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:121 [binder, in Coq.Logic.ClassicalFacts]
b:122 [binder, in Coq.ZArith.Zdiv]
b:122 [binder, in Coq.ZArith.Zquot]
b:122 [binder, in Coq.Numbers.NatInt.NZMulOrder]
b:122 [binder, in Coq.Logic.ClassicalFacts]
b:122 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
b:123 [binder, in Coq.Sorting.PermutSetoid]
b:123 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:123 [binder, in Coq.Numbers.NatInt.NZDiv]
b:123 [binder, in Coq.ZArith.Znumtheory]
b:124 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:124 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:124 [binder, in Coq.Numbers.NatInt.NZMulOrder]
b:124 [binder, in Coq.QArith.QArith_base]
b:1241 [binder, in Coq.FSets.FMapAVL]
b:1244 [binder, in Coq.FSets.FMapAVL]
B:125 [binder, in Coq.Vectors.VectorSpec]
b:125 [binder, in Coq.Logic.FunctionalExtensionality]
b:125 [binder, in Coq.ZArith.Zdiv]
b:125 [binder, in Coq.ZArith.Zquot]
b:125 [binder, in Coq.Reals.RiemannInt_SF]
b:126 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:126 [binder, in Coq.Structures.OrderedTypeEx]
B:126 [binder, in Coq.Classes.CMorphisms]
b:126 [binder, in Coq.Numbers.NatInt.NZDiv]
b:126 [binder, in Coq.Numbers.NatInt.NZMulOrder]
b:127 [binder, in Coq.Reals.MVT]
b:127 [binder, in Coq.Logic.FunctionalExtensionality]
b:127 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:127 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:127 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
b:127 [binder, in Coq.ZArith.Znumtheory]
b:128 [binder, in Coq.ZArith.Zdiv]
b:128 [binder, in Coq.ZArith.Zquot]
b:129 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:129 [binder, in Coq.Numbers.NatInt.NZDiv]
b:13 [binder, in Coq.Wellfounded.Inverse_Image]
b:13 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
b:13 [binder, in Coq.ZArith.BinInt]
b:13 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
B:13 [binder, in Coq.Logic.FunctionalExtensionality]
b:13 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
B:13 [binder, in Coq.Logic.Hurkens]
b:13 [binder, in Coq.ZArith.Zdigits]
B:13 [binder, in Coq.Sets.Cpo]
b:13 [binder, in Coq.Strings.Ascii]
b:13 [binder, in Coq.ZArith.Zquot]
B:13 [binder, in Coq.Bool.Sumbool]
B:13 [binder, in Coq.Sets.Powerset_facts]
b:13 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:13 [binder, in Coq.Logic.Diaconescu]
B:13 [binder, in Coq.Init.Logic]
b:130 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:130 [binder, in Coq.ZArith.Zdiv]
b:130 [binder, in Coq.Reals.Rbasic_fun]
b:130 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:130 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
b:130 [binder, in Coq.Reals.RiemannInt_SF]
b:130 [binder, in Coq.ZArith.Znumtheory]
b:131 [binder, in Coq.ZArith.BinIntDef]
b:131 [binder, in Coq.Logic.FunctionalExtensionality]
b:131 [binder, in Coq.Structures.OrderedTypeEx]
B:131 [binder, in Coq.Classes.CMorphisms]
b:131 [binder, in Coq.ZArith.Zquot]
b:131 [binder, in Coq.Logic.ClassicalFacts]
b:131 [binder, in Coq.Relations.Relation_Operators]
b:132 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:132 [binder, in Coq.ZArith.Zdiv]
b:132 [binder, in Coq.Numbers.NatInt.NZDiv]
B:133 [binder, in Coq.Vectors.VectorSpec]
b:133 [binder, in Coq.ZArith.BinIntDef]
b:133 [binder, in Coq.ZArith.BinInt]
b:133 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:133 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:133 [binder, in Coq.Bool.Bool]
b:133 [binder, in Coq.Structures.OrderedTypeEx]
b:133 [binder, in Coq.Reals.Rbasic_fun]
b:133 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:133 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
b:134 [binder, in Coq.Reals.Ranalysis1]
b:134 [binder, in Coq.Reals.MVT]
b:134 [binder, in Coq.ZArith.Zdiv]
b:134 [binder, in Coq.Bool.Bool]
b:135 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:135 [binder, in Coq.Logic.ChoiceFacts]
b:135 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:135 [binder, in Coq.Bool.Bool]
b:135 [binder, in Coq.Structures.OrderedTypeEx]
b:135 [binder, in Coq.Numbers.NatInt.NZDiv]
b:136 [binder, in Coq.Reals.RiemannInt]
b:136 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:136 [binder, in Coq.ZArith.Zdiv]
b:136 [binder, in Coq.Bool.Bool]
b:136 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:136 [binder, in Coq.Logic.ClassicalFacts]
b:136 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
b:136 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:137 [binder, in Coq.ZArith.BinInt]
B:137 [binder, in Coq.Logic.FunctionalExtensionality]
B:137 [binder, in Coq.Logic.ChoiceFacts]
b:137 [binder, in Coq.Bool.Bool]
b:137 [binder, in Coq.Structures.OrderedTypeEx]
b:138 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:138 [binder, in Coq.ZArith.Zdiv]
B:138 [binder, in Coq.Classes.CMorphisms]
B:139 [binder, in Coq.Logic.ChoiceFacts]
b:139 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:139 [binder, in Coq.ZArith.Zquot]
b:139 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:139 [binder, in Coq.Logic.ClassicalFacts]
B:14 [binder, in Coq.Logic.Decidable]
b:14 [binder, in Coq.Wellfounded.Inverse_Image]
b:14 [binder, in Coq.Logic.ConstructiveEpsilon]
b:14 [binder, in Coq.Numbers.Natural.Abstract.NPow]
B:14 [binder, in Coq.Bool.IfProp]
B:14 [binder, in Coq.Logic.JMeq]
b:14 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:14 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:14 [binder, in Coq.ssr.ssrbool]
b:14 [binder, in Coq.ZArith.Zdiv]
b:14 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
b:14 [binder, in Coq.Reals.Abstract.ConstructiveLimits]
B:14 [binder, in Coq.Classes.SetoidDec]
b:14 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:14 [binder, in Coq.Bool.Sumbool]
b:14 [binder, in Coq.Numbers.Integer.Abstract.ZPow]
B:14 [binder, in Coq.Logic.ClassicalFacts]
b:14 [binder, in Coq.ZArith.Znumtheory]
B:14 [binder, in Coq.Bool.DecBool]
B:140 [binder, in Coq.Vectors.VectorSpec]
b:140 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:140 [binder, in Coq.ZArith.Zdiv]
b:140 [binder, in Coq.Structures.OrderedTypeEx]
b:141 [binder, in Coq.ZArith.BinInt]
b:141 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:141 [binder, in Coq.Logic.ChoiceFacts]
b:141 [binder, in Coq.Arith.PeanoNat]
b:141 [binder, in Coq.ZArith.Zquot]
b:141 [binder, in Coq.ZArith.Znumtheory]
b:142 [binder, in Coq.Reals.MVT]
B:142 [binder, in Coq.Logic.FunctionalExtensionality]
b:142 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:142 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:142 [binder, in Coq.ZArith.Zdiv]
B:142 [binder, in Coq.Logic.ClassicalFacts]
b:143 [binder, in Coq.ZArith.BinInt]
b:143 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:143 [binder, in Coq.Reals.RiemannInt]
b:143 [binder, in Coq.Structures.OrderedTypeEx]
b:143 [binder, in Coq.ZArith.Zquot]
B:143 [binder, in Coq.Lists.ListSet]
b:144 [binder, in Coq.Init.Nat]
b:144 [binder, in Coq.Sorting.Permutation]
b:144 [binder, in Coq.ZArith.Zdiv]
b:144 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:144 [binder, in Coq.Relations.Relation_Operators]
B:145 [binder, in Coq.Logic.ChoiceFacts]
b:145 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:145 [binder, in Coq.Arith.PeanoNat]
b:145 [binder, in Coq.ZArith.Zquot]
B:145 [binder, in Coq.Lists.ListSet]
b:146 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:146 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:146 [binder, in Coq.setoid_ring.Field_theory]
b:146 [binder, in Coq.ZArith.Zdiv]
b:146 [binder, in Coq.Structures.OrderedTypeEx]
B:146 [binder, in Coq.Logic.ClassicalFacts]
B:147 [binder, in Coq.Vectors.VectorSpec]
b:147 [binder, in Coq.Reals.RiemannInt]
B:147 [binder, in Coq.Logic.ChoiceFacts]
B:147 [binder, in Coq.Lists.ListSet]
b:147 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:148 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:148 [binder, in Coq.Init.Nat]
b:148 [binder, in Coq.ZArith.Zdiv]
b:148 [binder, in Coq.Reals.RiemannInt_SF]
b:149 [binder, in Coq.ZArith.BinIntDef]
b:149 [binder, in Coq.ZArith.BinInt]
b:149 [binder, in Coq.Reals.MVT]
B:149 [binder, in Coq.Logic.ChoiceFacts]
B:149 [binder, in Coq.Lists.ListSet]
b:15 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:15 [binder, in Coq.Reals.Rtrigo_facts]
B:15 [binder, in Coq.Sets.Ensembles]
b:15 [binder, in Coq.ZArith.BinInt]
B:15 [binder, in Coq.Numbers.NaryFunctions]
b:15 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
B:15 [binder, in Coq.MSets.MSetWeakList]
b:15 [binder, in Coq.QArith.Qfield]
b:15 [binder, in Coq.QArith.Qabs]
b:15 [binder, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
b:15 [binder, in Coq.ZArith.Zgcd_alt]
b:15 [binder, in Coq.ZArith.Zpow_alt]
b:15 [binder, in Coq.ZArith.Zquot]
B:15 [binder, in Coq.Program.Combinators]
b:15 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:15 [binder, in Coq.Logic.Diaconescu]
B:15 [binder, in Coq.Program.Basics]
b:15 [binder, in Coq.QArith.Qpower]
b:150 [binder, in Coq.Init.Nat]
b:150 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:150 [binder, in Coq.Logic.Hurkens]
b:150 [binder, in Coq.Arith.PeanoNat]
B:150 [binder, in Coq.Classes.CMorphisms]
b:150 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:151 [binder, in Coq.ZArith.BinInt]
b:151 [binder, in Coq.ZArith.Zdiv]
b:151 [binder, in Coq.Arith.PeanoNat]
B:152 [binder, in Coq.Logic.ChoiceFacts]
b:152 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:152 [binder, in Coq.Init.Nat]
b:152 [binder, in Coq.Logic.Hurkens]
b:152 [binder, in Coq.Lists.ListSet]
b:153 [binder, in Coq.ZArith.BinIntDef]
b:153 [binder, in Coq.ZArith.BinInt]
b:153 [binder, in Coq.Init.Nat]
b:153 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:153 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:153 [binder, in Coq.Logic.ClassicalFacts]
b:154 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
B:154 [binder, in Coq.Logic.ChoiceFacts]
b:154 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:154 [binder, in Coq.ZArith.Zdiv]
b:154 [binder, in Coq.Bool.Bool]
B:154 [binder, in Coq.Lists.ListSet]
b:154 [binder, in Coq.ZArith.Znumtheory]
B:155 [binder, in Coq.Vectors.VectorSpec]
b:155 [binder, in Coq.ZArith.BinInt]
b:155 [binder, in Coq.Bool.Bool]
B:156 [binder, in Coq.Logic.ChoiceFacts]
b:156 [binder, in Coq.Init.Nat]
b:156 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:156 [binder, in Coq.Bool.Bool]
b:156 [binder, in Coq.Arith.PeanoNat]
b:156 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:157 [binder, in Coq.Reals.MVT]
b:157 [binder, in Coq.NArith.BinNat]
b:157 [binder, in Coq.Reals.Rpower]
b:157 [binder, in Coq.ZArith.Zdiv]
b:157 [binder, in Coq.Bool.Bool]
b:157 [binder, in Coq.Logic.ClassicalFacts]
b:157 [binder, in Coq.Reals.RiemannInt_SF]
b:158 [binder, in Coq.Reals.RiemannInt]
B:158 [binder, in Coq.Logic.ChoiceFacts]
b:158 [binder, in Coq.Bool.Bool]
b:158 [binder, in Coq.Arith.PeanoNat]
b:158 [binder, in Coq.Reals.Rtopology]
b:159 [binder, in Coq.ZArith.BinInt]
b:159 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:159 [binder, in Coq.Bool.Bool]
b:159 [binder, in Coq.MSets.MSetPositive]
b:159 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:16 [binder, in Coq.Logic.Decidable]
b:16 [binder, in Coq.Wellfounded.Inverse_Image]
b:16 [binder, in Coq.Numbers.NatInt.NZPow]
b:16 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:16 [binder, in Coq.Bool.IfProp]
B:16 [binder, in Coq.Classes.RelationPairs]
b:16 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:16 [binder, in Coq.Numbers.Natural.Abstract.NSqrt]
b:16 [binder, in Coq.ssr.ssrbool]
b:16 [binder, in Coq.ZArith.Zdigits]
b:16 [binder, in Coq.ZArith.Zdiv]
B:16 [binder, in Coq.Program.Equality]
B:16 [binder, in Coq.rtauto.Bintree]
B:16 [binder, in Coq.Classes.EquivDec]
b:16 [binder, in Coq.Reals.NewtonInt]
b:16 [binder, in Coq.Numbers.Integer.Abstract.ZPow]
b:16 [binder, in Coq.Reals.R_sqr]
b:16 [binder, in Coq.ZArith.Znumtheory]
b:16 [binder, in Coq.Sets.Powerset]
B:160 [binder, in Coq.Classes.Morphisms]
B:160 [binder, in Coq.Logic.ChoiceFacts]
b:160 [binder, in Coq.Reals.Rpower]
B:160 [binder, in Coq.Logic.ClassicalFacts]
b:161 [binder, in Coq.ZArith.BinInt]
b:161 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:161 [binder, in Coq.NArith.BinNat]
b:161 [binder, in Coq.Bool.Bool]
b:161 [binder, in Coq.Arith.PeanoNat]
b:162 [binder, in Coq.Reals.RiemannInt]
B:162 [binder, in Coq.Logic.ChoiceFacts]
b:162 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:162 [binder, in Coq.ZArith.Zdiv]
b:162 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:162 [binder, in Coq.Logic.ClassicalFacts]
b:162 [binder, in Coq.Reals.RiemannInt_SF]
b:163 [binder, in Coq.ZArith.BinInt]
b:163 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
b:163 [binder, in Coq.Logic.ClassicalFacts]
B:164 [binder, in Coq.Logic.ChoiceFacts]
b:164 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:164 [binder, in Coq.Bool.Bool]
b:164 [binder, in Coq.Arith.PeanoNat]
b:164 [binder, in Coq.ZArith.Znumtheory]
B:165 [binder, in Coq.Vectors.VectorSpec]
b:165 [binder, in Coq.ZArith.BinInt]
b:165 [binder, in Coq.ssr.ssrbool]
b:165 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:165 [binder, in Coq.NArith.BinNat]
b:165 [binder, in Coq.ZArith.Zdiv]
b:165 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:166 [binder, in Coq.Logic.Eqdep_dec]
b:166 [binder, in Coq.ZArith.BinIntDef]
b:166 [binder, in Coq.Reals.RiemannInt]
B:166 [binder, in Coq.Logic.ChoiceFacts]
b:166 [binder, in Coq.ssr.ssrbool]
b:166 [binder, in Coq.Sorting.Permutation]
b:166 [binder, in Coq.Bool.Bool]
b:167 [binder, in Coq.ZArith.BinInt]
b:167 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:167 [binder, in Coq.ssr.ssrbool]
b:167 [binder, in Coq.NArith.BinNat]
b:167 [binder, in Coq.Arith.PeanoNat]
b:168 [binder, in Coq.Vectors.VectorSpec]
b:168 [binder, in Coq.ssr.ssrbool]
b:168 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:168 [binder, in Coq.ZArith.Zdiv]
b:168 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:169 [binder, in Coq.ZArith.BinInt]
b:169 [binder, in Coq.ssr.ssrbool]
b:169 [binder, in Coq.NArith.BinNat]
b:169 [binder, in Coq.Bool.Bool]
b:169 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
B:169 [binder, in Coq.Init.Logic]
b:17 [binder, in Coq.Reals.Runcountable]
b:17 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:17 [binder, in Coq.Bool.IfProp]
b:17 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
b:17 [binder, in Coq.Reals.RiemannInt]
b:17 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:17 [binder, in Coq.Reals.Abstract.ConstructiveAbs]
b:17 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
b:17 [binder, in Coq.ZArith.Zgcd_alt]
b:17 [binder, in Coq.ZArith.Zpow_alt]
b:17 [binder, in Coq.ZArith.Zquot]
b:17 [binder, in Coq.Init.Datatypes]
B:17 [binder, in Coq.Init.Logic]
b:170 [binder, in Coq.ZArith.BinIntDef]
B:170 [binder, in Coq.Classes.Morphisms]
b:170 [binder, in Coq.Reals.RiemannInt]
b:170 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:170 [binder, in Coq.ssr.ssrbool]
b:170 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:170 [binder, in Coq.micromega.ZMicromega]
b:171 [binder, in Coq.ZArith.BinInt]
b:171 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:171 [binder, in Coq.NArith.BinNat]
b:171 [binder, in Coq.ZArith.Zdiv]
b:171 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:171 [binder, in Coq.Reals.RiemannInt_SF]
b:172 [binder, in Coq.ssr.ssrbool]
b:172 [binder, in Coq.Bool.Bool]
b:172 [binder, in Coq.Logic.ClassicalFacts]
b:172 [binder, in Coq.ZArith.Znumtheory]
b:173 [binder, in Coq.FSets.FMapFacts]
b:173 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:173 [binder, in Coq.NArith.BinNat]
b:173 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:173 [binder, in Coq.Reals.RiemannInt_SF]
b:173 [binder, in Coq.QArith.QArith_base]
b:174 [binder, in Coq.ZArith.BinIntDef]
b:174 [binder, in Coq.FSets.FMapFacts]
b:174 [binder, in Coq.ssr.ssrbool]
b:174 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:174 [binder, in Coq.ZArith.Zdiv]
b:175 [binder, in Coq.Reals.RiemannInt]
b:175 [binder, in Coq.Bool.Bool]
b:175 [binder, in Coq.ZArith.Znumtheory]
b:175 [binder, in Coq.micromega.ZMicromega]
B:176 [binder, in Coq.PArith.BinPos]
b:176 [binder, in Coq.Reals.MVT]
b:176 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:176 [binder, in Coq.ssr.ssrbool]
b:176 [binder, in Coq.QArith.QArith_base]
B:177 [binder, in Coq.Classes.Morphisms]
b:177 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:177 [binder, in Coq.ZArith.Zdiv]
b:177 [binder, in Coq.ZArith.Znumtheory]
b:177 [binder, in Coq.micromega.ZMicromega]
b:178 [binder, in Coq.ZArith.BinIntDef]
b:178 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:178 [binder, in Coq.Bool.Bool]
b:178 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:179 [binder, in Coq.ZArith.BinInt]
b:179 [binder, in Coq.Reals.RiemannInt]
b:179 [binder, in Coq.ssr.ssrbool]
b:179 [binder, in Coq.setoid_ring.Ring_theory]
B:18 [binder, in Coq.Logic.Decidable]
b:18 [binder, in Coq.Logic.ConstructiveEpsilon]
b:18 [binder, in Coq.Reals.Rtrigo_facts]
b:18 [binder, in Coq.Numbers.NatInt.NZPow]
b:18 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
b:18 [binder, in Coq.ZArith.Zpow_facts]
b:18 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
b:18 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:18 [binder, in Coq.ZArith.Wf_Z]
b:18 [binder, in Coq.Numbers.Natural.Abstract.NSqrt]
b:18 [binder, in Coq.ssr.ssrbool]
B:18 [binder, in Coq.Logic.Hurkens]
B:18 [binder, in Coq.Sets.Cpo]
B:18 [binder, in Coq.Classes.CMorphisms]
B:18 [binder, in Coq.Program.Combinators]
b:18 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:18 [binder, in Coq.Numbers.Integer.Abstract.ZPow]
b:18 [binder, in Coq.Reals.R_sqr]
b:180 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:180 [binder, in Coq.ZArith.Zdiv]
b:180 [binder, in Coq.Bool.Bool]
b:180 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:180 [binder, in Coq.ZArith.Znumtheory]
b:181 [binder, in Coq.ZArith.BinInt]
b:182 [binder, in Coq.ssr.ssrbool]
b:182 [binder, in Coq.NArith.BinNat]
b:182 [binder, in Coq.Bool.Bool]
B:182 [binder, in Coq.FSets.FMapPositive]
b:183 [binder, in Coq.ZArith.BinInt]
b:183 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:183 [binder, in Coq.ZArith.Zdiv]
b:183 [binder, in Coq.FSets.FSetPositive]
b:183 [binder, in Coq.Reals.RiemannInt_SF]
b:183 [binder, in Coq.ZArith.Znumtheory]
b:184 [binder, in Coq.Reals.RiemannInt]
b:184 [binder, in Coq.ssr.ssrbool]
b:184 [binder, in Coq.NArith.BinNat]
b:184 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:185 [binder, in Coq.ZArith.BinInt]
b:185 [binder, in Coq.Reals.Ranalysis5]
b:185 [binder, in Coq.ZArith.Znumtheory]
b:185 [binder, in Coq.micromega.Tauto]
b:186 [binder, in Coq.ssr.ssrbool]
b:186 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:186 [binder, in Coq.NArith.BinNat]
b:186 [binder, in Coq.ZArith.Zdiv]
b:186 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:187 [binder, in Coq.ZArith.BinInt]
b:187 [binder, in Coq.FSets.FMapFacts]
b:187 [binder, in Coq.Reals.RiemannInt_SF]
b:188 [binder, in Coq.FSets.FMapFacts]
b:188 [binder, in Coq.NArith.BinNat]
b:188 [binder, in Coq.Bool.Bool]
B:188 [binder, in Coq.FSets.FMapPositive]
b:189 [binder, in Coq.ssr.ssrbool]
b:189 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:189 [binder, in Coq.Bool.Bool]
b:189 [binder, in Coq.MSets.MSetRBT]
b:19 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:19 [binder, in Coq.Numbers.Natural.Abstract.NPow]
B:19 [binder, in Coq.Bool.IfProp]
B:19 [binder, in Coq.Classes.Morphisms]
B:19 [binder, in Coq.Logic.ExtensionalityFacts]
b:19 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
b:19 [binder, in Coq.Numbers.NatInt.NZLog]
B:19 [binder, in Coq.Classes.CEquivalence]
B:19 [binder, in Coq.Lists.ListDec]
b:19 [binder, in Coq.Sorting.Sorted]
b:19 [binder, in Coq.Reals.Abstract.ConstructiveLimits]
b:19 [binder, in Coq.FSets.FSetPositive]
b:19 [binder, in Coq.MSets.MSetPositive]
b:19 [binder, in Coq.ZArith.Zquot]
b:19 [binder, in Coq.Init.Datatypes]
b:19 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:19 [binder, in Coq.Reals.Rgeom]
b:19 [binder, in Coq.Reals.RiemannInt_SF]
b:19 [binder, in Coq.Sets.Powerset]
B:19 [binder, in Coq.Classes.Equivalence]
b:190 [binder, in Coq.NArith.BinNat]
b:190 [binder, in Coq.ZArith.Zdiv]
b:190 [binder, in Coq.Bool.Bool]
b:190 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:190 [binder, in Coq.Logic.ClassicalFacts]
B:191 [binder, in Coq.Logic.Hurkens]
B:192 [binder, in Coq.Classes.Morphisms]
b:192 [binder, in Coq.Reals.RiemannInt]
b:192 [binder, in Coq.ssr.ssrbool]
b:192 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:192 [binder, in Coq.Bool.Bool]
b:192 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:193 [binder, in Coq.NArith.BinNat]
b:193 [binder, in Coq.ZArith.Zdiv]
B:193 [binder, in Coq.Classes.CMorphisms]
B:193 [binder, in Coq.Init.Logic]
b:194 [binder, in Coq.Reals.MVT]
b:194 [binder, in Coq.ssr.ssrbool]
B:195 [binder, in Coq.Logic.ChoiceFacts]
b:195 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:195 [binder, in Coq.ZArith.Zdiv]
b:195 [binder, in Coq.MSets.MSetPositive]
b:196 [binder, in Coq.ZArith.BinInt]
b:196 [binder, in Coq.ssr.ssrbool]
b:196 [binder, in Coq.Sorting.Permutation]
B:196 [binder, in Coq.Logic.ClassicalFacts]
B:197 [binder, in Coq.Vectors.VectorDef]
b:198 [binder, in Coq.Reals.Ranalysis1]
b:198 [binder, in Coq.ZArith.BinInt]
b:198 [binder, in Coq.ssr.ssrbool]
b:198 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:199 [binder, in Coq.ZArith.Zdiv]
b:199 [binder, in Coq.MSets.MSetPositive]
b:199 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:2 [binder, in Coq.Wellfounded.Well_Ordering]
B:2 [binder, in Coq.Logic.ExtensionalFunctionRepresentative]
b:2 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
B:2 [binder, in Coq.Sets.Constructive_sets]
b:2 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:2 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:2 [binder, in Coq.Logic.SetoidChoice]
B:2 [binder, in Coq.Bool.IfProp]
B:2 [binder, in Coq.Classes.Morphisms]
B:2 [binder, in Coq.Classes.RelationPairs]
B:2 [binder, in Coq.Logic.ExtensionalityFacts]
B:2 [binder, in Coq.Logic.FunctionalExtensionality]
b:2 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
b:2 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:2 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:2 [binder, in Coq.ssr.ssrbool]
b:2 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:2 [binder, in Coq.Relations.Relations]
B:2 [binder, in Coq.Logic.ClassicalUniqueChoice]
B:2 [binder, in Coq.Logic.RelationalChoice]
b:2 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:2 [binder, in Coq.Strings.Byte]
b:2 [binder, in Coq.Bool.Sumbool]
B:2 [binder, in Coq.Program.Combinators]
b:2 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:2 [binder, in Coq.Numbers.Integer.Abstract.ZPow]
B:2 [binder, in Coq.Logic.PropExtensionalityFacts]
B:2 [binder, in Coq.Program.Basics]
b:2 [binder, in Coq.NArith.Ndiv_def]
b:2 [binder, in Coq.ZArith.Znumtheory]
b:2 [binder, in Coq.Arith.Euclid]
b:2 [binder, in Coq.ZArith.Zeuclid]
b:2 [binder, in Coq.Reals.ClassicalConstructiveReals]
B:2 [binder, in Coq.Logic.FinFun]
B:2 [binder, in Coq.Bool.DecBool]
B:20 [binder, in Coq.Logic.Decidable]
b:20 [binder, in Coq.Reals.Runcountable]
b:20 [binder, in Coq.Numbers.NatInt.NZPow]
b:20 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:20 [binder, in Coq.Bool.IfProp]
B:20 [binder, in Coq.Classes.RelationPairs]
B:20 [binder, in Coq.Logic.FunctionalExtensionality]
b:20 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:20 [binder, in Coq.ssr.ssrbool]
b:20 [binder, in Coq.ZArith.Zdiv]
B:20 [binder, in Coq.Program.Equality]
B:20 [binder, in Coq.rtauto.Bintree]
b:20 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
b:20 [binder, in Coq.ZArith.Zgcd_alt]
B:20 [binder, in Coq.Logic.ClassicalDescription]
b:20 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:20 [binder, in Coq.Numbers.Integer.Abstract.ZAxioms]
b:20 [binder, in Coq.Numbers.Integer.Abstract.ZPow]
B:20 [binder, in Coq.Init.Logic]
b:20 [binder, in Coq.ZArith.Znumtheory]
b:200 [binder, in Coq.ssr.ssrbool]
B:200 [binder, in Coq.Classes.CMorphisms]
b:200 [binder, in Coq.Logic.ClassicalFacts]
b:201 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:201 [binder, in Coq.MSets.MSetPositive]
B:201 [binder, in Coq.Logic.ClassicalFacts]
B:202 [binder, in Coq.Logic.ChoiceFacts]
b:202 [binder, in Coq.ssr.ssrbool]
b:202 [binder, in Coq.ZArith.Zdiv]
b:202 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:202 [binder, in Coq.Init.Logic]
b:203 [binder, in Coq.ssr.ssrbool]
b:203 [binder, in Coq.Bool.Bool]
b:203 [binder, in Coq.MSets.MSetPositive]
b:203 [binder, in Coq.Reals.RiemannInt_SF]
B:204 [binder, in Coq.Logic.ChoiceFacts]
b:204 [binder, in Coq.ssr.ssrbool]
b:204 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:204 [binder, in Coq.ZArith.Zdiv]
b:205 [binder, in Coq.ssr.ssrbool]
b:205 [binder, in Coq.Bool.Bool]
b:205 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:206 [binder, in Coq.Reals.Rfunctions]
b:206 [binder, in Coq.Reals.RiemannInt]
b:206 [binder, in Coq.ssr.ssrbool]
b:206 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:206 [binder, in Coq.Logic.ClassicalFacts]
B:206 [binder, in Coq.Vectors.VectorDef]
b:207 [binder, in Coq.ssr.ssrbool]
b:207 [binder, in Coq.ZArith.Zdiv]
B:207 [binder, in Coq.Classes.CMorphisms]
b:207 [binder, in Coq.MSets.MSetRBT]
b:208 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:209 [binder, in Coq.ssr.ssrbool]
b:209 [binder, in Coq.Reals.RiemannInt_SF]
b:21 [binder, in Coq.Numbers.Natural.Abstract.NPow]
B:21 [binder, in Coq.Sets.Ensembles]
b:21 [binder, in Coq.ZArith.Zpow_facts]
b:21 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
B:21 [binder, in Coq.Logic.ChoiceFacts]
b:21 [binder, in Coq.ssr.ssrbool]
b:21 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:21 [binder, in Coq.Numbers.NatInt.NZLog]
b:21 [binder, in Coq.Logic.ClassicalUniqueChoice]
b:21 [binder, in Coq.ZArith.Zquot]
B:21 [binder, in Coq.Program.Combinators]
B:21 [binder, in Coq.Program.Basics]
b:210 [binder, in Coq.Reals.Rfunctions]
b:210 [binder, in Coq.Reals.RiemannInt]
B:210 [binder, in Coq.Logic.ChoiceFacts]
B:210 [binder, in Coq.Logic.Hurkens]
b:211 [binder, in Coq.ssr.ssrbool]
b:211 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:211 [binder, in Coq.Logic.ClassicalFacts]
B:212 [binder, in Coq.Logic.ChoiceFacts]
b:212 [binder, in Coq.MSets.MSetRBT]
b:212 [binder, in Coq.Vectors.VectorDef]
b:213 [binder, in Coq.ssr.ssrbool]
b:213 [binder, in Coq.Bool.Bool]
B:213 [binder, in Coq.Logic.ClassicalFacts]
b:214 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:214 [binder, in Coq.Init.Logic]
b:215 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:215 [binder, in Coq.ssr.ssrbool]
B:215 [binder, in Coq.Logic.ClassicalFacts]
B:215 [binder, in Coq.Vectors.VectorDef]
b:216 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:216 [binder, in Coq.micromega.ZMicromega]
b:217 [binder, in Coq.ssr.ssrbool]
b:217 [binder, in Coq.ZArith.Zdiv]
B:217 [binder, in Coq.Logic.ClassicalFacts]
b:217 [binder, in Coq.Vectors.VectorDef]
b:218 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:218 [binder, in Coq.Bool.Bool]
b:219 [binder, in Coq.ssr.ssrbool]
b:219 [binder, in Coq.Logic.Hurkens]
b:219 [binder, in Coq.Bool.Bool]
b:219 [binder, in Coq.FSets.FSetPositive]
b:219 [binder, in Coq.Reals.Rtopology]
B:22 [binder, in Coq.Logic.Decidable]
B:22 [binder, in Coq.Sets.Constructive_sets]
b:22 [binder, in Coq.Numbers.NatInt.NZPow]
b:22 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:22 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:22 [binder, in Coq.Numbers.Natural.Abstract.NSqrt]
b:22 [binder, in Coq.ssr.ssrbool]
b:22 [binder, in Coq.ZArith.Zdigits]
b:22 [binder, in Coq.ZArith.Zdiv]
b:22 [binder, in Coq.Sets.Relations_2]
b:22 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:22 [binder, in Coq.Reals.RiemannInt_SF]
b:22 [binder, in Coq.ZArith.Znumtheory]
b:22 [binder, in Coq.QArith.Qpower]
b:22 [binder, in Coq.Sets.Powerset]
b:220 [binder, in Coq.Logic.Hurkens]
b:220 [binder, in Coq.ZArith.Zdiv]
b:220 [binder, in Coq.Bool.Bool]
b:220 [binder, in Coq.micromega.ZMicromega]
b:220 [binder, in Coq.Vectors.VectorDef]
b:221 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:221 [binder, in Coq.ssr.ssrbool]
b:221 [binder, in Coq.Bool.Bool]
b:221 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:222 [binder, in Coq.ZArith.Zdiv]
b:223 [binder, in Coq.ssr.ssrbool]
b:223 [binder, in Coq.FSets.FSetPositive]
B:224 [binder, in Coq.Logic.ChoiceFacts]
b:224 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:224 [binder, in Coq.Logic.ClassicalFacts]
b:224 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:225 [binder, in Coq.ssr.ssrbool]
b:225 [binder, in Coq.ZArith.Zdiv]
b:225 [binder, in Coq.Bool.Bool]
b:225 [binder, in Coq.FSets.FSetPositive]
b:225 [binder, in Coq.Logic.ClassicalFacts]
b:225 [binder, in Coq.Reals.RiemannInt_SF]
b:226 [binder, in Coq.ssr.ssrbool]
B:226 [binder, in Coq.Vectors.VectorDef]
b:227 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:227 [binder, in Coq.ZArith.Zdiv]
B:227 [binder, in Coq.Classes.CMorphisms]
b:227 [binder, in Coq.FSets.FSetPositive]
b:227 [binder, in Coq.Reals.Rtopology]
b:228 [binder, in Coq.ssr.ssrbool]
b:229 [binder, in Coq.ZArith.Zdiv]
B:229 [binder, in Coq.Init.Logic]
b:23 [binder, in Coq.Numbers.Natural.Abstract.NPow]
B:23 [binder, in Coq.Sets.Ensembles]
b:23 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
b:23 [binder, in Coq.Numbers.NatInt.NZLog]
b:23 [binder, in Coq.Logic.ClassicalUniqueChoice]
b:23 [binder, in Coq.Sets.Uniset]
b:23 [binder, in Coq.ZArith.Zquot]
b:23 [binder, in Coq.Numbers.NatInt.NZDiv]
b:23 [binder, in Coq.Numbers.Integer.Abstract.ZAxioms]
b:23 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:23 [binder, in Coq.Init.Logic]
b:230 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:230 [binder, in Coq.ssr.ssrbool]
b:230 [binder, in Coq.Bool.Bool]
b:230 [binder, in Coq.Vectors.VectorDef]
b:231 [binder, in Coq.ZArith.Zdiv]
b:231 [binder, in Coq.Reals.RiemannInt_SF]
b:231 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:232 [binder, in Coq.ssr.ssrbool]
b:232 [binder, in Coq.Bool.Bool]
b:233 [binder, in Coq.Numbers.Natural.Abstract.NBits]
B:233 [binder, in Coq.Logic.ClassicalFacts]
b:234 [binder, in Coq.ZArith.BinInt]
B:234 [binder, in Coq.Logic.ChoiceFacts]
b:234 [binder, in Coq.Bool.Bool]
B:234 [binder, in Coq.Vectors.VectorDef]
B:235 [binder, in Coq.Classes.CMorphisms]
b:235 [binder, in Coq.MSets.MSetRBT]
b:236 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:237 [binder, in Coq.ZArith.BinInt]
b:237 [binder, in Coq.Reals.RiemannInt]
B:237 [binder, in Coq.Logic.Hurkens]
B:238 [binder, in Coq.FSets.FSetBridge]
b:239 [binder, in Coq.ZArith.Zdiv]
b:239 [binder, in Coq.Bool.Bool]
b:239 [binder, in Coq.micromega.Tauto]
b:24 [binder, in Coq.Reals.Runcountable]
b:24 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:24 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:24 [binder, in Coq.Numbers.NaryFunctions]
b:24 [binder, in Coq.Reals.RiemannInt]
b:24 [binder, in Coq.Numbers.Natural.Abstract.NSqrt]
b:24 [binder, in Coq.ssr.ssrbool]
B:24 [binder, in Coq.setoid_ring.Algebra_syntax]
b:24 [binder, in Coq.ZArith.Zdigits]
B:24 [binder, in Coq.Program.Equality]
b:24 [binder, in Coq.Reals.NewtonInt]
b:24 [binder, in Coq.Bool.BoolEq]
b:24 [binder, in Coq.Init.Datatypes]
b:24 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:24 [binder, in Coq.ZArith.Znumtheory]
b:24 [binder, in Coq.Sets.Powerset]
b:240 [binder, in Coq.ZArith.BinInt]
b:240 [binder, in Coq.Vectors.VectorDef]
b:241 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:241 [binder, in Coq.Bool.Bool]
b:242 [binder, in Coq.Reals.RiemannInt]
B:242 [binder, in Coq.Init.Logic]
b:242 [binder, in Coq.Reals.RiemannInt_SF]
B:242 [binder, in Coq.Vectors.VectorDef]
b:243 [binder, in Coq.ZArith.BinInt]
b:243 [binder, in Coq.Bool.Bool]
b:244 [binder, in Coq.Bool.Bool]
b:244 [binder, in Coq.MSets.MSetRBT]
b:245 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:245 [binder, in Coq.Init.Logic]
b:248 [binder, in Coq.ZArith.Zdiv]
b:249 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:249 [binder, in Coq.Reals.Ranalysis5]
B:25 [binder, in Coq.Logic.Decidable]
b:25 [binder, in Coq.Numbers.NatInt.NZPow]
b:25 [binder, in Coq.Numbers.NaryFunctions]
B:25 [binder, in Coq.Logic.ExtensionalityFacts]
B:25 [binder, in Coq.Logic.FunctionalExtensionality]
b:25 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
b:25 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:25 [binder, in Coq.Numbers.NatInt.NZLog]
b:25 [binder, in Coq.ZArith.Zdiv]
b:25 [binder, in Coq.ZArith.Zquot]
B:25 [binder, in Coq.Sets.Powerset_facts]
B:25 [binder, in Coq.Init.Logic]
B:250 [binder, in Coq.Logic.Hurkens]
b:250 [binder, in Coq.ZArith.Zdiv]
b:250 [binder, in Coq.Reals.RiemannInt_SF]
b:251 [binder, in Coq.ZArith.Zdiv]
b:253 [binder, in Coq.MSets.MSetRBT]
b:253 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:254 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:256 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:256 [binder, in Coq.Reals.RiemannInt_SF]
b:258 [binder, in Coq.Reals.RiemannInt]
b:259 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:259 [binder, in Coq.Reals.RiemannInt_SF]
b:26 [binder, in Coq.Sorting.PermutEq]
b:26 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:26 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:26 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:26 [binder, in Coq.ssr.ssrbool]
B:26 [binder, in Coq.Classes.CEquivalence]
b:26 [binder, in Coq.Sorting.Permutation]
b:26 [binder, in Coq.Init.Datatypes]
b:26 [binder, in Coq.Reals.RiemannInt_SF]
b:26 [binder, in Coq.ZArith.Znumtheory]
b:26 [binder, in Coq.Sets.Powerset]
B:26 [binder, in Coq.Classes.Equivalence]
B:262 [binder, in Coq.Logic.Hurkens]
B:262 [binder, in Coq.NArith.BinNat]
b:262 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:263 [binder, in Coq.MSets.MSetRBT]
B:264 [binder, in Coq.Logic.ChoiceFacts]
B:265 [binder, in Coq.Init.Specif]
b:265 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:265 [binder, in Coq.Logic.ClassicalFacts]
b:266 [binder, in Coq.Logic.ClassicalFacts]
b:267 [binder, in Coq.Logic.ChoiceFacts]
b:267 [binder, in Coq.Reals.Ratan]
b:268 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:269 [binder, in Coq.Reals.Ratan]
B:27 [binder, in Coq.Logic.Decidable]
b:27 [binder, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
b:27 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
b:27 [binder, in Coq.Reals.RiemannInt]
b:27 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:27 [binder, in Coq.ZArith.Zdiv]
B:27 [binder, in Coq.Program.Equality]
B:27 [binder, in Coq.Sets.Cpo]
b:27 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
b:27 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]
b:27 [binder, in Coq.ZArith.Zquot]
B:27 [binder, in Coq.Sets.Powerset_facts]
b:27 [binder, in Coq.Numbers.NatInt.NZDiv]
b:27 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:27 [binder, in Coq.Logic.Diaconescu]
b:270 [binder, in Coq.Reals.RiemannInt_SF]
b:271 [binder, in Coq.MSets.MSetRBT]
b:271 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:273 [binder, in Coq.Reals.Ratan]
b:274 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:274 [binder, in Coq.QArith.QArith_base]
b:275 [binder, in Coq.Reals.Rtopology]
b:276 [binder, in Coq.Reals.Ratan]
b:276 [binder, in Coq.Reals.RiemannInt_SF]
b:277 [binder, in Coq.QArith.QArith_base]
b:279 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
B:279 [binder, in Coq.Init.Logic]
B:28 [binder, in Coq.Sets.Constructive_sets]
b:28 [binder, in Coq.Numbers.NatInt.NZPow]
b:28 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:28 [binder, in Coq.Numbers.NaryFunctions]
b:28 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:28 [binder, in Coq.ssr.ssrbool]
B:28 [binder, in Coq.setoid_ring.Algebra_syntax]
b:28 [binder, in Coq.Reals.NewtonInt]
b:28 [binder, in Coq.Init.Datatypes]
b:28 [binder, in Coq.Reals.Ratan]
b:28 [binder, in Coq.Numbers.Integer.Abstract.ZAxioms]
b:28 [binder, in Coq.Logic.Diaconescu]
B:28 [binder, in Coq.Init.Logic]
b:28 [binder, in Coq.Logic.StrictProp]
b:28 [binder, in Coq.Sets.Powerset]
B:280 [binder, in Coq.FSets.FMapPositive]
b:282 [binder, in Coq.Reals.RiemannInt_SF]
b:282 [binder, in Coq.QArith.QArith_base]
b:282 [binder, in Coq.Lists.SetoidList]
b:284 [binder, in Coq.QArith.QArith_base]
b:285 [binder, in Coq.Numbers.Natural.Abstract.NBits]
B:286 [binder, in Coq.Vectors.VectorDef]
b:288 [binder, in Coq.Numbers.Natural.Abstract.NBits]
B:288 [binder, in Coq.Init.Logic]
b:288 [binder, in Coq.Reals.RiemannInt_SF]
b:288 [binder, in Coq.QArith.QArith_base]
b:289 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:29 [binder, in Coq.Logic.Decidable]
b:29 [binder, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
b:29 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:29 [binder, in Coq.Reals.MVT]
b:29 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:29 [binder, in Coq.Numbers.NatInt.NZLog]
b:29 [binder, in Coq.ZArith.Zdiv]
b:29 [binder, in Coq.ZArith.Zquot]
b:29 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:29 [binder, in Coq.Logic.Diaconescu]
b:29 [binder, in Coq.Sorting.Heap]
B:29 [binder, in Coq.Logic.FinFun]
b:291 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:292 [binder, in Coq.FSets.FMapWeakList]
b:292 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:293 [binder, in Coq.Reals.RiemannInt_SF]
b:293 [binder, in Coq.QArith.QArith_base]
b:294 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:294 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:295 [binder, in Coq.QArith.QArith_base]
b:296 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:297 [binder, in Coq.Numbers.Natural.Abstract.NBits]
B:297 [binder, in Coq.Vectors.VectorDef]
b:298 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:298 [binder, in Coq.QArith.QArith_base]
b:299 [binder, in Coq.Reals.RiemannInt_SF]
b:3 [binder, in Coq.Init.Byte]
B:3 [binder, in Coq.Numbers.NaryFunctions]
b:3 [binder, in Coq.FSets.FMapFacts]
B:3 [binder, in Coq.Logic.JMeq]
b:3 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]
b:3 [binder, in Coq.Reals.RiemannInt]
b:3 [binder, in Coq.Numbers.Natural.Abstract.NSqrt]
B:3 [binder, in Coq.Sets.Cpo]
b:3 [binder, in Coq.Reals.NewtonInt]
B:3 [binder, in Coq.Classes.CRelationClasses]
b:3 [binder, in Coq.Numbers.Natural.Abstract.NAxioms]
B:3 [binder, in Coq.Sets.Powerset_Classical_facts]
b:3 [binder, in Coq.Logic.Diaconescu]
B:3 [binder, in Coq.Logic.ClassicalFacts]
B:3 [binder, in Coq.Logic.PropFacts]
b:3 [binder, in Coq.Classes.Init]
b:30 [binder, in Coq.Reals.Runcountable]
b:30 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:30 [binder, in Coq.Logic.ExtensionalityFacts]
b:30 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
B:30 [binder, in Coq.Logic.ChoiceFacts]
b:30 [binder, in Coq.ssr.ssrbool]
b:30 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
b:30 [binder, in Coq.Init.Datatypes]
B:30 [binder, in Coq.Sets.Powerset_facts]
b:30 [binder, in Coq.Logic.Diaconescu]
b:30 [binder, in Coq.ZArith.Znumtheory]
b:300 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:300 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:301 [binder, in Coq.Reals.RiemannInt]
b:302 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:303 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:305 [binder, in Coq.Reals.RiemannInt_SF]
b:306 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:306 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:306 [binder, in Coq.Lists.SetoidList]
b:308 [binder, in Coq.Reals.RiemannInt]
B:309 [binder, in Coq.Init.Logic]
B:31 [binder, in Coq.Logic.Decidable]
b:31 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:31 [binder, in Coq.Numbers.NatInt.NZPow]
b:31 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:31 [binder, in Coq.Numbers.NatInt.NZLog]
b:31 [binder, in Coq.ZArith.Zdiv]
b:31 [binder, in Coq.Bool.Bool]
B:31 [binder, in Coq.Classes.CMorphisms]
b:31 [binder, in Coq.Wellfounded.Lexicographic_Exponentiation]
b:31 [binder, in Coq.ZArith.Zquot]
B:31 [binder, in Coq.Logic.Berardi]
b:31 [binder, in Coq.Reals.Ratan]
b:31 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:31 [binder, in Coq.Numbers.NatInt.NZDiv]
b:31 [binder, in Coq.Numbers.Integer.Abstract.ZAxioms]
b:31 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:31 [binder, in Coq.Logic.Diaconescu]
B:31 [binder, in Coq.Init.Logic]
b:31 [binder, in Coq.Sets.Powerset]
b:311 [binder, in Coq.Reals.RiemannInt]
b:312 [binder, in Coq.Reals.RiemannInt_SF]
b:315 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:316 [binder, in Coq.Reals.RiemannInt_SF]
b:317 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
b:317 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:319 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:32 [binder, in Coq.Reals.Abstract.ConstructiveReals]
b:32 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:32 [binder, in Coq.Numbers.NaryFunctions]
B:32 [binder, in Coq.Logic.FunctionalExtensionality]
b:32 [binder, in Coq.ssr.ssrbool]
b:32 [binder, in Coq.ZArith.Zdiv]
B:32 [binder, in Coq.Lists.ListSet]
b:32 [binder, in Coq.Logic.Diaconescu]
b:32 [binder, in Coq.Reals.RiemannInt_SF]
b:32 [binder, in Coq.Numbers.Natural.Abstract.NGcd]
b:32 [binder, in Coq.ZArith.Znumtheory]
b:321 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:322 [binder, in Coq.Reals.RIneq]
b:323 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:324 [binder, in Coq.Reals.RiemannInt_SF]
b:324 [binder, in Coq.micromega.ZMicromega]
b:325 [binder, in Coq.Numbers.Natural.Abstract.NBits]
B:326 [binder, in Coq.FSets.FMapPositive]
b:327 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:329 [binder, in Coq.Numbers.Natural.Abstract.NBits]
B:33 [binder, in Coq.Logic.Decidable]
b:33 [binder, in Coq.Numbers.NatInt.NZPow]
b:33 [binder, in Coq.Numbers.NaryFunctions]
b:33 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
b:33 [binder, in Coq.Numbers.NatInt.NZLog]
b:33 [binder, in Coq.Bool.Bool]
b:33 [binder, in Coq.ZArith.Zgcd_alt]
b:33 [binder, in Coq.ZArith.Zquot]
B:33 [binder, in Coq.Sets.Powerset_facts]
B:33 [binder, in Coq.Logic.FinFun]
b:331 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:331 [binder, in Coq.Reals.RiemannInt_SF]
b:332 [binder, in Coq.Reals.RiemannInt]
b:333 [binder, in Coq.Numbers.Natural.Abstract.NBits]
B:333 [binder, in Coq.FSets.FMapPositive]
b:335 [binder, in Coq.Logic.ChoiceFacts]
b:335 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:336 [binder, in Coq.Logic.ChoiceFacts]
b:337 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
b:337 [binder, in Coq.Logic.ChoiceFacts]
b:338 [binder, in Coq.Logic.ChoiceFacts]
b:338 [binder, in Coq.Reals.RiemannInt_SF]
b:34 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:34 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:34 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:34 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
B:34 [binder, in Coq.Classes.CEquivalence]
b:34 [binder, in Coq.Reals.NewtonInt]
b:34 [binder, in Coq.Numbers.Integer.Abstract.ZAxioms]
B:34 [binder, in Coq.Init.Logic]
b:34 [binder, in Coq.btauto.Reflect]
b:34 [binder, in Coq.Sets.Powerset]
B:34 [binder, in Coq.Classes.Equivalence]
b:340 [binder, in Coq.Reals.Abstract.ConstructiveReals]
b:341 [binder, in Coq.Reals.RiemannInt]
b:341 [binder, in Coq.Numbers.Natural.Abstract.NBits]
B:343 [binder, in Coq.FSets.FMapFacts]
b:343 [binder, in Coq.Reals.RiemannInt_SF]
b:344 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:345 [binder, in Coq.Lists.List]
b:346 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:347 [binder, in Coq.Init.Logic]
b:348 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:348 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:35 [binder, in Coq.Logic.Decidable]
B:35 [binder, in Coq.setoid_ring.Ncring_initial]
B:35 [binder, in Coq.Sets.Constructive_sets]
b:35 [binder, in Coq.Numbers.NatInt.NZPow]
B:35 [binder, in Coq.Classes.Morphisms]
b:35 [binder, in Coq.Bool.Bool]
B:35 [binder, in Coq.Program.Equality]
b:35 [binder, in Coq.Numbers.NatInt.NZBits]
b:35 [binder, in Coq.Sets.Relations_2_facts]
b:35 [binder, in Coq.ZArith.Zquot]
B:35 [binder, in Coq.Logic.ClassicalDescription]
b:35 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:35 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:35 [binder, in Coq.ZArith.Znumtheory]
b:350 [binder, in Coq.Numbers.Natural.Abstract.NBits]
B:351 [binder, in Coq.Init.Logic]
b:351 [binder, in Coq.Reals.RiemannInt_SF]
b:352 [binder, in Coq.MSets.MSetRBT]
b:352 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:353 [binder, in Coq.FSets.FMapFacts]
b:353 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:354 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:355 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:356 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:356 [binder, in Coq.Reals.Ratan]
b:357 [binder, in Coq.FSets.FMapFacts]
b:358 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:358 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:358 [binder, in Coq.Reals.RiemannInt_SF]
b:359 [binder, in Coq.Reals.Ratan]
B:359 [binder, in Coq.Init.Logic]
b:36 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:36 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:36 [binder, in Coq.Logic.ExtensionalityFacts]
b:36 [binder, in Coq.Numbers.NatInt.NZLog]
b:36 [binder, in Coq.ZArith.Zgcd_alt]
B:36 [binder, in Coq.Sets.Powerset_facts]
b:36 [binder, in Coq.Numbers.NatInt.NZDiv]
b:360 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:361 [binder, in Coq.FSets.FMapFacts]
b:361 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:362 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:362 [binder, in Coq.MSets.MSetRBT]
b:362 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:363 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:363 [binder, in Coq.Reals.RiemannInt_SF]
b:364 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:364 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:366 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:366 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:368 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:369 [binder, in Coq.Numbers.Natural.Abstract.NBits]
B:37 [binder, in Coq.Logic.Decidable]
b:37 [binder, in Coq.Reals.Runcountable]
b:37 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:37 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:37 [binder, in Coq.Reals.RiemannInt]
B:37 [binder, in Coq.ssr.ssrbool]
b:37 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:37 [binder, in Coq.Bool.Bool]
B:37 [binder, in Coq.Classes.SetoidDec]
b:37 [binder, in Coq.ZArith.Zquot]
b:37 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:37 [binder, in Coq.Numbers.Integer.Abstract.ZAxioms]
b:37 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:37 [binder, in Coq.Init.Logic]
b:37 [binder, in Coq.ZArith.Znumtheory]
b:371 [binder, in Coq.Reals.RiemannInt_SF]
b:372 [binder, in Coq.Numbers.Natural.Abstract.NBits]
B:376 [binder, in Coq.Lists.List]
B:376 [binder, in Coq.FSets.FMapWeakList]
b:378 [binder, in Coq.Reals.RiemannInt_SF]
b:379 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:38 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:38 [binder, in Coq.Numbers.NatInt.NZPow]
b:38 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:38 [binder, in Coq.Logic.ClassicalEpsilon]
B:38 [binder, in Coq.Numbers.NaryFunctions]
B:38 [binder, in Coq.Classes.CEquivalence]
b:38 [binder, in Coq.ZArith.Zdiv]
b:38 [binder, in Coq.Reals.Abstract.ConstructiveLimits]
b:38 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
B:38 [binder, in Coq.Lists.ListSet]
b:38 [binder, in Coq.Numbers.NatInt.NZDiv]
b:38 [binder, in Coq.Reals.R_sqr]
B:38 [binder, in Coq.Logic.FinFun]
B:38 [binder, in Coq.rtauto.Rtauto]
B:38 [binder, in Coq.Classes.Equivalence]
B:380 [binder, in Coq.Lists.List]
b:380 [binder, in Coq.Reals.RiemannInt]
b:381 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:383 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:385 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:385 [binder, in Coq.Init.Logic]
b:387 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:389 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:39 [binder, in Coq.Logic.Decidable]
B:39 [binder, in Coq.Sets.Ensembles]
B:39 [binder, in Coq.Logic.FunctionalExtensionality]
b:39 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:39 [binder, in Coq.Numbers.NatInt.NZBits]
b:39 [binder, in Coq.ZArith.Zgcd_alt]
B:39 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]
b:39 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:39 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:39 [binder, in Coq.Reals.RiemannInt_SF]
B:391 [binder, in Coq.Logic.ChoiceFacts]
b:391 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:393 [binder, in Coq.Lists.List]
B:393 [binder, in Coq.Logic.ChoiceFacts]
b:393 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:395 [binder, in Coq.Logic.ChoiceFacts]
b:395 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:397 [binder, in Coq.Logic.ChoiceFacts]
b:397 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:399 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:4 [binder, in Coq.Logic.Decidable]
b:4 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
B:4 [binder, in Coq.Sets.Ensembles]
b:4 [binder, in Coq.Reals.MVT]
b:4 [binder, in Coq.Arith.Wf_nat]
b:4 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
b:4 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:4 [binder, in Coq.ssr.ssrbool]
b:4 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:4 [binder, in Coq.ZArith.Zgcd_alt]
B:4 [binder, in Coq.Logic.Berardi]
b:4 [binder, in Coq.Bool.Sumbool]
b:4 [binder, in Coq.Numbers.NatInt.NZDiv]
b:4 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:4 [binder, in Coq.Numbers.Integer.Abstract.ZPow]
b:4 [binder, in Coq.NArith.Ndiv_def]
b:4 [binder, in Coq.ZArith.Zeuclid]
b:40 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:40 [binder, in Coq.Numbers.NaryFunctions]
b:40 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:40 [binder, in Coq.Numbers.NatInt.NZLog]
b:40 [binder, in Coq.ZArith.Zquot]
B:40 [binder, in Coq.Init.Logic]
b:40 [binder, in Coq.Reals.R_sqr]
B:400 [binder, in Coq.Lists.List]
b:405 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:406 [binder, in Coq.Lists.List]
b:408 [binder, in Coq.FSets.FMapFacts]
b:409 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:41 [binder, in Coq.Logic.Decidable]
b:41 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:41 [binder, in Coq.Numbers.NatInt.NZPow]
B:41 [binder, in Coq.Classes.RelationPairs]
B:41 [binder, in Coq.ssr.ssrbool]
b:41 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:41 [binder, in Coq.Program.Equality]
B:41 [binder, in Coq.Init.Datatypes]
b:41 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:41 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:410 [binder, in Coq.FSets.FMapFacts]
b:410 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
B:411 [binder, in Coq.Logic.ChoiceFacts]
B:412 [binder, in Coq.Lists.List]
B:413 [binder, in Coq.Logic.ChoiceFacts]
b:413 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:415 [binder, in Coq.Logic.ChoiceFacts]
B:417 [binder, in Coq.Logic.ChoiceFacts]
b:417 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:418 [binder, in Coq.Lists.List]
b:419 [binder, in Coq.Reals.RiemannInt]
b:419 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:42 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
B:42 [binder, in Coq.Sets.Ensembles]
b:42 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:42 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:42 [binder, in Coq.Numbers.NatInt.NZLog]
B:42 [binder, in Coq.Classes.CEquivalence]
B:42 [binder, in Coq.Classes.EquivDec]
b:42 [binder, in Coq.ZArith.Zgcd_alt]
b:42 [binder, in Coq.Numbers.Natural.Abstract.NGcd]
b:42 [binder, in Coq.ZArith.Znumtheory]
b:42 [binder, in Coq.NArith.Ndec]
B:42 [binder, in Coq.Logic.FinFun]
B:42 [binder, in Coq.rtauto.Rtauto]
B:42 [binder, in Coq.Classes.Equivalence]
b:421 [binder, in Coq.Logic.ChoiceFacts]
b:422 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:423 [binder, in Coq.Logic.ChoiceFacts]
B:424 [binder, in Coq.Lists.List]
b:424 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:425 [binder, in Coq.Reals.RiemannInt]
B:425 [binder, in Coq.Init.Logic]
b:427 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:43 [binder, in Coq.Logic.Decidable]
b:43 [binder, in Coq.Numbers.NatInt.NZPow]
b:43 [binder, in Coq.Numbers.Integer.Abstract.ZGcd]
b:43 [binder, in Coq.Reals.MVT]
b:43 [binder, in Coq.ZArith.Zdiv]
b:43 [binder, in Coq.Numbers.NatInt.NZBits]
b:43 [binder, in Coq.ZArith.Zquot]
b:43 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:43 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:43 [binder, in Coq.Init.Logic]
b:430 [binder, in Coq.Reals.RiemannInt]
b:430 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:431 [binder, in Coq.Init.Logic]
b:432 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:434 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:437 [binder, in Coq.Reals.Ranalysis1]
b:437 [binder, in Coq.Reals.RiemannInt]
b:437 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
b:44 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
B:44 [binder, in Coq.Sets.Ensembles]
b:44 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:44 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
B:44 [binder, in Coq.MSets.MSetList]
b:44 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:44 [binder, in Coq.ZArith.Zdigits]
B:44 [binder, in Coq.Classes.CMorphisms]
b:44 [binder, in Coq.Reals.Ratan]
b:44 [binder, in Coq.Reals.RiemannInt_SF]
b:44 [binder, in Coq.NArith.Ndec]
b:443 [binder, in Coq.Reals.Ranalysis1]
b:444 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
b:444 [binder, in Coq.Reals.RiemannInt]
B:444 [binder, in Coq.FSets.FMapList]
b:45 [binder, in Coq.Numbers.Natural.Abstract.NPow]
B:45 [binder, in Coq.ssr.ssrbool]
b:45 [binder, in Coq.Numbers.NatInt.NZLog]
B:45 [binder, in Coq.Sets.Powerset_facts]
b:45 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:45 [binder, in Coq.ZArith.Znumtheory]
b:451 [binder, in Coq.Reals.Ranalysis1]
b:452 [binder, in Coq.Reals.RiemannInt]
b:456 [binder, in Coq.Reals.RiemannInt]
b:459 [binder, in Coq.FSets.FMapFacts]
b:46 [binder, in Coq.Reals.Runcountable]
b:46 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:46 [binder, in Coq.Numbers.NatInt.NZPow]
B:46 [binder, in Coq.Logic.FunctionalExtensionality]
b:46 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:46 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:46 [binder, in Coq.Classes.CEquivalence]
b:46 [binder, in Coq.Bool.Bool]
b:46 [binder, in Coq.ZArith.Zquot]
B:46 [binder, in Coq.Init.Datatypes]
b:46 [binder, in Coq.Numbers.NatInt.NZDiv]
B:46 [binder, in Coq.Init.Logic]
B:46 [binder, in Coq.micromega.Tauto]
b:46 [binder, in Coq.NArith.Ndec]
B:46 [binder, in Coq.Structures.OrdersFacts]
B:46 [binder, in Coq.Classes.Equivalence]
b:460 [binder, in Coq.Reals.RiemannInt]
B:461 [binder, in Coq.Lists.List]
b:462 [binder, in Coq.Reals.RIneq]
b:464 [binder, in Coq.FSets.FMapFacts]
b:464 [binder, in Coq.Reals.RiemannInt]
B:467 [binder, in Coq.Lists.List]
b:47 [binder, in Coq.Numbers.NatInt.NZLog]
b:47 [binder, in Coq.Bool.Bool]
b:47 [binder, in Coq.Numbers.NatInt.NZBits]
b:47 [binder, in Coq.ZArith.Zgcd_alt]
b:47 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]
b:47 [binder, in Coq.Reals.Ratan]
b:47 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:47 [binder, in Coq.Reals.RiemannInt_SF]
B:47 [binder, in Coq.Logic.FinFun]
b:47 [binder, in Coq.Structures.OrdersFacts]
B:47 [binder, in Coq.rtauto.Rtauto]
b:472 [binder, in Coq.Reals.RIneq]
b:48 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:48 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:48 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:48 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:48 [binder, in Coq.Logic.Hurkens]
b:48 [binder, in Coq.Bool.Bool]
B:48 [binder, in Coq.Program.Equality]
b:48 [binder, in Coq.Vectors.Fin]
b:48 [binder, in Coq.Sorting.CPermutation]
B:48 [binder, in Coq.Sets.Powerset_facts]
b:48 [binder, in Coq.Numbers.NatInt.NZDiv]
b:48 [binder, in Coq.ZArith.Znumtheory]
b:48 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
B:482 [binder, in Coq.Lists.List]
b:49 [binder, in Coq.Numbers.NatInt.NZPow]
B:49 [binder, in Coq.Sets.Ensembles]
B:49 [binder, in Coq.Logic.JMeq]
b:49 [binder, in Coq.ZArith.Zeven]
b:49 [binder, in Coq.ZArith.Zdiv]
B:49 [binder, in Coq.Classes.CMorphisms]
b:49 [binder, in Coq.Strings.Ascii]
b:49 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]
b:49 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:49 [binder, in Coq.Init.Logic]
b:49 [binder, in Coq.NArith.Ndec]
b:493 [binder, in Coq.FSets.FMapFacts]
b:496 [binder, in Coq.FSets.FMapFacts]
b:499 [binder, in Coq.Reals.RiemannInt]
b:5 [binder, in Coq.Init.Byte]
b:5 [binder, in Coq.Bool.BoolOrder]
b:5 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:5 [binder, in Coq.Numbers.NatInt.NZPow]
b:5 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:5 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:5 [binder, in Coq.ssr.ssrbool]
b:5 [binder, in Coq.Bool.Bool]
B:5 [binder, in Coq.Classes.CRelationClasses]
b:5 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:5 [binder, in Coq.Program.Combinators]
b:5 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:50 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
B:50 [binder, in Coq.Numbers.NaryFunctions]
b:50 [binder, in Coq.Lists.List]
b:50 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
B:50 [binder, in Coq.Logic.ChoiceFacts]
b:50 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:50 [binder, in Coq.Bool.Bool]
b:50 [binder, in Coq.ZArith.Zgcd_alt]
b:50 [binder, in Coq.ZArith.Zquot]
b:50 [binder, in Coq.Logic.Berardi]
B:50 [binder, in Coq.Init.Datatypes]
b:50 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:50 [binder, in Coq.Numbers.NatInt.NZDiv]
b:501 [binder, in Coq.FSets.FMapFacts]
b:504 [binder, in Coq.FSets.FMapFacts]
B:505 [binder, in Coq.Init.Specif]
b:506 [binder, in Coq.Reals.RiemannInt]
b:51 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:51 [binder, in Coq.ZArith.Zeven]
b:51 [binder, in Coq.Bool.Bool]
b:51 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]
b:51 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:51 [binder, in Coq.Vectors.VectorDef]
b:51 [binder, in Coq.NArith.Ndec]
b:513 [binder, in Coq.Reals.RiemannInt]
b:52 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:52 [binder, in Coq.Reals.R_sqrt]
b:52 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:52 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:52 [binder, in Coq.Bool.Bool]
B:52 [binder, in Coq.Classes.EquivDec]
b:52 [binder, in Coq.Reals.NewtonInt]
b:52 [binder, in Coq.Sorting.CPermutation]
b:52 [binder, in Coq.Numbers.NatInt.NZDiv]
B:52 [binder, in Coq.Init.Logic]
b:52 [binder, in Coq.Reals.RiemannInt_SF]
b:52 [binder, in Coq.Sorting.Heap]
b:528 [binder, in Coq.Reals.RiemannInt]
b:53 [binder, in Coq.Reals.Ranalysis2]
b:53 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:53 [binder, in Coq.Numbers.NatInt.NZPow]
B:53 [binder, in Coq.Sets.Ensembles]
B:53 [binder, in Coq.Logic.JMeq]
B:53 [binder, in Coq.Logic.FunctionalExtensionality]
b:53 [binder, in Coq.ZArith.Zeven]
b:53 [binder, in Coq.ZArith.Zdiv]
b:53 [binder, in Coq.ZArith.Zgcd_alt]
b:53 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]
b:53 [binder, in Coq.Lists.ListSet]
b:53 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:534 [binder, in Coq.Reals.RiemannInt]
b:54 [binder, in Coq.Reals.Runcountable]
b:54 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:54 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:54 [binder, in Coq.Lists.List]
b:54 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:54 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
B:54 [binder, in Coq.Logic.Hurkens]
b:54 [binder, in Coq.Bool.Bool]
b:54 [binder, in Coq.ZArith.Zquot]
B:54 [binder, in Coq.Init.Datatypes]
b:54 [binder, in Coq.Numbers.NatInt.NZDiv]
B:54 [binder, in Coq.Init.Logic]
b:54 [binder, in Coq.ZArith.Znumtheory]
b:54 [binder, in Coq.NArith.Ndec]
b:543 [binder, in Coq.Reals.RiemannInt]
b:546 [binder, in Coq.Reals.RiemannInt]
b:549 [binder, in Coq.Reals.RiemannInt]
b:55 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
B:55 [binder, in Coq.Sets.Ensembles]
b:55 [binder, in Coq.Reals.RiemannInt]
b:55 [binder, in Coq.Numbers.NatInt.NZLog]
b:55 [binder, in Coq.ZArith.Zeven]
b:55 [binder, in Coq.ZArith.Zgcd_alt]
b:55 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:55 [binder, in Coq.Reals.RiemannInt_SF]
b:555 [binder, in Coq.Reals.RiemannInt]
b:559 [binder, in Coq.Reals.RiemannInt]
b:56 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:56 [binder, in Coq.Reals.R_sqrt]
B:56 [binder, in Coq.Logic.FunctionalExtensionality]
b:56 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:56 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
b:56 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:56 [binder, in Coq.Lists.ListSet]
b:56 [binder, in Coq.Numbers.NatInt.NZDiv]
b:57 [binder, in Coq.Reals.Ranalysis2]
b:57 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:57 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:57 [binder, in Coq.Numbers.NatInt.NZPow]
b:57 [binder, in Coq.ZArith.Zeven]
b:57 [binder, in Coq.ZArith.Zdiv]
b:57 [binder, in Coq.Bool.Bool]
B:57 [binder, in Coq.Classes.CMorphisms]
b:57 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:57 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:57 [binder, in Coq.NArith.BinNatDef]
B:57 [binder, in Coq.Init.Logic]
b:57 [binder, in Coq.NArith.Ndec]
b:571 [binder, in Coq.Reals.RiemannInt]
b:578 [binder, in Coq.Reals.RiemannInt]
B:58 [binder, in Coq.Sets.Ensembles]
B:58 [binder, in Coq.Logic.JMeq]
b:58 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
b:58 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:58 [binder, in Coq.Bool.Bool]
b:58 [binder, in Coq.Sorting.CPermutation]
b:58 [binder, in Coq.ZArith.Zquot]
B:58 [binder, in Coq.Sets.Powerset_facts]
b:58 [binder, in Coq.Numbers.NatInt.NZDiv]
B:58 [binder, in Coq.Logic.FinFun]
b:580 [binder, in Coq.PArith.BinPos]
b:582 [binder, in Coq.PArith.BinPos]
b:585 [binder, in Coq.PArith.BinPos]
b:587 [binder, in Coq.PArith.BinPos]
b:589 [binder, in Coq.PArith.BinPos]
b:59 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:59 [binder, in Coq.Reals.Rfunctions]
b:59 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:59 [binder, in Coq.Numbers.NaryFunctions]
b:59 [binder, in Coq.Reals.R_sqrt]
b:59 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:59 [binder, in Coq.MSets.MSetAVL]
b:59 [binder, in Coq.ZArith.Zeven]
b:59 [binder, in Coq.Reals.Raxioms]
b:59 [binder, in Coq.Lists.ListSet]
b:59 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:59 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:59 [binder, in Coq.Logic.ClassicalFacts]
b:59 [binder, in Coq.Vectors.VectorDef]
b:591 [binder, in Coq.PArith.BinPos]
b:594 [binder, in Coq.PArith.BinPos]
b:597 [binder, in Coq.PArith.BinPos]
b:598 [binder, in Coq.Reals.RIneq]
B:6 [binder, in Coq.Logic.Decidable]
b:6 [binder, in Coq.Bool.BoolOrder]
b:6 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:6 [binder, in Coq.Bool.IfProp]
b:6 [binder, in Coq.Arith.Wf_nat]
b:6 [binder, in Coq.Logic.ExtensionalityFacts]
b:6 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:6 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
b:6 [binder, in Coq.Numbers.Natural.Abstract.NSqrt]
B:6 [binder, in Coq.Program.Subset]
b:6 [binder, in Coq.ssr.ssrbool]
b:6 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:6 [binder, in Coq.Reals.Machin]
b:6 [binder, in Coq.ZArith.Zdiv]
b:6 [binder, in Coq.Bool.Bool]
b:6 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
b:6 [binder, in Coq.Numbers.NatInt.NZSqrt]
B:6 [binder, in Coq.Logic.Diaconescu]
b:6 [binder, in Coq.Numbers.Integer.Abstract.ZPow]
b:6 [binder, in Coq.ZArith.Znumtheory]
B:6 [binder, in Coq.Logic.PropFacts]
b:6 [binder, in Coq.ZArith.Zeuclid]
b:60 [binder, in Coq.Reals.Runcountable]
b:60 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:60 [binder, in Coq.Numbers.NatInt.NZPow]
b:60 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:60 [binder, in Coq.ZArith.Zquot]
B:60 [binder, in Coq.Init.Datatypes]
b:60 [binder, in Coq.Numbers.NatInt.NZDiv]
B:60 [binder, in Coq.Init.Logic]
b:60 [binder, in Coq.Logic.ClassicalFacts]
b:60 [binder, in Coq.ZArith.Znumtheory]
b:60 [binder, in Coq.NArith.Ndec]
b:600 [binder, in Coq.PArith.BinPos]
b:600 [binder, in Coq.Reals.RIneq]
b:603 [binder, in Coq.Reals.RIneq]
b:61 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:61 [binder, in Coq.Reals.MVT]
b:61 [binder, in Coq.setoid_ring.Field_theory]
b:61 [binder, in Coq.ZArith.Zeven]
b:61 [binder, in Coq.ZArith.Zdiv]
b:61 [binder, in Coq.Reals.NewtonInt]
b:61 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:61 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:61 [binder, in Coq.Logic.ClassicalFacts]
b:62 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:62 [binder, in Coq.Reals.R_sqrt]
b:62 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:62 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:62 [binder, in Coq.Numbers.NatInt.NZLog]
b:62 [binder, in Coq.MSets.MSetAVL]
b:62 [binder, in Coq.Arith.PeanoNat]
b:62 [binder, in Coq.ZArith.Zquot]
b:62 [binder, in Coq.Lists.ListSet]
b:62 [binder, in Coq.Numbers.NatInt.NZDiv]
b:62 [binder, in Coq.Logic.ClassicalFacts]
b:62 [binder, in Coq.QArith.QArith_base]
b:63 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:63 [binder, in Coq.Numbers.NatInt.NZPow]
b:63 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:63 [binder, in Coq.Init.Datatypes]
b:63 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:63 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:63 [binder, in Coq.Init.Logic]
b:63 [binder, in Coq.Logic.ClassicalFacts]
b:63 [binder, in Coq.Reals.RiemannInt_SF]
b:63 [binder, in Coq.ZArith.Znumtheory]
b:63 [binder, in Coq.NArith.Ndec]
b:64 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:64 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:64 [binder, in Coq.Reals.RiemannInt]
b:64 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:64 [binder, in Coq.Vectors.Fin]
b:64 [binder, in Coq.Numbers.NatInt.NZDiv]
b:65 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
B:65 [binder, in Coq.Sorting.PermutSetoid]
b:65 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:65 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:65 [binder, in Coq.Reals.R_sqrt]
b:65 [binder, in Coq.setoid_ring.Field_theory]
b:65 [binder, in Coq.Arith.PeanoNat]
b:65 [binder, in Coq.ZArith.Zquot]
b:65 [binder, in Coq.Lists.ListSet]
b:65 [binder, in Coq.Numbers.NatInt.NZSqrt]
B:65 [binder, in Coq.Init.Logic]
b:65 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:65 [binder, in Coq.NArith.Ndec]
B:650 [binder, in Coq.MSets.MSetRBT]
B:653 [binder, in Coq.MSets.MSetRBT]
B:656 [binder, in Coq.MSets.MSetRBT]
B:658 [binder, in Coq.Init.Specif]
b:66 [binder, in Coq.Sorting.PermutSetoid]
b:66 [binder, in Coq.Numbers.NatInt.NZPow]
b:66 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:66 [binder, in Coq.Numbers.NatInt.NZLog]
b:66 [binder, in Coq.Bool.Bool]
b:66 [binder, in Coq.Reals.RiemannInt_SF]
b:67 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:67 [binder, in Coq.Vectors.Fin]
b:67 [binder, in Coq.ZArith.Zquot]
B:67 [binder, in Coq.Init.Datatypes]
b:67 [binder, in Coq.Numbers.NatInt.NZDiv]
b:67 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:67 [binder, in Coq.Reals.R_sqr]
b:67 [binder, in Coq.ZArith.Znumtheory]
b:67 [binder, in Coq.NArith.Ndec]
b:68 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
b:68 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:68 [binder, in Coq.Reals.MVT]
b:68 [binder, in Coq.Reals.R_sqrt]
b:68 [binder, in Coq.Lists.List]
b:68 [binder, in Coq.Init.Specif]
b:68 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:68 [binder, in Coq.Numbers.NatInt.NZLog]
B:68 [binder, in Coq.Classes.CMorphisms]
b:68 [binder, in Coq.NArith.BinNatDef]
B:68 [binder, in Coq.Init.Logic]
B:680 [binder, in Coq.Init.Specif]
B:684 [binder, in Coq.Init.Specif]
b:688 [binder, in Coq.MSets.MSetRBT]
b:69 [binder, in Coq.Numbers.NatInt.NZPow]
b:69 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:69 [binder, in Coq.Numbers.NaryFunctions]
b:69 [binder, in Coq.Reals.NewtonInt]
b:69 [binder, in Coq.ZArith.Zquot]
b:69 [binder, in Coq.Numbers.NatInt.NZDiv]
b:69 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:69 [binder, in Coq.Reals.RiemannInt_SF]
b:69 [binder, in Coq.NArith.Ndec]
B:691 [binder, in Coq.Lists.List]
b:7 [binder, in Coq.Init.Byte]
b:7 [binder, in Coq.Bool.BoolOrder]
b:7 [binder, in Coq.Reals.Runcountable]
b:7 [binder, in Coq.Bool.IfProp]
B:7 [binder, in Coq.Numbers.NaryFunctions]
b:7 [binder, in Coq.ZArith.Zpow_facts]
B:7 [binder, in Coq.Logic.FunctionalExtensionality]
b:7 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
b:7 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:7 [binder, in Coq.ssr.ssrbool]
B:7 [binder, in Coq.Logic.Hurkens]
B:7 [binder, in Coq.Numbers.Cyclic.Abstract.DoubleType]
b:7 [binder, in Coq.Bool.Bool]
b:7 [binder, in Coq.Sorting.Sorted]
b:7 [binder, in Coq.Reals.NewtonInt]
b:7 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
b:7 [binder, in Coq.Strings.Ascii]
b:7 [binder, in Coq.ZArith.Zquot]
b:7 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:7 [binder, in Coq.Sets.Powerset_facts]
b:7 [binder, in Coq.Numbers.NatInt.NZDiv]
B:7 [binder, in Coq.Init.Logic]
B:7 [binder, in Coq.Logic.FinFun]
b:70 [binder, in Coq.setoid_ring.Field_theory]
b:70 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:70 [binder, in Coq.Numbers.NatInt.NZLog]
b:70 [binder, in Coq.Vectors.Fin]
b:70 [binder, in Coq.Lists.ListSet]
b:70 [binder, in Coq.Numbers.NatInt.NZSqrt]
B:70 [binder, in Coq.Init.Logic]
b:70 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:71 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:71 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:71 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:71 [binder, in Coq.Vectors.Fin]
b:71 [binder, in Coq.ZArith.Zquot]
b:71 [binder, in Coq.Numbers.NatInt.NZDiv]
b:71 [binder, in Coq.ZArith.Znumtheory]
b:71 [binder, in Coq.NArith.Ndec]
b:71 [binder, in Coq.Sorting.Heap]
b:72 [binder, in Coq.Numbers.NatInt.NZPow]
b:72 [binder, in Coq.Reals.R_sqrt]
b:72 [binder, in Coq.Init.Wf]
b:72 [binder, in Coq.setoid_ring.Field_theory]
b:72 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:72 [binder, in Coq.Numbers.NatInt.NZLog]
b:72 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:72 [binder, in Coq.NArith.BinNatDef]
b:73 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:73 [binder, in Coq.Bool.Bool]
b:73 [binder, in Coq.Vectors.Fin]
b:73 [binder, in Coq.ZArith.Zquot]
B:73 [binder, in Coq.Init.Datatypes]
b:73 [binder, in Coq.Reals.Ratan]
b:73 [binder, in Coq.Numbers.NatInt.NZDiv]
b:73 [binder, in Coq.NArith.Ndec]
b:74 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:74 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:74 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:74 [binder, in Coq.Bool.Bool]
b:74 [binder, in Coq.NArith.BinNatDef]
b:74 [binder, in Coq.Logic.ClassicalFacts]
b:74 [binder, in Coq.Reals.RiemannInt_SF]
b:74 [binder, in Coq.ZArith.Znumtheory]
b:75 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
b:75 [binder, in Coq.Sorting.PermutSetoid]
b:75 [binder, in Coq.Numbers.NatInt.NZPow]
B:75 [binder, in Coq.Classes.Morphisms]
b:75 [binder, in Coq.ZArith.Zdiv]
b:75 [binder, in Coq.Bool.Bool]
b:75 [binder, in Coq.Lists.ListSet]
b:75 [binder, in Coq.NArith.Ndec]
B:75 [binder, in Coq.Logic.FinFun]
b:76 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:76 [binder, in Coq.Numbers.NaryFunctions]
B:76 [binder, in Coq.Logic.FunctionalExtensionality]
b:76 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:76 [binder, in Coq.Numbers.NatInt.NZLog]
b:76 [binder, in Coq.Bool.Bool]
b:76 [binder, in Coq.Structures.OrderedTypeEx]
b:76 [binder, in Coq.ZArith.Zquot]
b:76 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:76 [binder, in Coq.Numbers.NatInt.NZDiv]
b:76 [binder, in Coq.NArith.BinNatDef]
b:77 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:77 [binder, in Coq.Numbers.NatInt.NZPow]
b:77 [binder, in Coq.Reals.RiemannInt]
b:77 [binder, in Coq.setoid_ring.Field_theory]
b:77 [binder, in Coq.ZArith.Zdiv]
b:77 [binder, in Coq.Bool.Bool]
b:77 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:77 [binder, in Coq.Reals.RiemannInt_SF]
b:77 [binder, in Coq.NArith.Ndec]
b:78 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:78 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:78 [binder, in Coq.Numbers.NaryFunctions]
b:78 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:78 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:78 [binder, in Coq.Numbers.NatInt.NZLog]
b:78 [binder, in Coq.Bool.Bool]
b:78 [binder, in Coq.Structures.OrderedTypeEx]
B:78 [binder, in Coq.Sorting.CPermutation]
b:78 [binder, in Coq.Lists.ListSet]
b:78 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:79 [binder, in Coq.Lists.Streams]
b:79 [binder, in Coq.setoid_ring.Field_theory]
b:79 [binder, in Coq.ZArith.Zdiv]
b:79 [binder, in Coq.Bool.Bool]
b:79 [binder, in Coq.ZArith.Zquot]
B:79 [binder, in Coq.Init.Datatypes]
b:79 [binder, in Coq.Numbers.NatInt.NZDiv]
b:79 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:79 [binder, in Coq.NArith.Ndec]
b:8 [binder, in Coq.Init.Byte]
b:8 [binder, in Coq.Numbers.Natural.Abstract.NPow]
b:8 [binder, in Coq.Numbers.NatInt.NZPow]
B:8 [binder, in Coq.Classes.RelationPairs]
b:8 [binder, in Coq.Numbers.Natural.Abstract.NDefOps]
b:8 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
b:8 [binder, in Coq.Numbers.Natural.Abstract.NSqrt]
b:8 [binder, in Coq.ssr.ssrbool]
b:8 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:8 [binder, in Coq.Numbers.NatInt.NZLog]
B:8 [binder, in Coq.Relations.Relations]
b:8 [binder, in Coq.Bool.Bool]
B:8 [binder, in Coq.Sets.Cpo]
B:8 [binder, in Coq.Logic.Berardi]
B:8 [binder, in Coq.Program.Combinators]
b:8 [binder, in Coq.Numbers.Integer.Abstract.ZPow]
B:8 [binder, in Coq.Program.Basics]
b:8 [binder, in Coq.NArith.Ndiv_def]
b:8 [binder, in Coq.ZArith.Znumtheory]
b:8 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
b:8 [binder, in Coq.ZArith.Zeuclid]
B:8 [binder, in Coq.Bool.DecBool]
b:80 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:80 [binder, in Coq.Numbers.NatInt.NZPow]
B:80 [binder, in Coq.MSets.MSetProperties]
b:80 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:80 [binder, in Coq.Numbers.Natural.Abstract.NBits]
b:80 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:80 [binder, in Coq.Numbers.NatInt.NZLog]
b:80 [binder, in Coq.Structures.OrderedTypeEx]
b:80 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:80 [binder, in Coq.NArith.BinNatDef]
b:80 [binder, in Coq.Reals.RiemannInt_SF]
B:80 [binder, in Coq.FSets.FSetProperties]
b:81 [binder, in Coq.Reals.RiemannInt]
b:81 [binder, in Coq.Sorting.Permutation]
b:81 [binder, in Coq.ZArith.Zdiv]
B:81 [binder, in Coq.Sorting.CPermutation]
b:81 [binder, in Coq.Lists.ListSet]
b:81 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:81 [binder, in Coq.NArith.Ndec]
b:82 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:82 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
B:82 [binder, in Coq.Sorting.PermutSetoid]
B:82 [binder, in Coq.micromega.RingMicromega]
b:82 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:82 [binder, in Coq.Structures.OrderedTypeEx]
B:82 [binder, in Coq.Classes.CMorphisms]
b:82 [binder, in Coq.ZArith.Zquot]
b:82 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:82 [binder, in Coq.Logic.ClassicalFacts]
b:83 [binder, in Coq.Lists.Streams]
b:83 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:83 [binder, in Coq.Sorting.PermutSetoid]
b:83 [binder, in Coq.Numbers.NatInt.NZPow]
b:83 [binder, in Coq.setoid_ring.Field_theory]
b:83 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:83 [binder, in Coq.Numbers.NatInt.NZLog]
b:83 [binder, in Coq.ZArith.Zdiv]
b:83 [binder, in Coq.NArith.Ndec]
b:84 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
b:84 [binder, in Coq.FSets.FMapFacts]
b:84 [binder, in Coq.ZArith.Zquot]
b:84 [binder, in Coq.Lists.ListSet]
b:84 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:84 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:85 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
B:85 [binder, in Coq.Logic.ChoiceFacts]
b:85 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:85 [binder, in Coq.ZArith.Zdiv]
b:85 [binder, in Coq.Numbers.NatInt.NZDiv]
b:85 [binder, in Coq.Reals.RiemannInt_SF]
b:85 [binder, in Coq.NArith.Ndec]
B:856 [binder, in Coq.Lists.List]
b:86 [binder, in Coq.Lists.Streams]
b:86 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
B:86 [binder, in Coq.Sorting.PermutSetoid]
b:86 [binder, in Coq.Numbers.NatInt.NZPow]
b:86 [binder, in Coq.Reals.RiemannInt]
B:86 [binder, in Coq.Classes.CMorphisms]
b:86 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:87 [binder, in Coq.Sorting.PermutSetoid]
B:87 [binder, in Coq.micromega.RingMicromega]
b:87 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:87 [binder, in Coq.Numbers.NatInt.NZLog]
B:87 [binder, in Coq.Sorting.CPermutation]
b:87 [binder, in Coq.ZArith.Zquot]
b:87 [binder, in Coq.Reals.RiemannInt_SF]
b:87 [binder, in Coq.NArith.Ndec]
b:88 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:88 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
B:88 [binder, in Coq.Logic.FunctionalExtensionality]
B:88 [binder, in Coq.ssr.ssreflect]
b:88 [binder, in Coq.Reals.NewtonInt]
b:88 [binder, in Coq.Numbers.NatInt.NZDiv]
b:88 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:89 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
B:89 [binder, in Coq.Sorting.PermutSetoid]
b:89 [binder, in Coq.MSets.MSetProperties]
b:89 [binder, in Coq.setoid_ring.Field_theory]
b:89 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:89 [binder, in Coq.Numbers.NatInt.NZLog]
b:89 [binder, in Coq.ZArith.Zdiv]
b:89 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
b:89 [binder, in Coq.Reals.Abstract.ConstructiveSum]
b:89 [binder, in Coq.FSets.FSetProperties]
b:89 [binder, in Coq.NArith.Ndec]
B:9 [binder, in Coq.Logic.Decidable]
b:9 [binder, in Coq.Init.Byte]
B:9 [binder, in Coq.Bool.IfProp]
b:9 [binder, in Coq.ssr.ssrbool]
b:9 [binder, in Coq.Reals.Machin]
b:9 [binder, in Coq.Bool.Bool]
b:9 [binder, in Coq.Strings.Ascii]
b:9 [binder, in Coq.ZArith.Zquot]
B:9 [binder, in Coq.Sets.Powerset_facts]
b:9 [binder, in Coq.Numbers.NatInt.NZSqrt]
b:9 [binder, in Coq.Numbers.NatInt.NZDiv]
b:90 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:90 [binder, in Coq.Sorting.PermutSetoid]
b:90 [binder, in Coq.Reals.RiemannInt]
b:90 [binder, in Coq.Bool.Bool]
b:90 [binder, in Coq.ZArith.Zquot]
b:90 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:91 [binder, in Coq.ZArith.BinIntDef]
b:91 [binder, in Coq.Floats.SpecFloat]
b:91 [binder, in Coq.Init.Specif]
b:91 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:91 [binder, in Coq.Structures.OrderedTypeEx]
b:91 [binder, in Coq.Numbers.NatInt.NZDiv]
b:91 [binder, in Coq.NArith.Ndec]
b:92 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:92 [binder, in Coq.MSets.MSetProperties]
b:92 [binder, in Coq.Numbers.NatInt.NZLog]
B:92 [binder, in Coq.ssr.ssreflect]
b:92 [binder, in Coq.ZArith.Zdiv]
b:92 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:92 [binder, in Coq.FSets.FSetProperties]
b:928 [binder, in Coq.Lists.List]
B:93 [binder, in Coq.Logic.FunctionalExtensionality]
b:93 [binder, in Coq.setoid_ring.Field_theory]
b:93 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:93 [binder, in Coq.ZArith.Zquot]
b:93 [binder, in Coq.ZArith.Znumtheory]
b:93 [binder, in Coq.micromega.ZifyInst]
B:936 [binder, in Coq.Lists.List]
b:94 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
b:94 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:94 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
b:94 [binder, in Coq.Numbers.NatInt.NZLog]
b:94 [binder, in Coq.Structures.OrderedTypeEx]
b:94 [binder, in Coq.Reals.NewtonInt]
b:94 [binder, in Coq.Numbers.NatInt.NZDiv]
b:94 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:94 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
b:94 [binder, in Coq.NArith.Ndec]
b:95 [binder, in Coq.MSets.MSetProperties]
B:95 [binder, in Coq.Numbers.NaryFunctions]
b:95 [binder, in Coq.Lists.List]
b:95 [binder, in Coq.FSets.FMapFacts]
b:95 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:95 [binder, in Coq.ZArith.Zdiv]
b:95 [binder, in Coq.Bool.Bool]
B:95 [binder, in Coq.Logic.ClassicalFacts]
b:95 [binder, in Coq.FSets.FSetProperties]
b:96 [binder, in Coq.Vectors.VectorSpec]
B:96 [binder, in Coq.ssr.ssreflect]
b:96 [binder, in Coq.Bool.Bool]
b:96 [binder, in Coq.Reals.Rbasic_fun]
b:96 [binder, in Coq.ZArith.Zquot]
b:96 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
b:97 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
B:97 [binder, in Coq.Sorting.PermutSetoid]
b:97 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
b:97 [binder, in Coq.Numbers.NaryFunctions]
b:97 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
b:97 [binder, in Coq.ZArith.Zdiv]
b:97 [binder, in Coq.Bool.Bool]
b:97 [binder, in Coq.Structures.OrderedTypeEx]
b:97 [binder, in Coq.Numbers.NatInt.NZDiv]
b:97 [binder, in Coq.ZArith.Znumtheory]
b:97 [binder, in Coq.NArith.Ndec]
b:98 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
b:98 [binder, in Coq.Sorting.PermutSetoid]
b:98 [binder, in Coq.Bool.Bool]
b:98 [binder, in Coq.Reals.NewtonInt]
B:98 [binder, in Coq.Sorting.CPermutation]
b:98 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
B:98 [binder, in Coq.Logic.ClassicalFacts]
b:98 [binder, in Coq.Reals.RiemannInt_SF]
B:984 [binder, in Coq.Lists.List]
b:99 [binder, in Coq.ZArith.Zdiv]
b:99 [binder, in Coq.Bool.Bool]
b:99 [binder, in Coq.ZArith.Zquot]
b:99 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
B:991 [binder, in Coq.Lists.List]


Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (68863 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (985 entries)
Binder Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (44709 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (761 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1497 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (570 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11380 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (976 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (603 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (298 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (460 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (476 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (811 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1157 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4018 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (162 entries)