| 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 | (72487 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1049 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (47021 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 | (788 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1537 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (588 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11841 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1025 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (634 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (306 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (473 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (486 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (881 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1465 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4229 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (164 entries) |
C
C [definition, in Coq.Reals.Binomial]cadd:298 [binder, in Coq.setoid_ring.Ring_theory]
cancel [definition, in Coq.ssr.ssrfun]
CancelOn [section, in Coq.ssr.ssrbool]
CancelOn.aD [variable, in Coq.ssr.ssrbool]
CancelOn.aT [variable, in Coq.ssr.ssrbool]
CancelOn.f [variable, in Coq.ssr.ssrbool]
CancelOn.g [variable, in Coq.ssr.ssrbool]
CancelOn.rD [variable, in Coq.ssr.ssrbool]
CancelOn.rT [variable, in Coq.ssr.ssrbool]
cancel_to_of [lemma, in Coq.Arith.Cantor]
cancel_of_to [lemma, in Coq.Arith.Cantor]
canLR [lemma, in Coq.ssr.ssrfun]
canLR_on [lemma, in Coq.ssr.ssrbool]
canLR_in [lemma, in Coq.ssr.ssrbool]
canon [projection, in Coq.QArith.Qcanon]
canonical_mantissa [definition, in Coq.Floats.SpecFloat]
canonical_Rsqr [lemma, in Coq.Reals.R_sqr]
canRL [lemma, in Coq.ssr.ssrfun]
canRL_on [lemma, in Coq.ssr.ssrbool]
canRL_in [lemma, in Coq.ssr.ssrbool]
Cantor [library]
can_inj [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]
can_mono_in [lemma, in Coq.ssr.ssrbool]
can_mono [lemma, in Coq.ssr.ssrbool]
can_in_inj [lemma, in Coq.ssr.ssrbool]
can_comp [lemma, in Coq.ssr.ssrfun]
can_inj [lemma, in Coq.ssr.ssrfun]
can_pcan [lemma, in Coq.ssr.ssrfun]
can_compute_Z [record, in Coq.nsatz.Nsatz]
can_compute_Z [inductive, in Coq.nsatz.Nsatz]
can_inj [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
cardinal [inductive, in Coq.Sets.Finite_sets]
cardinalO_empty [lemma, in Coq.Sets.Finite_sets_facts]
cardinal_unicity [lemma, in Coq.Sets.Finite_sets_facts]
cardinal_Empty [lemma, in Coq.Sets.Finite_sets_facts]
cardinal_is_functional [lemma, in Coq.Sets.Finite_sets_facts]
cardinal_finite [lemma, in Coq.Sets.Finite_sets_facts]
cardinal_elim [lemma, in Coq.Sets.Finite_sets]
cardinal_invert [lemma, in Coq.Sets.Finite_sets]
cardinal_decreases [lemma, in Coq.Sets.Image]
cardinal_Im_intro [lemma, in Coq.Sets.Image]
card_Add_gen [lemma, in Coq.Sets.Finite_sets_facts]
card_soustr_1 [lemma, in Coq.Sets.Finite_sets_facts]
card_add [constructor, in Coq.Sets.Finite_sets]
card_empty [constructor, in Coq.Sets.Finite_sets]
Carrier [definition, in Coq.Sets.Partial_Order]
Carrier_of [projection, in Coq.Sets.Partial_Order]
carry [abbreviation, in Coq.Numbers.Cyclic.Abstract.DoubleType]
carry [inductive, in Coq.Numbers.Cyclic.Abstract.CarryType]
CarryType [library]
carry:5 [binder, in Coq.Bool.Bvector]
carry:8 [binder, in Coq.Bool.Bvector]
caserec:17 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
caserec:25 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
caserec:55 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
caseS [definition, in Coq.Vectors.Fin]
caseS [definition, in Coq.Vectors.VectorDef]
caseS' [definition, in Coq.Vectors.Fin]
caseS' [definition, in Coq.Vectors.VectorDef]
case0 [definition, in Coq.Vectors.Fin]
case0 [definition, in Coq.Vectors.VectorDef]
case0:16 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
case0:24 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
case0:54 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
cast [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]
cast [definition, in Coq.Vectors.Fin]
cast [definition, in Coq.Vectors.VectorEq]
CAST [section, in Coq.Vectors.VectorEq]
cast [definition, in Coq.Numbers.Cyclic.Int63.Uint63]
cast_diff [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]
cast_refl [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]
cast_diff [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
cast_refl [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
catcomp [definition, in Coq.ssr.ssrfun]
cauchy [projection, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CauchyMorph_rat [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
cauchy_finite [lemma, in Coq.Reals.Cauchy_prod]
cauchy_bound [lemma, in Coq.Reals.Rseries]
Cauchy_crit [definition, in Coq.Reals.Rseries]
cauchy_abs [lemma, in Coq.Reals.PartSum]
Cauchy_crit_series [definition, in Coq.Reals.PartSum]
cauchy_min [lemma, in Coq.Reals.SeqProp]
cauchy_opp [lemma, in Coq.Reals.SeqProp]
cauchy_maj [lemma, in Coq.Reals.SeqProp]
Cauchy_prod [library]
cau:139 [binder, in Coq.Reals.Abstract.ConstructiveSum]
cau:144 [binder, in Coq.Reals.Abstract.ConstructiveSum]
cd:618 [binder, in Coq.ssr.ssrbool]
ceiling [definition, in Coq.micromega.ZMicromega]
ceqb_spec [lemma, in Coq.setoid_ring.Ring_polynom]
ceqb_spec [lemma, in Coq.micromega.EnvRing]
ceqb_spec' [lemma, in Coq.setoid_ring.Field_theory]
ceqb_spec [lemma, in Coq.setoid_ring.Field_theory]
ceqb:302 [binder, in Coq.setoid_ring.Ring_theory]
CEquivalence [library]
certif:30 [binder, in Coq.nsatz.NsatzTactic]
certif:60 [binder, in Coq.nsatz.NsatzTactic]
Cesaro [lemma, in Coq.Reals.SeqSeries]
Cesaro_1 [lemma, in Coq.Reals.SeqSeries]
CFactor [definition, in Coq.setoid_ring.Ring_polynom]
Chain [record, in Coq.Sets.Cpo]
Chain_cond [projection, in Coq.Sets.Cpo]
Char [library]
charac [definition, in Coq.Sets.Uniset]
Charac [constructor, in Coq.Sets.Uniset]
Characterisation_wf_relations.leA [variable, in Coq.Wellfounded.Well_Ordering]
Characterisation_wf_relations.A [variable, in Coq.Wellfounded.Well_Ordering]
Characterisation_wf_relations [section, in Coq.Wellfounded.Well_Ordering]
check [definition, in Coq.nsatz.NsatzTactic]
checker_nf_sound [lemma, in Coq.micromega.RingMicromega]
check_correct [lemma, in Coq.nsatz.NsatzTactic]
check_normalised_formulas [definition, in Coq.micromega.RingMicromega]
check_inconsistent_sound [lemma, in Coq.micromega.RingMicromega]
check_inconsistent [definition, in Coq.micromega.RingMicromega]
check_applicative_mem_pred [definition, in Coq.ssr.ssrbool]
check_proof [definition, in Coq.rtauto.Rtauto]
choice [lemma, in Coq.Logic.ClassicalEpsilon]
Choice [lemma, in Coq.Init.Specif]
choice [lemma, in Coq.Logic.ClassicalChoice]
ChoiceFacts [library]
ChoiceSchemes [section, in Coq.Logic.ChoiceFacts]
ChoiceSchemes.A [variable, in Coq.Logic.ChoiceFacts]
ChoiceSchemes.B [variable, in Coq.Logic.ChoiceFacts]
ChoiceSchemes.P [variable, in Coq.Logic.ChoiceFacts]
Choice_lemmas.R2 [variable, in Coq.Init.Specif]
Choice_lemmas.R1 [variable, in Coq.Init.Specif]
Choice_lemmas.R' [variable, in Coq.Init.Specif]
Choice_lemmas.R [variable, in Coq.Init.Specif]
Choice_lemmas.S' [variable, in Coq.Init.Specif]
Choice_lemmas.S [variable, in Coq.Init.Specif]
Choice_lemmas [section, in Coq.Init.Specif]
Choice2 [lemma, in Coq.Init.Specif]
ch:1 [binder, in Coq.Strings.OctalString]
ch:1 [binder, in Coq.Strings.HexString]
ch:1 [binder, in Coq.Strings.BinaryString]
cI [definition, in Coq.setoid_ring.Ncring_polynom]
CInv [constructor, in Coq.micromega.RMicromega]
CInvR0 [definition, in Coq.micromega.RMicromega]
cI:297 [binder, in Coq.setoid_ring.Ring_theory]
ck:419 [binder, in Coq.micromega.ZMicromega]
ck:421 [binder, in Coq.micromega.ZMicromega]
ck:423 [binder, in Coq.micromega.ZMicromega]
ck:425 [binder, in Coq.micromega.ZMicromega]
ck:439 [binder, in Coq.micromega.ZMicromega]
ck:441 [binder, in Coq.micromega.ZMicromega]
classic [axiom, in Coq.Logic.Classical_Prop]
Classical [library]
ClassicalChoice [library]
ClassicalConstructiveReals [library]
ClassicalDedekindReals [library]
ClassicalDescription [library]
ClassicalEpsilon [library]
ClassicalFacts [library]
classically [definition, in Coq.ssr.ssrbool]
ClassicalUniqueChoice [library]
classical_indefinite_description [lemma, in Coq.Logic.ClassicalEpsilon]
classical_denumerable_description_imp_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
classical_proof_irrelevence [abbreviation, in Coq.Logic.Berardi]
classical_proof_irrelevance [lemma, in Coq.Logic.Berardi]
classical_definite_description [lemma, in Coq.Logic.ClassicalDescription]
classical_de_morgan_law [definition, in Coq.Logic.ClassicalFacts]
Classical_Prop [library]
Classical_Pred_Type [library]
Classical_sets [library]
classicP [lemma, in Coq.ssr.ssrbool]
classicW [lemma, in Coq.ssr.ssrbool]
classic_imply [lemma, in Coq.ssr.ssrbool]
classic_pick [lemma, in Coq.ssr.ssrbool]
classic_EM [lemma, in Coq.ssr.ssrbool]
classic_bind [lemma, in Coq.ssr.ssrbool]
classic_set [abbreviation, in Coq.Logic.ClassicalUniqueChoice]
classic_set_in_prop_context [lemma, in Coq.Logic.ClassicalUniqueChoice]
classify [axiom, in Coq.Floats.PrimFloat]
classify_spec [axiom, in Coq.Floats.FloatAxioms]
clause [definition, in Coq.micromega.Tauto]
cleb_sound [lemma, in Coq.micromega.RingMicromega]
clone_pred [definition, in Coq.ssr.ssrbool]
closed [record, in Coq.setoid_ring.Ncring_tac]
closed_set_P1 [lemma, in Coq.Reals.Rtopology]
closed_set [definition, in Coq.Reals.Rtopology]
clos_trans_transp_permute [lemma, in Coq.Relations.Operators_Properties]
clos_rst_rstn1_iff [lemma, in Coq.Relations.Operators_Properties]
clos_rst_rstn1 [lemma, in Coq.Relations.Operators_Properties]
clos_rstn1_sym [lemma, in Coq.Relations.Operators_Properties]
clos_rstn1_trans [lemma, in Coq.Relations.Operators_Properties]
clos_rstn1_rst [lemma, in Coq.Relations.Operators_Properties]
clos_rst_rst1n_iff [lemma, in Coq.Relations.Operators_Properties]
clos_rst_rst1n [lemma, in Coq.Relations.Operators_Properties]
clos_rst1n_sym [lemma, in Coq.Relations.Operators_Properties]
clos_rst1n_trans [lemma, in Coq.Relations.Operators_Properties]
clos_rst1n_rst [lemma, in Coq.Relations.Operators_Properties]
clos_refl_trans_ind_right [lemma, in Coq.Relations.Operators_Properties]
clos_refl_trans_ind_left [lemma, in Coq.Relations.Operators_Properties]
clos_rt_rtn1_iff [lemma, in Coq.Relations.Operators_Properties]
clos_rt_rtn1 [lemma, in Coq.Relations.Operators_Properties]
clos_rtn1_rt [lemma, in Coq.Relations.Operators_Properties]
clos_rt_rt1n_iff [lemma, in Coq.Relations.Operators_Properties]
clos_rt_rt1n [lemma, in Coq.Relations.Operators_Properties]
clos_rt1n_rt [lemma, in Coq.Relations.Operators_Properties]
clos_rtn1_step [lemma, in Coq.Relations.Operators_Properties]
clos_rt1n_step [lemma, in Coq.Relations.Operators_Properties]
clos_trans_tn1_iff [lemma, in Coq.Relations.Operators_Properties]
clos_trans_tn1 [lemma, in Coq.Relations.Operators_Properties]
clos_tn1_trans [lemma, in Coq.Relations.Operators_Properties]
clos_trans_t1n_iff [lemma, in Coq.Relations.Operators_Properties]
clos_trans_t1n [lemma, in Coq.Relations.Operators_Properties]
clos_t1n_trans [lemma, in Coq.Relations.Operators_Properties]
clos_rst_idempotent [lemma, in Coq.Relations.Operators_Properties]
clos_rst_is_equiv [lemma, in Coq.Relations.Operators_Properties]
clos_rt_t [lemma, in Coq.Relations.Operators_Properties]
clos_r_clos_rt [lemma, in Coq.Relations.Operators_Properties]
clos_rt_clos_rst [lemma, in Coq.Relations.Operators_Properties]
clos_rt_idempotent [lemma, in Coq.Relations.Operators_Properties]
clos_rt_is_preorder [lemma, in Coq.Relations.Operators_Properties]
clos_refl_sym_trans_n1 [inductive, in Coq.Relations.Relation_Operators]
clos_refl_sym_trans_1n [inductive, in Coq.Relations.Relation_Operators]
clos_refl_sym_trans [inductive, in Coq.Relations.Relation_Operators]
clos_refl_trans_n1 [inductive, in Coq.Relations.Relation_Operators]
clos_refl_trans_1n [inductive, in Coq.Relations.Relation_Operators]
clos_refl_trans [inductive, in Coq.Relations.Relation_Operators]
clos_refl [inductive, in Coq.Relations.Relation_Operators]
clos_trans_n1 [inductive, in Coq.Relations.Relation_Operators]
clos_trans_1n [inductive, in Coq.Relations.Relation_Operators]
clos_trans [inductive, in Coq.Relations.Relation_Operators]
cltb [definition, in Coq.micromega.RingMicromega]
cltb_sound [lemma, in Coq.micromega.RingMicromega]
clt_morph [lemma, in Coq.micromega.ZCoeff]
clt_pos_morph [lemma, in Coq.micromega.ZCoeff]
cl':536 [binder, in Coq.micromega.Tauto]
cl1:134 [binder, in Coq.micromega.Tauto]
cl1:204 [binder, in Coq.micromega.Tauto]
cl2:135 [binder, in Coq.micromega.Tauto]
cl2:205 [binder, in Coq.micromega.Tauto]
cl:117 [binder, in Coq.micromega.RMicromega]
cl:131 [binder, in Coq.micromega.Tauto]
cl:186 [binder, in Coq.micromega.ZMicromega]
cl:201 [binder, in Coq.micromega.Tauto]
cl:430 [binder, in Coq.micromega.Tauto]
cl:433 [binder, in Coq.micromega.Tauto]
cl:444 [binder, in Coq.micromega.ZMicromega]
cl:516 [binder, in Coq.micromega.Tauto]
cl:528 [binder, in Coq.micromega.Tauto]
cl:532 [binder, in Coq.micromega.Tauto]
cl:535 [binder, in Coq.micromega.Tauto]
cl:81 [binder, in Coq.micromega.QMicromega]
CMinus [constructor, in Coq.micromega.RMicromega]
cmod [definition, in Coq.Numbers.Cyclic.Int63.Sint63]
cmodwB [abbreviation, in Coq.micromega.ZifySint63]
cmod_small [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]
cmod_mod [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]
CMorphisms [library]
Cmp [definition, in Coq.FSets.FMapInterface]
CmpNotation [module, in Coq.Structures.Orders]
_ ?= _ [notation, in Coq.Structures.Orders]
CmpSpec [module, in Coq.Structures.Orders]
CmpSpec.compare_spec [axiom, in Coq.Structures.Orders]
cmp:134 [binder, in Coq.FSets.FMapFullAVL]
cmp:1385 [binder, in Coq.FSets.FMapAVL]
cmp:1460 [binder, in Coq.FSets.FMapAVL]
cmp:1461 [binder, in Coq.FSets.FMapAVL]
cmp:1466 [binder, in Coq.FSets.FMapAVL]
cmp:1469 [binder, in Coq.FSets.FMapAVL]
cmp:16 [binder, in Coq.Structures.GenericMinMax]
cmp:2 [binder, in Coq.FSets.FMapInterface]
cmp:20 [binder, in Coq.Structures.GenericMinMax]
cmp:209 [binder, in Coq.FSets.FMapFullAVL]
cmp:210 [binder, in Coq.FSets.FMapFullAVL]
cmp:215 [binder, in Coq.FSets.FMapFullAVL]
cmp:216 [binder, in Coq.FSets.FMapFacts]
cmp:218 [binder, in Coq.FSets.FMapFullAVL]
cmp:226 [binder, in Coq.FSets.FMapFacts]
cmp:283 [binder, in Coq.FSets.FMapWeakList]
cmp:286 [binder, in Coq.FSets.FMapPositive]
cmp:287 [binder, in Coq.FSets.FMapWeakList]
cmp:291 [binder, in Coq.FSets.FMapList]
cmp:293 [binder, in Coq.FSets.FMapWeakList]
cmp:297 [binder, in Coq.FSets.FMapList]
cmp:298 [binder, in Coq.FSets.FMapWeakList]
cmp:300 [binder, in Coq.FSets.FMapList]
cmp:304 [binder, in Coq.FSets.FMapList]
cmp:305 [binder, in Coq.FSets.FMapWeakList]
cmp:307 [binder, in Coq.FSets.FMapPositive]
cmp:309 [binder, in Coq.FSets.FMapList]
cmp:311 [binder, in Coq.FSets.FMapPositive]
cmp:315 [binder, in Coq.FSets.FMapPositive]
cmp:316 [binder, in Coq.FSets.FMapWeakList]
cmp:321 [binder, in Coq.FSets.FMapWeakList]
cmp:326 [binder, in Coq.FSets.FMapWeakList]
cmp:331 [binder, in Coq.FSets.FMapWeakList]
cmp:351 [binder, in Coq.FSets.FMapList]
cmp:362 [binder, in Coq.FSets.FMapList]
cmp:367 [binder, in Coq.FSets.FMapList]
cmp:368 [binder, in Coq.FSets.FMapList]
cmp:39 [binder, in Coq.FSets.FMapFacts]
cmp:518 [binder, in Coq.FSets.FMapWeakList]
cmp:537 [binder, in Coq.FSets.FMapWeakList]
cmp:538 [binder, in Coq.FSets.FMapList]
cmp:557 [binder, in Coq.FSets.FMapList]
cmp:597 [binder, in Coq.FSets.FMapWeakList]
cmp:600 [binder, in Coq.FSets.FMapWeakList]
cmp:618 [binder, in Coq.FSets.FMapList]
cmp:621 [binder, in Coq.FSets.FMapList]
cmp:76 [binder, in Coq.FSets.FMapInterface]
cmt [constructor, in Coq.funind.Recdef]
CMult [constructor, in Coq.micromega.RMicromega]
cmul:299 [binder, in Coq.setoid_ring.Ring_theory]
cM1:161 [binder, in Coq.setoid_ring.Ring_polynom]
cM1:169 [binder, in Coq.setoid_ring.Ring_polynom]
cM1:175 [binder, in Coq.setoid_ring.Ring_polynom]
cM1:286 [binder, in Coq.setoid_ring.Ring_polynom]
cM1:292 [binder, in Coq.setoid_ring.Ring_polynom]
cM1:297 [binder, in Coq.setoid_ring.Ring_polynom]
cm:113 [binder, in Coq.micromega.RMicromega]
cm:179 [binder, in Coq.micromega.RingMicromega]
cm:181 [binder, in Coq.micromega.RingMicromega]
cM:279 [binder, in Coq.setoid_ring.Ring_polynom]
cm:72 [binder, in Coq.micromega.QMicromega]
cm:78 [binder, in Coq.micromega.ZMicromega]
cneqb [definition, in Coq.micromega.RingMicromega]
cneqb_sound [lemma, in Coq.micromega.RingMicromega]
cnf [definition, in Coq.micromega.Tauto]
cnfQ [definition, in Coq.micromega.QMicromega]
cnfZ [definition, in Coq.micromega.ZMicromega]
cnf_negate_correct [lemma, in Coq.micromega.RingMicromega]
cnf_normalise_correct [lemma, in Coq.micromega.RingMicromega]
cnf_negate [definition, in Coq.micromega.RingMicromega]
cnf_normalise [definition, in Coq.micromega.RingMicromega]
cnf_of_list_correct [lemma, in Coq.micromega.RingMicromega]
cnf_of_list [definition, in Coq.micromega.RingMicromega]
cnf_of_list_correct [lemma, in Coq.micromega.ZMicromega]
cnf_of_list [definition, in Coq.micromega.ZMicromega]
cnf_checker_sound [lemma, in Coq.micromega.Tauto]
cnf_checker [definition, in Coq.micromega.Tauto]
cnf_ff [definition, in Coq.micromega.Tauto]
cnf_tt [definition, in Coq.micromega.Tauto]
Cn:36 [binder, in Coq.Reals.PartSum]
cO [definition, in Coq.setoid_ring.Ncring_polynom]
coherent [definition, in Coq.Sets.Relations_3]
COHERENT_VALUE [section, in Coq.ZArith.Zdigits]
coherent_symmetric [lemma, in Coq.Sets.Relations_3_facts]
collective_pred_of_simpl [definition, in Coq.ssr.ssrbool]
collective_pred [definition, in Coq.ssr.ssrbool]
collect_annot [definition, in Coq.micromega.Tauto]
Color [module, in Coq.MSets.MSetRBT]
color [inductive, in Coq.MSets.MSetRBT]
Color.t [definition, in Coq.MSets.MSetRBT]
Combinators [library]
combine [definition, in Coq.Lists.List]
combine_firstn [lemma, in Coq.Lists.List]
combine_firstn_r [lemma, in Coq.Lists.List]
combine_firstn_l [lemma, in Coq.Lists.List]
combine_nil [lemma, in Coq.Lists.List]
combine_nth [lemma, in Coq.Lists.List]
combine_length [lemma, in Coq.Lists.List]
combine_split [lemma, in Coq.Lists.List]
Combining [section, in Coq.Lists.List]
Combining.A [variable, in Coq.Lists.List]
Combining.B [variable, in Coq.Lists.List]
comm [lemma, in Coq.setoid_ring.Ncring_tac]
common [abbreviation, in Coq.setoid_ring.Field_theory]
commut [definition, in Coq.Relations.Relation_Definitions]
commutative [definition, in Coq.ssr.ssrfun]
comm_left [lemma, in Coq.Sets.Permut]
comm_right [lemma, in Coq.Sets.Permut]
comp [definition, in Coq.Reals.Ranalysis1]
comp [definition, in Coq.ssr.ssrfun]
compact [definition, in Coq.Reals.Rtopology]
compact_P6 [lemma, in Coq.Reals.Rtopology]
compact_carac [lemma, in Coq.Reals.Rtopology]
compact_P5 [lemma, in Coq.Reals.Rtopology]
compact_P4 [lemma, in Coq.Reals.Rtopology]
compact_P3 [lemma, in Coq.Reals.Rtopology]
compact_eqDom [lemma, in Coq.Reals.Rtopology]
compact_EMP [lemma, in Coq.Reals.Rtopology]
compact_P2 [lemma, in Coq.Reals.Rtopology]
compact_P1 [lemma, in Coq.Reals.Rtopology]
compare [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
compare [axiom, in Coq.Floats.PrimFloat]
compare [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]
compare [definition, in Coq.Init.Nat]
compare [definition, in Coq.Bool.Bool]
compare [axiom, in Coq.Numbers.Cyclic.Int63.PrimInt63]
Compare [inductive, in Coq.Structures.OrderedType]
compare [abbreviation, in Coq.Numbers.Cyclic.Int63.Uint63]
compare [abbreviation, in Coq.Numbers.Cyclic.Int63.Sint63]
Compare [library]
CompareBasedOrder [module, in Coq.Structures.OrdersFacts]
CompareBasedOrderFacts [module, in Coq.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_nge_iff [lemma, in Coq.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_nle_iff [lemma, in Coq.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_nlt_iff [lemma, in Coq.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_ngt_iff [lemma, in Coq.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_ge_iff [lemma, in Coq.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_gt_iff [lemma, in Coq.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_refl [lemma, in Coq.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_eq [lemma, in Coq.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_spec [lemma, in Coq.Structures.OrdersFacts]
CompareBasedOrderFacts.lt_eq_cases [lemma, in Coq.Structures.OrdersFacts]
CompareBasedOrderFacts.lt_irrefl [lemma, in Coq.Structures.OrdersFacts]
CompareBasedOrder.compare_antisym [axiom, in Coq.Structures.OrdersFacts]
CompareBasedOrder.compare_le_iff [axiom, in Coq.Structures.OrdersFacts]
CompareBasedOrder.compare_lt_iff [axiom, in Coq.Structures.OrdersFacts]
CompareBasedOrder.compare_eq_iff [axiom, in Coq.Structures.OrdersFacts]
CompareFacts [module, in Coq.Structures.OrdersFacts]
CompareFacts.compare_antisym [lemma, in Coq.Structures.OrdersFacts]
CompareFacts.compare_refl [lemma, in Coq.Structures.OrdersFacts]
CompareFacts.compare_compat [instance, in Coq.Structures.OrdersFacts]
CompareFacts.compare_ngt_iff [lemma, in Coq.Structures.OrdersFacts]
CompareFacts.compare_nlt_iff [lemma, in Coq.Structures.OrdersFacts]
CompareFacts.compare_gt_iff [lemma, in Coq.Structures.OrdersFacts]
CompareFacts.compare_lt_iff [lemma, in Coq.Structures.OrdersFacts]
CompareFacts.compare_eq [lemma, in Coq.Structures.OrdersFacts]
CompareFacts.compare_eq_iff [lemma, in Coq.Structures.OrdersFacts]
_ ?= _ [notation, in Coq.Structures.OrdersFacts]
compares [axiom, in Coq.Numbers.Cyclic.Int63.PrimInt63]
CompareSpec [inductive, in Coq.Init.Datatypes]
CompareSpecT [inductive, in Coq.Init.Datatypes]
CompareSpec2Type [lemma, in Coq.Init.Datatypes]
compare_spec [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]
compare_def_spec [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]
compare_def [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]
compare_spec [lemma, in Coq.Bool.Bool]
compare_spec [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
compare_def_spec [axiom, in Coq.Numbers.Cyclic.Int63.Uint63]
compare_def [definition, in Coq.Numbers.Cyclic.Int63.Uint63]
compare_spec [axiom, in Coq.Numbers.Cyclic.Int63.Sint63]
compare_spec [axiom, in Coq.Floats.FloatAxioms]
Compare_dec [library]
Compare2EqBool [module, in Coq.Structures.Orders]
Compare2EqBool.eqb [definition, in Coq.Structures.Orders]
Compare2EqBool.eqb_eq [lemma, in Coq.Structures.Orders]
compare31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
comparison [inductive, in Coq.Init.Datatypes]
comparison_eq_stable [lemma, in Coq.Init.Datatypes]
Compatible [definition, in Coq.Sets.Cpo]
compat_Reflexive [instance, in Coq.ssr.ssrsetoid]
compat_op [definition, in Coq.Lists.SetoidList]
compat_P [definition, in Coq.Lists.SetoidList]
compat_nat [definition, in Coq.Lists.SetoidList]
compat_bool [definition, in Coq.Lists.SetoidList]
CompEq [constructor, in Coq.Init.Datatypes]
CompEqT [constructor, in Coq.Init.Datatypes]
CompGt [constructor, in Coq.Init.Datatypes]
CompGtT [constructor, in Coq.Init.Datatypes]
complement [definition, in Coq.Classes.RelationClasses]
Complement [definition, in Coq.Sets.Ensembles]
Complement [definition, in Coq.Sets.Relations_1_facts]
complement [definition, in Coq.Classes.CRelationClasses]
complementary [definition, in Coq.Reals.Rtopology]
complementary_P1 [lemma, in Coq.Reals.Rtopology]
complement_Symmetric [definition, in Coq.Classes.RelationClasses]
complement_Irreflexive [definition, in Coq.Classes.RelationClasses]
complement_inverse [lemma, in Coq.Classes.RelationClasses]
complement_proper [definition, in Coq.Classes.Morphisms]
complement_Symmetric [definition, in Coq.Classes.CRelationClasses]
complement_Irreflexive [definition, in Coq.Classes.CRelationClasses]
complement_inverse [lemma, in Coq.Classes.CRelationClasses]
complement_negative [definition, in Coq.Numbers.Cyclic.Int31.Int31]
Complement_Complement [lemma, in Coq.Sets.Classical_sets]
Complete [section, in Coq.setoid_ring.Field_theory]
Complete [inductive, in Coq.Sets.Cpo]
completeness [lemma, in Coq.Reals.Raxioms]
Completeness [section, in Coq.btauto.Reflect]
completeness_weak [lemma, in Coq.Reals.RIneq]
Complete.AlmostField [section, in Coq.setoid_ring.Field_theory]
Complete.AlmostField.AFth [variable, in Coq.setoid_ring.Field_theory]
Complete.AlmostField.ARth [variable, in Coq.setoid_ring.Field_theory]
Complete.AlmostField.gen_phiPOS_not_0 [variable, in Coq.setoid_ring.Field_theory]
Complete.AlmostField.rdiv_def [variable, in Coq.setoid_ring.Field_theory]
Complete.AlmostField.rinv_l [variable, in Coq.setoid_ring.Field_theory]
Complete.AlmostField.rI_neq_rO [variable, in Coq.setoid_ring.Field_theory]
Complete.AlmostField.S_inj [variable, in Coq.setoid_ring.Field_theory]
Complete.Field [section, in Coq.setoid_ring.Field_theory]
Complete.Field.AFth [variable, in Coq.setoid_ring.Field_theory]
Complete.Field.ARth [variable, in Coq.setoid_ring.Field_theory]
Complete.Field.Fth [variable, in Coq.setoid_ring.Field_theory]
Complete.Field.gen_phiPOS_inject [variable, in Coq.setoid_ring.Field_theory]
Complete.Field.gen_phiPOS_not_0 [variable, in Coq.setoid_ring.Field_theory]
Complete.Field.rdiv_def [variable, in Coq.setoid_ring.Field_theory]
Complete.Field.rinv_l [variable, in Coq.setoid_ring.Field_theory]
Complete.Field.rI_neq_rO [variable, in Coq.setoid_ring.Field_theory]
Complete.Field.Rth [variable, in Coq.setoid_ring.Field_theory]
Complete.R [variable, in Coq.setoid_ring.Field_theory]
Complete.radd [variable, in Coq.setoid_ring.Field_theory]
Complete.rdiv [variable, in Coq.setoid_ring.Field_theory]
Complete.req [variable, in Coq.setoid_ring.Field_theory]
Complete.Reqe [variable, in Coq.setoid_ring.Field_theory]
Complete.rI [variable, in Coq.setoid_ring.Field_theory]
Complete.rinv [variable, in Coq.setoid_ring.Field_theory]
Complete.rmul [variable, in Coq.setoid_ring.Field_theory]
Complete.rO [variable, in Coq.setoid_ring.Field_theory]
Complete.ropp [variable, in Coq.setoid_ring.Field_theory]
Complete.Rsth [variable, in Coq.setoid_ring.Field_theory]
Complete.rsub [variable, in Coq.setoid_ring.Field_theory]
_ == _ [notation, in Coq.setoid_ring.Field_theory]
_ / _ [notation, in Coq.setoid_ring.Field_theory]
_ - _ [notation, in Coq.setoid_ring.Field_theory]
_ * _ [notation, in Coq.setoid_ring.Field_theory]
_ + _ [notation, in Coq.setoid_ring.Field_theory]
- _ [notation, in Coq.setoid_ring.Field_theory]
/ _ [notation, in Coq.setoid_ring.Field_theory]
0 [notation, in Coq.setoid_ring.Field_theory]
1 [notation, in Coq.setoid_ring.Field_theory]
CompLt [constructor, in Coq.Init.Datatypes]
CompLtT [constructor, in Coq.Init.Datatypes]
CompOpp [definition, in Coq.Init.Datatypes]
CompOpp_iff [lemma, in Coq.Init.Datatypes]
CompOpp_inj [lemma, in Coq.Init.Datatypes]
CompOpp_involutive [lemma, in Coq.Init.Datatypes]
compose [definition, in Coq.Program.Basics]
compose_proper [instance, in Coq.Classes.Morphisms]
compose_proper [instance, in Coq.Classes.CMorphisms]
compose_assoc [lemma, in Coq.Program.Combinators]
compose_id_right [lemma, in Coq.Program.Combinators]
compose_id_left [lemma, in Coq.Program.Combinators]
compose0 [lemma, in Coq.rtauto.Rtauto]
compose1 [lemma, in Coq.rtauto.Rtauto]
compose2 [lemma, in Coq.rtauto.Rtauto]
compose3 [lemma, in Coq.rtauto.Rtauto]
Composition [section, in Coq.ssr.ssrfun]
Composition.A [variable, in Coq.ssr.ssrfun]
Composition.B [variable, in Coq.ssr.ssrfun]
Composition.C [variable, in Coq.ssr.ssrfun]
CompSpec [definition, in Coq.Init.Datatypes]
CompSpecT [definition, in Coq.Init.Datatypes]
CompSpec2Type [lemma, in Coq.Init.Datatypes]
Computational [section, in Coq.btauto.Algebra]
Computational [constructor, in Coq.setoid_ring.Ring_theory]
compute_list_correct [lemma, in Coq.nsatz.NsatzTactic]
compute_list [definition, in Coq.nsatz.NsatzTactic]
concat [definition, in Coq.Strings.String]
concat [definition, in Coq.Lists.List]
concat_nil_Forall [lemma, in Coq.Lists.List]
concat_filter_map [lemma, in Coq.Lists.List]
concat_map [lemma, in Coq.Lists.List]
concat_app [lemma, in Coq.Lists.List]
concat_cons [lemma, in Coq.Lists.List]
concat_nil [lemma, in Coq.Lists.List]
condition [projection, in Coq.setoid_ring.Field_theory]
Conditionally_complete [inductive, in Coq.Sets.Cpo]
conditional_eq [definition, in Coq.Program.Equality]
condition:111 [binder, in Coq.ssr.ssrbool]
condition:123 [binder, in Coq.ssr.ssreflect]
cond_D2 [projection, in Coq.Reals.Ranalysis1]
cond_D1 [projection, in Coq.Reals.Ranalysis1]
cond_diff [projection, in Coq.Reals.Ranalysis1]
cond_Zopp [definition, in Coq.Floats.SpecFloat]
cond_positivity [definition, in Coq.Reals.Rsqrt_def]
cond_fam [projection, in Coq.Reals.Rtopology]
cond_nonzero [projection, in Coq.Reals.RIneq]
cond_neg [projection, in Coq.Reals.RIneq]
cond_nonpos [projection, in Coq.Reals.RIneq]
cond_pos [projection, in Coq.Reals.RIneq]
cond_nonneg [projection, in Coq.Reals.RIneq]
cond_pos_sum [lemma, in Coq.Reals.PartSum]
cond_pos_sum [lemma, in Coq.Reals.Abstract.ConstructiveSum]
cond_eq [lemma, in Coq.Reals.SeqProp]
Cond0 [definition, in Coq.nsatz.NsatzTactic]
coneMember [definition, in Coq.micromega.ZMicromega]
Confluent [definition, in Coq.Sets.Relations_3]
confluent [definition, in Coq.Sets.Relations_3]
congr1 [definition, in Coq.ssr.ssrfun]
congr2 [definition, in Coq.ssr.ssrfun]
cong_transitive_same_relation [lemma, in Coq.Sets.Relations_1_facts]
cong_antisymmetric_same_relation [lemma, in Coq.Sets.Relations_1_facts]
cong_symmetric_same_relation [lemma, in Coq.Sets.Relations_1_facts]
cong_reflexive_same_relation [lemma, in Coq.Sets.Relations_1_facts]
cong_congr [lemma, in Coq.Sets.Permut]
conj [constructor, in Coq.Init.Logic]
Conjunct [constructor, in Coq.rtauto.Rtauto]
Conjunction [section, in Coq.Init.Logic]
Conjunction.A [variable, in Coq.Init.Logic]
Conjunction.B [variable, in Coq.Init.Logic]
connectives [section, in Coq.Bool.Sumbool]
connectives.A [variable, in Coq.Bool.Sumbool]
connectives.B [variable, in Coq.Bool.Sumbool]
connectives.C [variable, in Coq.Bool.Sumbool]
connectives.D [variable, in Coq.Bool.Sumbool]
connectives.H1 [variable, in Coq.Bool.Sumbool]
connectives.H2 [variable, in Coq.Bool.Sumbool]
Cons [constructor, in Coq.Lists.Streams]
cons [abbreviation, in Coq.Lists.List]
cons [constructor, in Coq.Init.Datatypes]
cons [abbreviation, in Coq.Reals.RList]
cons [constructor, in Coq.Vectors.VectorDef]
const [definition, in Coq.Lists.Streams]
const [definition, in Coq.Program.Basics]
const [definition, in Coq.Vectors.VectorDef]
constant [definition, in Coq.Reals.Ranalysis1]
Constant_Stream.a [variable, in Coq.Lists.Streams]
Constant_Stream.A [variable, in Coq.Lists.Streams]
Constant_Stream [section, in Coq.Lists.Streams]
constant_D_eq [definition, in Coq.Reals.Ranalysis1]
Constr [library]
ConstructiveAbs [library]
ConstructiveCauchyAbs [library]
ConstructiveCauchyReals [library]
ConstructiveCauchyRealsMult [library]
ConstructiveDefiniteDescription [abbreviation, in Coq.Logic.ChoiceFacts]
ConstructiveDefiniteDescription_on [definition, in Coq.Logic.ChoiceFacts]
ConstructiveEpsilon [library]
ConstructiveExtra [library]
ConstructiveGroundEpsilon [section, in Coq.Logic.ConstructiveEpsilon]
ConstructiveGroundEpsilon_nat.P_decidable [variable, in Coq.Logic.ConstructiveEpsilon]
ConstructiveGroundEpsilon_nat.P [variable, in Coq.Logic.ConstructiveEpsilon]
ConstructiveGroundEpsilon_nat [section, in Coq.Logic.ConstructiveEpsilon]
ConstructiveGroundEpsilon.A [variable, in Coq.Logic.ConstructiveEpsilon]
ConstructiveGroundEpsilon.f [variable, in Coq.Logic.ConstructiveEpsilon]
ConstructiveGroundEpsilon.g [variable, in Coq.Logic.ConstructiveEpsilon]
ConstructiveGroundEpsilon.gof_eq_id [variable, in Coq.Logic.ConstructiveEpsilon]
ConstructiveGroundEpsilon.P [variable, in Coq.Logic.ConstructiveEpsilon]
ConstructiveGroundEpsilon.P_decidable [variable, in Coq.Logic.ConstructiveEpsilon]
ConstructiveIndefiniteDescription [abbreviation, in Coq.Logic.ChoiceFacts]
ConstructiveIndefiniteDescription_on [definition, in Coq.Logic.ChoiceFacts]
ConstructiveIndefiniteGroundDescription_Acc.R [variable, in Coq.Logic.ConstructiveEpsilon]
ConstructiveIndefiniteGroundDescription_Acc.P_decidable [variable, in Coq.Logic.ConstructiveEpsilon]
ConstructiveIndefiniteGroundDescription_Acc.P [variable, in Coq.Logic.ConstructiveEpsilon]
ConstructiveIndefiniteGroundDescription_Acc [section, in Coq.Logic.ConstructiveEpsilon]
ConstructiveIndefiniteGroundDescription_Direct.P_dec [variable, in Coq.Logic.ConstructiveEpsilon]
ConstructiveIndefiniteGroundDescription_Direct.P [variable, in Coq.Logic.ConstructiveEpsilon]
ConstructiveIndefiniteGroundDescription_Direct [section, in Coq.Logic.ConstructiveEpsilon]
ConstructiveLimits [library]
ConstructiveLUB [library]
ConstructiveMinMax [library]
ConstructivePower [library]
ConstructiveRcomplete [library]
ConstructiveReals [record, in Coq.Reals.Abstract.ConstructiveReals]
ConstructiveReals [library]
ConstructiveRealsMorphism [record, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
ConstructiveRealsMorphisms [library]
ConstructiveSum [library]
constructive_epsilon [abbreviation, in Coq.Logic.ConstructiveEpsilon]
constructive_epsilon_spec [abbreviation, in Coq.Logic.ConstructiveEpsilon]
constructive_definite_description [abbreviation, in Coq.Logic.ConstructiveEpsilon]
constructive_indefinite_description [abbreviation, in Coq.Logic.ConstructiveEpsilon]
constructive_epsilon_nat [abbreviation, in Coq.Logic.ConstructiveEpsilon]
constructive_epsilon_spec_nat [abbreviation, in Coq.Logic.ConstructiveEpsilon]
constructive_indefinite_description_nat [abbreviation, in Coq.Logic.ConstructiveEpsilon]
constructive_ground_epsilon_spec [definition, in Coq.Logic.ConstructiveEpsilon]
constructive_ground_epsilon [definition, in Coq.Logic.ConstructiveEpsilon]
constructive_definite_ground_description [lemma, in Coq.Logic.ConstructiveEpsilon]
constructive_indefinite_ground_description [lemma, in Coq.Logic.ConstructiveEpsilon]
constructive_ground_epsilon_spec_nat [definition, in Coq.Logic.ConstructiveEpsilon]
constructive_ground_epsilon_nat [definition, in Coq.Logic.ConstructiveEpsilon]
constructive_indefinite_ground_description_nat_Acc [lemma, in Coq.Logic.ConstructiveEpsilon]
constructive_indefinite_ground_description_nat [definition, in Coq.Logic.ConstructiveEpsilon]
constructive_definite_description [lemma, in Coq.Logic.Epsilon]
constructive_indefinite_description [lemma, in Coq.Logic.Epsilon]
constructive_definite_description [lemma, in Coq.Logic.ClassicalEpsilon]
constructive_indefinite_description [axiom, in Coq.Logic.ClassicalEpsilon]
constructive_definite_descr_excluded_middle [lemma, in Coq.Logic.ChoiceFacts]
constructive_definite_descr_fun_reification [lemma, in Coq.Logic.ChoiceFacts]
constructive_indefinite_descr_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
constructive_indefinite_description_and_small_drinker_iff_epsilon [lemma, in Coq.Logic.ChoiceFacts]
constructive_indefinite_description_and_small_drinker_imp_epsilon [lemma, in Coq.Logic.ChoiceFacts]
constructive_definite_description [lemma, in Coq.Logic.IndefiniteDescription]
constructive_indefinite_description [axiom, in Coq.Logic.IndefiniteDescription]
constructive_indefinite_ground_description_Z [lemma, in Coq.Reals.Cauchy.ConstructiveExtra]
constructive_definite_description [axiom, in Coq.Logic.Description]
Constructive_sets [library]
const_nth [lemma, in Coq.Vectors.VectorSpec]
cons_inj [definition, in Coq.Vectors.VectorSpec]
cons_seq [lemma, in Coq.Lists.List]
cons_sort [abbreviation, in Coq.Sorting.Sorted]
cons_leA [abbreviation, in Coq.Sorting.Sorted]
cons_ORlist [definition, in Coq.Reals.RList]
cons_id [definition, in Coq.micromega.Tauto]
contains [definition, in Coq.Sets.Relations_1]
contains_is_preorder [lemma, in Coq.Sets.Relations_1_facts]
contents [projection, in Coq.rtauto.Bintree]
contents [definition, in Coq.Sorting.Heap]
continue_in [definition, in Coq.Reals.Rderiv]
continuity [definition, in Coq.Reals.Ranalysis1]
continuity_comp [lemma, in Coq.Reals.Ranalysis1]
continuity_div [lemma, in Coq.Reals.Ranalysis1]
continuity_inv [lemma, in Coq.Reals.Ranalysis1]
continuity_scal [lemma, in Coq.Reals.Ranalysis1]
continuity_const [lemma, in Coq.Reals.Ranalysis1]
continuity_mult [lemma, in Coq.Reals.Ranalysis1]
continuity_minus [lemma, in Coq.Reals.Ranalysis1]
continuity_opp [lemma, in Coq.Reals.Ranalysis1]
continuity_plus [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_comp [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_div [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_inv [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_scal [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_const [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_mult [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_minus [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_opp [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_plus [lemma, in Coq.Reals.Ranalysis1]
continuity_pt_locally_ext [lemma, in Coq.Reals.Ranalysis1]
continuity_pt [definition, in Coq.Reals.Ranalysis1]
continuity_pt_sqrt [lemma, in Coq.Reals.Sqrt_reg]
continuity_sin [lemma, in Coq.Reals.Rtrigo_reg]
continuity_cos [lemma, in Coq.Reals.Rtrigo1]
continuity_finite_sum [lemma, in Coq.Reals.Ranalysis4]
continuity_seq [lemma, in Coq.Reals.Rsqrt_def]
continuity_implies_RiemannInt [lemma, in Coq.Reals.RiemannInt]
continuity_ab_min [lemma, in Coq.Reals.Rtopology]
continuity_ab_maj [lemma, in Coq.Reals.Rtopology]
continuity_compact [lemma, in Coq.Reals.Rtopology]
continuity_P3 [lemma, in Coq.Reals.Rtopology]
continuity_P2 [lemma, in Coq.Reals.Rtopology]
continuity_P1 [lemma, in Coq.Reals.Rtopology]
continuity_pt_finite_SF [lemma, in Coq.Reals.PSeries_reg]
continuity_pt_recip_interv [lemma, in Coq.Reals.Ranalysis5]
continuity_pt_recip_prelim [lemma, in Coq.Reals.Ranalysis5]
continuous_neq_0 [lemma, in Coq.Reals.Ranalysis2]
contra [lemma, in Coq.ssr.ssrbool]
contraFF [lemma, in Coq.ssr.ssrbool]
contraFN [lemma, in Coq.ssr.ssrbool]
contraFnot [lemma, in Coq.ssr.ssrbool]
contraFT [lemma, in Coq.ssr.ssrbool]
contraL [lemma, in Coq.ssr.ssrbool]
contraLR [lemma, in Coq.ssr.ssrbool]
contraNF [lemma, in Coq.ssr.ssrbool]
contraNN [definition, in Coq.ssr.ssrbool]
contraNnot [lemma, in Coq.ssr.ssrbool]
contraNT [definition, in Coq.ssr.ssrbool]
contraPF [lemma, in Coq.ssr.ssrbool]
contraPN [lemma, in Coq.ssr.ssrbool]
contraPnot [lemma, in Coq.ssr.ssrbool]
contrapositive [lemma, in Coq.Logic.Decidable]
contraPT [lemma, in Coq.ssr.ssrbool]
contraR [lemma, in Coq.ssr.ssrbool]
contraT [lemma, in Coq.ssr.ssrbool]
contraTF [lemma, in Coq.ssr.ssrbool]
contraTN [definition, in Coq.ssr.ssrbool]
contraTnot [lemma, in Coq.ssr.ssrbool]
contraTT [definition, in Coq.ssr.ssrbool]
contra_notF [lemma, in Coq.ssr.ssrbool]
contra_notN [lemma, in Coq.ssr.ssrbool]
contra_notT [lemma, in Coq.ssr.ssrbool]
contra_not [lemma, in Coq.ssr.ssrbool]
Control [library]
cont_deriv [lemma, in Coq.Reals.Rderiv]
cont1 [projection, in Coq.Reals.RiemannInt]
cont:102 [binder, in Coq.FSets.FMapAVL]
cont:106 [binder, in Coq.FSets.FMapAVL]
cont:1254 [binder, in Coq.FSets.FMapAVL]
cont:1261 [binder, in Coq.FSets.FMapAVL]
cont:1511 [binder, in Coq.FSets.FMapAVL]
cont:1515 [binder, in Coq.FSets.FMapAVL]
cont:1537 [binder, in Coq.FSets.FMapAVL]
cont:1544 [binder, in Coq.FSets.FMapAVL]
cont:358 [binder, in Coq.MSets.MSetGenTree]
cont:364 [binder, in Coq.MSets.MSetGenTree]
cont:54 [binder, in Coq.MSets.MSetGenTree]
cont:58 [binder, in Coq.MSets.MSetGenTree]
Converse [section, in Coq.Relations.Relation_Operators]
Converse.A [variable, in Coq.Relations.Relation_Operators]
Converse.R [variable, in Coq.Relations.Relation_Operators]
COpp [constructor, in Coq.micromega.RMicromega]
copp:301 [binder, in Coq.setoid_ring.Ring_theory]
copy [axiom, in Coq.Array.PArray]
Coq [module, in Coq.Compat.Coq813]
CoqCast [abbreviation, in Coq.ssr.ssreflect]
CoqGenericDependentIf [abbreviation, in Coq.ssr.ssreflect]
CoqGenericIf [abbreviation, in Coq.ssr.ssreflect]
Coq.omega [module, in Coq.Compat.Coq813]
Coq.omega.Omega [module, in Coq.Compat.Coq813]
Coq811 [library]
Coq812 [library]
Coq813 [library]
Coq814 [library]
Corollaries [section, in Coq.Logic.EqdepFacts]
Corollaries.U [variable, in Coq.Logic.EqdepFacts]
cos [definition, in Coq.Reals.Rtrigo_def]
COS [lemma, in Coq.Reals.Rtrigo1]
cosd [definition, in Coq.Reals.Rtrigo_calc]
cosh [definition, in Coq.Reals.Rtrigo_def]
cosh_0 [lemma, in Coq.Reals.Rtrigo_def]
cosn_no_R0 [lemma, in Coq.Reals.Rtrigo_def]
cos_0 [lemma, in Coq.Reals.Rtrigo_def]
cos_sym [lemma, in Coq.Reals.Rtrigo_def]
cos_in [definition, in Coq.Reals.Rtrigo_def]
cos_n [definition, in Coq.Reals.Rtrigo_def]
cos_pi_plus [lemma, in Coq.Reals.Rtrigo_facts]
cos_pi_minus [lemma, in Coq.Reals.Rtrigo_facts]
cos_tan [lemma, in Coq.Reals.Rtrigo_facts]
cos_sin_Rabs [lemma, in Coq.Reals.Rtrigo_facts]
cos_sin_opp [lemma, in Coq.Reals.Rtrigo_facts]
cos_sin [lemma, in Coq.Reals.Rtrigo_facts]
cos_eq_0_2PI_1 [lemma, in Coq.Reals.Rtrigo1]
cos_eq_0_2PI_0 [lemma, in Coq.Reals.Rtrigo1]
cos_eq_0_1 [lemma, in Coq.Reals.Rtrigo1]
cos_eq_0_0 [lemma, in Coq.Reals.Rtrigo1]
cos_decr_1 [lemma, in Coq.Reals.Rtrigo1]
cos_decr_0 [lemma, in Coq.Reals.Rtrigo1]
cos_incr_1 [lemma, in Coq.Reals.Rtrigo1]
cos_incr_0 [lemma, in Coq.Reals.Rtrigo1]
cos_inj [lemma, in Coq.Reals.Rtrigo1]
cos_decreasing_1 [lemma, in Coq.Reals.Rtrigo1]
cos_decreasing_0 [lemma, in Coq.Reals.Rtrigo1]
cos_increasing_1 [lemma, in Coq.Reals.Rtrigo1]
cos_increasing_0 [lemma, in Coq.Reals.Rtrigo1]
cos_ge_0_3PI2 [lemma, in Coq.Reals.Rtrigo1]
cos_lt_0 [lemma, in Coq.Reals.Rtrigo1]
cos_le_0 [lemma, in Coq.Reals.Rtrigo1]
cos_ge_0 [lemma, in Coq.Reals.Rtrigo1]
cos_gt_0 [lemma, in Coq.Reals.Rtrigo1]
cos_ub [definition, in Coq.Reals.Rtrigo1]
cos_lb [definition, in Coq.Reals.Rtrigo1]
cos_sin_0_var [lemma, in Coq.Reals.Rtrigo1]
cos_sin_0 [lemma, in Coq.Reals.Rtrigo1]
COS_bound [lemma, in Coq.Reals.Rtrigo1]
cos_sin [lemma, in Coq.Reals.Rtrigo1]
cos_shift [lemma, in Coq.Reals.Rtrigo1]
cos_period [lemma, in Coq.Reals.Rtrigo1]
cos_2PI [lemma, in Coq.Reals.Rtrigo1]
cos_3PI2 [lemma, in Coq.Reals.Rtrigo1]
cos_neg [lemma, in Coq.Reals.Rtrigo1]
cos_2a_sin [lemma, in Coq.Reals.Rtrigo1]
cos_2a_cos [lemma, in Coq.Reals.Rtrigo1]
cos_2a [lemma, in Coq.Reals.Rtrigo1]
cos_bound [lemma, in Coq.Reals.Rtrigo1]
cos_PI [lemma, in Coq.Reals.Rtrigo1]
cos_PI2 [lemma, in Coq.Reals.Rtrigo1]
cos_minus [lemma, in Coq.Reals.Rtrigo1]
cos_pi2 [lemma, in Coq.Reals.Rtrigo1]
cos_approx [definition, in Coq.Reals.Rtrigo_alt]
cos_term [definition, in Coq.Reals.Rtrigo_alt]
cos_acos [lemma, in Coq.Reals.Ratan]
cos_asin [lemma, in Coq.Reals.Ratan]
cos_atan [lemma, in Coq.Reals.Ratan]
cos_5PI4 [lemma, in Coq.Reals.Rtrigo_calc]
cos_2PI3 [lemma, in Coq.Reals.Rtrigo_calc]
cos_PI3 [lemma, in Coq.Reals.Rtrigo_calc]
cos_PI6 [lemma, in Coq.Reals.Rtrigo_calc]
cos_3PI4 [lemma, in Coq.Reals.Rtrigo_calc]
cos_PI4 [lemma, in Coq.Reals.Rtrigo_calc]
cos_plus_form [lemma, in Coq.Reals.Cos_rel]
cos_plus [lemma, in Coq.Reals.Cos_plus]
Cos_plus [library]
Cos_rel [library]
cos2 [lemma, in Coq.Reals.Rtrigo1]
cos2_bound [lemma, in Coq.Reals.Rtrigo_facts]
cos3PI4 [abbreviation, in Coq.Reals.Rtrigo_calc]
count_occ_sgt [lemma, in Coq.Lists.List]
count_occ_repeat_excl [lemma, in Coq.Lists.List]
count_occ_unique [lemma, in Coq.Lists.List]
count_occ_repeat_neq [lemma, in Coq.Lists.List]
count_occ_repeat_eq [lemma, in Coq.Lists.List]
count_occ_alt [lemma, in Coq.Lists.List]
count_occ' [definition, in Coq.Lists.List]
count_occ_map [lemma, in Coq.Lists.List]
count_occ_bound [lemma, in Coq.Lists.List]
count_occ_elt_neq [lemma, in Coq.Lists.List]
count_occ_elt_eq [lemma, in Coq.Lists.List]
count_occ_app [lemma, in Coq.Lists.List]
count_occ_cons_neq [lemma, in Coq.Lists.List]
count_occ_cons_eq [lemma, in Coq.Lists.List]
count_occ_inv_nil [lemma, in Coq.Lists.List]
count_occ_nil [lemma, in Coq.Lists.List]
count_occ_not_In [lemma, in Coq.Lists.List]
count_occ_In [lemma, in Coq.Lists.List]
count_occ [definition, in Coq.Lists.List]
Couple [inductive, in Coq.Sets.Ensembles]
Couple_inv [lemma, in Coq.Sets.Constructive_sets]
Couple_r [constructor, in Coq.Sets.Ensembles]
Couple_l [constructor, in Coq.Sets.Ensembles]
Couple_as_union [lemma, in Coq.Sets.Powerset_facts]
covering [definition, in Coq.Reals.Rtopology]
covering_finite [definition, in Coq.Reals.Rtopology]
covering_open_set [definition, in Coq.Reals.Rtopology]
covers [inductive, in Coq.Sets.Partial_Order]
covers_is_Add [lemma, in Coq.Sets.Powerset_Classical_facts]
covers_Add [lemma, in Coq.Sets.Powerset_Classical_facts]
co_interval [definition, in Coq.Reals.RiemannInt_SF]
cO:296 [binder, in Coq.setoid_ring.Ring_theory]
cperm [constructor, in Coq.Sorting.CPermutation]
CPermutation [inductive, in Coq.Sorting.CPermutation]
CPermutation [section, in Coq.Sorting.CPermutation]
CPermutation [library]
CPermutation_rewrite_rev [definition, in Coq.Sorting.CPermutation]
CPermutation_Forall2 [lemma, in Coq.Sorting.CPermutation]
CPermutation_Exists [instance, in Coq.Sorting.CPermutation]
CPermutation_Forall [instance, in Coq.Sorting.CPermutation]
CPermutation_image [lemma, in Coq.Sorting.CPermutation]
CPermutation_map_inv [lemma, in Coq.Sorting.CPermutation]
CPermutation_map [instance, in Coq.Sorting.CPermutation]
CPermutation_in' [instance, in Coq.Sorting.CPermutation]
CPermutation_in [instance, in Coq.Sorting.CPermutation]
CPermutation_rev [instance, in Coq.Sorting.CPermutation]
CPermutation_vs_cons_inv [lemma, in Coq.Sorting.CPermutation]
CPermutation_vs_elt_inv [lemma, in Coq.Sorting.CPermutation]
CPermutation_length_2_inv [lemma, in Coq.Sorting.CPermutation]
CPermutation_length_2 [lemma, in Coq.Sorting.CPermutation]
CPermutation_swap [lemma, in Coq.Sorting.CPermutation]
CPermutation_length_1_inv [lemma, in Coq.Sorting.CPermutation]
CPermutation_length_1 [lemma, in Coq.Sorting.CPermutation]
CPermutation_morph_cons [lemma, in Coq.Sorting.CPermutation]
CPermutation_cons_append [lemma, in Coq.Sorting.CPermutation]
CPermutation_app_rot [lemma, in Coq.Sorting.CPermutation]
CPermutation_app_comm [lemma, in Coq.Sorting.CPermutation]
CPermutation_app [lemma, in Coq.Sorting.CPermutation]
CPermutation_properties.B [variable, in Coq.Sorting.CPermutation]
CPermutation_properties.A [variable, in Coq.Sorting.CPermutation]
CPermutation_properties [section, in Coq.Sorting.CPermutation]
CPermutation_Equivalence [instance, in Coq.Sorting.CPermutation]
CPermutation_trans [lemma, in Coq.Sorting.CPermutation]
CPermutation_sym [lemma, in Coq.Sorting.CPermutation]
CPermutation_refl' [instance, in Coq.Sorting.CPermutation]
CPermutation_refl [lemma, in Coq.Sorting.CPermutation]
CPermutation_split [lemma, in Coq.Sorting.CPermutation]
CPermutation_nil_app_cons [lemma, in Coq.Sorting.CPermutation]
CPermutation_nil_cons [lemma, in Coq.Sorting.CPermutation]
CPermutation_nil [lemma, in Coq.Sorting.CPermutation]
CPermutation_Permutation [instance, in Coq.Sorting.CPermutation]
CPermutation.A [variable, in Coq.Sorting.CPermutation]
CPlus [constructor, in Coq.micromega.RMicromega]
Cpo [record, in Coq.Sets.Cpo]
Cpo [library]
CPow [constructor, in Coq.micromega.RMicromega]
CPowR0 [definition, in Coq.micromega.RMicromega]
Cpo_cond [projection, in Coq.Sets.Cpo]
CQ [constructor, in Coq.micromega.RMicromega]
CRabs [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRabs_def [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRabs_def2 [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_def1 [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_lt [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_mult [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_appart_0 [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_pos [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_triang_inv2 [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_triang_inv [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_le [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_triang [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_left [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_minus_sym [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_opp [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_right [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRabs_morph [instance, in Coq.Reals.Abstract.ConstructiveAbs]
CRapart [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRapart_morph [instance, in Coq.Reals.Abstract.ConstructiveReals]
CRcarrier [projection, in Coq.Reals.Abstract.ConstructiveReals]
CReal [record, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealAbsLUB [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CRealArchimedean [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CRealComplete [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CRealConstructive [definition, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CRealEq [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealEq_relT [instance, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealEq_trans [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealEq_sym [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealEq_refl [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealEq_diff [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealGe [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealGt [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealGt_morph [instance, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLe [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLe_0R_to_single_dist [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CRealLe_proper_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLe_proper_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLe_refl [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLe_not_lt [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLowerBound [definition, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CRealLowerBoundSpec [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CRealLowerBound_lt_scale [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CRealLt [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLtDisjunctEpsilon [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CRealLtEpsilon [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLtForget [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLtIsLinear [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CRealLtProp [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_RQ_to_single_dist [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CRealLt_QR_to_single_dist [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CRealLt_QR_from_single_dist [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CRealLt_RQ_from_single_dist [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CRealLt_0_1 [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_proper_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_proper_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_morph [instance, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_dec [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_irrefl [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_asym [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_above_same [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_above [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_aboveSig' [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_aboveSig [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_lpo_dec [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CRealQ_dense [definition, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_from_cauchy [definition, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_from_cauchy_bound [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_from_cauchy_scale [definition, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_from_cauchy_seq_bound [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_abs_Qabs_diff [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_abs_Qabs_seq [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_abs_Qabs [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_abs_upper_bound [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_from_cauchy_cauchy [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_from_cauchy_seq [definition, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_from_cauchy_cm_mono [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_from_cauchy_cm [definition, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_cv_self' [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_cv_self [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
CReal_min_contract [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_contract [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_lub_lt [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_assoc [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_max_mult_neg [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_assoc [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_lt [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_plus [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_plus [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_mult [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_sym [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_sym [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_lt_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_right [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_left [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_right [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_left [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_glb [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_lub [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_double [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max [definition, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min [definition, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_def2 [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_mult [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_gt [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_triang_inv2 [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_triang_inv [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_triang [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_lt [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_minus_sym [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_le [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_appart_0 [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_left [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_opp [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_pos [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_le_abs [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_right [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs [definition, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_bound [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_cauchy [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_scale [definition, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_seq [definition, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_opp_ge_le_contravar [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_gt_lt_contravar [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_involutive [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_plus_distr [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_0 [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_eq_reg_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_morph_T [instance, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_proper_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_proper_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_opp_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_opp_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_le_compat [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_le_lt_compat [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_le_compat_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_le_reg_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_le_reg_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_lt_reg_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_lt_reg_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_lt_compat_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_lt_compat_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_0_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_0_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_comm [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_assoc [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_red_seq [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_minus [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_bound [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_cauchy [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_scale [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_seq [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_bound [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_cauchy [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_scale [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_seq [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_injectQPos [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_appart_morph [instance, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_lt_trans [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_le_trans [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_lt_le_trans [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_le_lt_trans [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_appart [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
CReal_mult_le_reg_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_le_reg_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_le_compat_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_le_compat_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_le_0_compat [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_invQ [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_le_compat_l_half [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_pos_appart_zero [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_eq_compat_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_eq_compat_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_eq_reg_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_lt_reg_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_lt_reg_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_mult_distr [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_1 [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_l_pos [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_0_lt_compat [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv [definition, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_neg_lt_pos [definition, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_pos [definition, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_pos_bound [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_pos_cauchy [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_pos_scale [definition, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_pos_seq [definition, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_pos_cm [definition, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_abs_appart_zero [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_eq_reg_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_lt_compat_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_lt_compat_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_opp_mult_distr_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_1_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_minus_morph_T [instance, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_opp_morph_T [instance, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_morph_T [instance, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_isRing [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_isRingExt [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_1_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_assoc [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_proper_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_proper_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_opp_mult_distr_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_plus_distr_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_plus_distr_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_lt_0_compat [definition, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_lt_0_compat_correct [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_scale_sep0_limit [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_0_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_0_r [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_proper_0_l [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_red_scale [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_comm [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult [definition, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_bound [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_cauchy [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_scale [definition, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_seq [definition, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_of_DReal_bound [lemma, in Coq.Reals.ClassicalDedekindReals]
CReal_of_DReal_scale [definition, in Coq.Reals.ClassicalDedekindReals]
CReal_of_DReal_seq_bound [lemma, in Coq.Reals.ClassicalDedekindReals]
CReal_of_DReal_seq_max_prec_1 [lemma, in Coq.Reals.ClassicalDedekindReals]
CReal_of_DReal_cauchy [lemma, in Coq.Reals.ClassicalDedekindReals]
CReal_of_DReal_seq [definition, in Coq.Reals.ClassicalDedekindReals]
crelation [definition, in Coq.Classes.CRelationClasses]
CRelationClasses [library]
CReq [projection, in Coq.Reals.Abstract.ConstructiveReals]
CReq_relT [instance, in Coq.Reals.Abstract.ConstructiveReals]
CReq_trans [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CReq_sym [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CReq_refl [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRfloor [definition, in Coq.Reals.Abstract.ConstructiveReals]
cring [section, in Coq.setoid_ring.Cring]
Cring [record, in Coq.setoid_ring.Cring]
Cring [inductive, in Coq.setoid_ring.Cring]
Cring [library]
cring_div_theory [lemma, in Coq.setoid_ring.Cring]
cring_power_theory [lemma, in Coq.setoid_ring.Cring]
cring_morph [lemma, in Coq.setoid_ring.Cring]
cring_almost_ring_theory [lemma, in Coq.setoid_ring.Cring]
cring_eq_ext [lemma, in Coq.setoid_ring.Cring]
cring_mul_comm [projection, in Coq.setoid_ring.Cring]
cring_mul_comm [constructor, in Coq.setoid_ring.Cring]
CRinv [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRinv_morph [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRinv_mult_distr [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRinv_1 [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRinv_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRinv_0_lt_compat [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRinv_l [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRisRing [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRisRingExt [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRis_upper_bound [definition, in Coq.Reals.Abstract.ConstructiveLUB]
CRle [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRle_minus [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRle_trans [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRle_lt_trans [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRle_refl [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRle_abs [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CRlt [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRltDisjunctEpsilon [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRltEpsilon [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRltForget [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRltLinear [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRltProp [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRlt_minus [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRlt_morph [instance, in Coq.Reals.Abstract.ConstructiveReals]
CRlt_trans_flip [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRlt_trans [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRlt_le_trans [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRlt_proper [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRlt_asym [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRlt_lpo_dec [lemma, in Coq.Reals.Abstract.ConstructiveLUB]
CRlt_max [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRlt_min [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax [definition, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax_mult [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax_min_mult_neg [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax_assoc [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax_lub_lt [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax_contract [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax_right [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax_left [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax_plus [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax_sym [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax_r [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax_l [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax_lub [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmax_morphT [instance, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin [definition, in Coq.Reals.Abstract.ConstructiveMinMax]
CRminus [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRminus_morph_T [instance, in Coq.Reals.Abstract.ConstructiveReals]
CRmin_max_mult_neg [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin_assoc [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin_glb [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin_contract [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin_lt [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin_right [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin_left [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin_plus [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin_mult [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin_sym [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin_r [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin_l [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin_morphT [instance, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmin_lt_r [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmorph [projection, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_series_cv [lemma, in Coq.Reals.Abstract.ConstructiveSum]
CRmorph_INR [lemma, in Coq.Reals.Abstract.ConstructiveSum]
CRmorph_sum [lemma, in Coq.Reals.Abstract.ConstructiveSum]
CRmorph_min [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRmorph_cauchy_reverse [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_cv [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_abs [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_rat_cv [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_inv [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_appart_zero [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_appart [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult_pos_pos [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult_pos_pos_le [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult_rat [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult_inv [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult_int [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult_pos [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_plus [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_plus_rat [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_opp [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_one [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_zero [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_le_inv [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_le [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_compose [definition, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_proper [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_unique [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_increasing_inv [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_increasing [projection, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_rat [projection, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRmult [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_appart_reg_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_appart_reg_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_le_reg_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_le_reg_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_pos_appart_zero [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_pos_pos [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_le_compat_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_le_compat_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_le_0_compat [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_eq_reg_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_eq_reg_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_le_compat_r_half [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_le_compat_l_half [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_lt_reg_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_lt_reg_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_lt_compat_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_lt_compat_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_0_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_0_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_plus_distr_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_plus_distr_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_comm [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_assoc [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_1_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_1_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_morph_T [instance, in Coq.Reals.Abstract.ConstructiveReals]
CRmult_lt_0_compat [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRnegPartAbsMin [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRopp [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRopp_mult_distr_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRopp_mult_distr_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRopp_plus_distr [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRopp_ge_le_contravar [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRopp_lt_cancel [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRopp_gt_lt_contravar [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRopp_involutive [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRopp_morph_T [instance, in Coq.Reals.Abstract.ConstructiveReals]
CRopp_0 [lemma, in Coq.Reals.Abstract.ConstructiveReals]
cross_product_eq [lemma, in Coq.setoid_ring.Field_theory]
CRplus [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_appart_reg_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_appart_reg_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_morph_T [instance, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_comm [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_assoc [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_eq_reg_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_eq_reg_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_le_lt_compat [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_lt_le_compat [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_le_reg_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_le_reg_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_le_compat [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_le_compat_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_le_compat_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_lt_reg_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_lt_compat_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_opp_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_opp_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_0_r [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_0_l [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_lt_reg_l [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_lt_compat_l [projection, in Coq.Reals.Abstract.ConstructiveReals]
CRplus_neg_rat_lt [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRplus_pos_rat_lt [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CRposPartAbsMax [lemma, in Coq.Reals.Abstract.ConstructiveMinMax]
CRpow [definition, in Coq.Reals.Abstract.ConstructivePower]
CRpow_plus_distr [lemma, in Coq.Reals.Abstract.ConstructivePower]
CRpow_inv [lemma, in Coq.Reals.Abstract.ConstructivePower]
CRpow_proper [lemma, in Coq.Reals.Abstract.ConstructivePower]
CRpow_one [lemma, in Coq.Reals.Abstract.ConstructivePower]
CRpow_mult [lemma, in Coq.Reals.Abstract.ConstructivePower]
CRpow_gt_zero [lemma, in Coq.Reals.Abstract.ConstructivePower]
CRpow_ge_zero [lemma, in Coq.Reals.Abstract.ConstructivePower]
CRpow_ge_one [lemma, in Coq.Reals.Abstract.ConstructivePower]
CRsum [definition, in Coq.Reals.Abstract.ConstructiveSum]
CRsum_eq [lemma, in Coq.Reals.Abstract.ConstructiveSum]
CRup_nat [definition, in Coq.Reals.Abstract.ConstructiveReals]
CRzero_double [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CRzero_lt_one [projection, in Coq.Reals.Abstract.ConstructiveReals]
CR_of_Q_inv [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CR_of_Q_pos [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CR_of_Q_opp [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CR_of_Q_morph_T [instance, in Coq.Reals.Abstract.ConstructiveReals]
CR_of_Q_le [lemma, in Coq.Reals.Abstract.ConstructiveReals]
CR_complete [projection, in Coq.Reals.Abstract.ConstructiveReals]
CR_cauchy [projection, in Coq.Reals.Abstract.ConstructiveReals]
CR_cv [projection, in Coq.Reals.Abstract.ConstructiveReals]
CR_archimedean [projection, in Coq.Reals.Abstract.ConstructiveReals]
CR_Q_dense [projection, in Coq.Reals.Abstract.ConstructiveReals]
CR_of_Q_mult [projection, in Coq.Reals.Abstract.ConstructiveReals]
CR_of_Q_plus [projection, in Coq.Reals.Abstract.ConstructiveReals]
CR_of_Q_lt [projection, in Coq.Reals.Abstract.ConstructiveReals]
CR_of_Q [projection, in Coq.Reals.Abstract.ConstructiveReals]
CR_sig_lub [lemma, in Coq.Reals.Abstract.ConstructiveLUB]
CR_double [lemma, in Coq.Reals.Abstract.ConstructivePower]
CR_of_Q_abs [lemma, in Coq.Reals.Abstract.ConstructiveAbs]
CR_cv_shift' [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_shift [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_dist_cont [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_abs_cont [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_le [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_bound_up [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_bound_down [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_open_above [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_open_below [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_growing_transit [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_const [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_scale [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_nonneg [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_minus [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_morph [instance, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_proper [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cauchy_eq [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_eq [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_unique [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_plus [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_opp [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_cv_extens [lemma, in Coq.Reals.Abstract.ConstructiveLimits]
CR_Q_limit_cv [lemma, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
CR_Q_limit [definition, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
Cr:161 [binder, in Coq.setoid_ring.Ncring]
Cst [constructor, in Coq.micromega.Ztac]
Cst [constructor, in Coq.btauto.Algebra]
cstlist [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
CstOp [record, in Coq.micromega.ZifyClasses]
cstr [projection, in Coq.micromega.ZifyClasses]
csub:300 [binder, in Coq.setoid_ring.Ring_theory]
ctx [definition, in Coq.rtauto.Rtauto]
curry [definition, in Coq.Init.Datatypes]
Cut [constructor, in Coq.rtauto.Rtauto]
CutProof [constructor, in Coq.micromega.ZMicromega]
Cutting [section, in Coq.Lists.List]
CuttingMap [section, in Coq.Lists.List]
CuttingMap.A [variable, in Coq.Lists.List]
CuttingMap.B [variable, in Coq.Lists.List]
CuttingMap.f [variable, in Coq.Lists.List]
cutting_plane_sound [lemma, in Coq.micromega.ZMicromega]
Cutting.A [variable, in Coq.Lists.List]
CVN_R_sin [lemma, in Coq.Reals.Rtrigo_reg]
CVN_R_cos [lemma, in Coq.Reals.Rtrigo1]
CVN_R_CVS [lemma, in Coq.Reals.PSeries_reg]
CVN_CVU [lemma, in Coq.Reals.PSeries_reg]
CVN_R [definition, in Coq.Reals.PSeries_reg]
CVN_r [definition, in Coq.Reals.PSeries_reg]
CVU [definition, in Coq.Reals.PSeries_reg]
CVU_derivable [lemma, in Coq.Reals.PSeries_reg]
CVU_ext_lim [lemma, in Coq.Reals.PSeries_reg]
CVU_cv [lemma, in Coq.Reals.PSeries_reg]
CVU_continuity [lemma, in Coq.Reals.PSeries_reg]
CV_shift' [lemma, in Coq.Reals.Rseries]
CV_shift [lemma, in Coq.Reals.Rseries]
cv_pow_half [lemma, in Coq.Reals.Rsqrt_def]
cv_dicho [lemma, in Coq.Reals.Rsqrt_def]
CV_ALT [lemma, in Coq.Reals.AltSeries]
CV_ALT_step4 [lemma, in Coq.Reals.AltSeries]
CV_ALT_step3 [lemma, in Coq.Reals.AltSeries]
CV_ALT_step2 [lemma, in Coq.Reals.AltSeries]
CV_ALT_step1 [lemma, in Coq.Reals.AltSeries]
CV_ALT_step0 [lemma, in Coq.Reals.AltSeries]
cv_cauchy_2 [lemma, in Coq.Reals.PartSum]
cv_cauchy_1 [lemma, in Coq.Reals.PartSum]
cv_speed_pow_fact [lemma, in Coq.Reals.SeqProp]
cv_infty_cv_R0 [lemma, in Coq.Reals.SeqProp]
cv_infty [definition, in Coq.Reals.SeqProp]
CV_minus [lemma, in Coq.Reals.SeqProp]
CV_opp [lemma, in Coq.Reals.SeqProp]
CV_mult [lemma, in Coq.Reals.SeqProp]
CV_Cauchy [lemma, in Coq.Reals.SeqProp]
cv_cvabs [lemma, in Coq.Reals.SeqProp]
CV_plus [lemma, in Coq.Reals.SeqProp]
cv:121 [binder, in Coq.Reals.PSeries_reg]
cv:130 [binder, in Coq.Reals.PSeries_reg]
cv:65 [binder, in Coq.Reals.PSeries_reg]
cv:72 [binder, in Coq.Reals.PSeries_reg]
CyclicAxioms [library]
CyclicRing [module, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.add_opp_diag_r [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.add_opp_r [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.add_assoc [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.add_comm [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.add_0_l [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.CyclicRing [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.eq [definition, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.eqb [definition, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.eqb_correct [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.eqb_eq [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.mul_add_distr_r [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.mul_assoc [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.mul_comm [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.mul_1_l [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.wB [abbreviation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
_ * _ [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
_ - _ [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
_ + _ [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
_ == _ [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
- _ [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
0 [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
1 [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
[| _ |] [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicType [module, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicType.ops [instance, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicType.specs [instance, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicType.t [axiom, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Cyclic31 [library]
Cyclic63 [library]
CZ [constructor, in Coq.micromega.RMicromega]
C_maj [lemma, in Coq.Reals.Rprod]
c':114 [binder, in Coq.Init.Datatypes]
c':119 [binder, in Coq.Init.Datatypes]
c':121 [binder, in Coq.Init.Datatypes]
c':173 [binder, in Coq.setoid_ring.Ring_theory]
c':222 [binder, in Coq.setoid_ring.Ring_polynom]
c':225 [binder, in Coq.micromega.EnvRing]
c':252 [binder, in Coq.PArith.BinPos]
c':36 [binder, in Coq.setoid_ring.Field_theory]
C0 [abbreviation, in Coq.Numbers.Cyclic.Abstract.DoubleType]
C0 [constructor, in Coq.Numbers.Cyclic.Abstract.CarryType]
C0 [constructor, in Coq.micromega.RMicromega]
c0:339 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c0:342 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c0:345 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c0:403 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c0:406 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c0:410 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c0:414 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
C0:510 [binder, in Coq.Reals.RiemannInt]
C0:517 [binder, in Coq.Reals.RiemannInt]
C0:531 [binder, in Coq.Reals.RiemannInt]
c1 [projection, in Coq.Reals.RiemannInt]
C1 [abbreviation, in Coq.Numbers.Cyclic.Abstract.DoubleType]
C1 [constructor, in Coq.Numbers.Cyclic.Abstract.CarryType]
C1 [constructor, in Coq.micromega.RMicromega]
C1 [definition, in Coq.Reals.Cos_rel]
C1_fun [record, in Coq.Reals.RiemannInt]
C1_cvg [lemma, in Coq.Reals.Cos_rel]
c1:106 [binder, in Coq.omega.OmegaLemmas]
c1:115 [binder, in Coq.omega.OmegaLemmas]
c1:129 [binder, in Coq.omega.OmegaLemmas]
c1:20 [binder, in Coq.Reals.PSeries_reg]
c1:209 [binder, in Coq.micromega.ZMicromega]
c1:22 [binder, in Coq.Sets.Finite_sets_facts]
c1:321 [binder, in Coq.MSets.MSetGenTree]
c1:330 [binder, in Coq.MSets.MSetGenTree]
c1:34 [binder, in Coq.Sets.Finite_sets_facts]
c1:38 [binder, in Coq.ZArith.Zcompare]
c1:406 [binder, in Coq.setoid_ring.Field_theory]
c1:409 [binder, in Coq.setoid_ring.Field_theory]
c1:42 [binder, in Coq.omega.OmegaLemmas]
c1:43 [binder, in Coq.ZArith.Zcompare]
c1:49 [binder, in Coq.omega.OmegaLemmas]
c1:51 [binder, in Coq.Logic.ClassicalFacts]
c1:55 [binder, in Coq.Logic.ClassicalFacts]
c1:66 [binder, in Coq.Logic.ClassicalFacts]
c1:67 [binder, in Coq.omega.OmegaLemmas]
c1:69 [binder, in Coq.Logic.ClassicalFacts]
c1:72 [binder, in Coq.Logic.ClassicalFacts]
c1:76 [binder, in Coq.Logic.ClassicalFacts]
c1:79 [binder, in Coq.Logic.ClassicalFacts]
c1:85 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
c1:86 [binder, in Coq.Logic.ClassicalFacts]
c1:89 [binder, in Coq.Logic.ClassicalFacts]
c1:90 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
c2:107 [binder, in Coq.omega.OmegaLemmas]
c2:122 [binder, in Coq.omega.OmegaLemmas]
c2:130 [binder, in Coq.omega.OmegaLemmas]
c2:21 [binder, in Coq.Reals.PSeries_reg]
c2:211 [binder, in Coq.micromega.ZMicromega]
c2:24 [binder, in Coq.Sets.Finite_sets_facts]
c2:36 [binder, in Coq.Sets.Finite_sets_facts]
c2:39 [binder, in Coq.ZArith.Zcompare]
c2:407 [binder, in Coq.setoid_ring.Field_theory]
c2:410 [binder, in Coq.setoid_ring.Field_theory]
c2:43 [binder, in Coq.omega.OmegaLemmas]
c2:44 [binder, in Coq.ZArith.Zcompare]
c2:52 [binder, in Coq.Logic.ClassicalFacts]
c2:54 [binder, in Coq.omega.OmegaLemmas]
c2:56 [binder, in Coq.Logic.ClassicalFacts]
c2:67 [binder, in Coq.Logic.ClassicalFacts]
c2:68 [binder, in Coq.omega.OmegaLemmas]
c2:70 [binder, in Coq.Logic.ClassicalFacts]
c2:73 [binder, in Coq.Logic.ClassicalFacts]
c2:77 [binder, in Coq.Logic.ClassicalFacts]
c2:80 [binder, in Coq.Logic.ClassicalFacts]
c2:86 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
c2:87 [binder, in Coq.Logic.ClassicalFacts]
c2:90 [binder, in Coq.Logic.ClassicalFacts]
c2:91 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
c3:40 [binder, in Coq.ZArith.Zcompare]
c3:45 [binder, in Coq.ZArith.Zcompare]
C:1 [binder, in Coq.micromega.EnvRing]
c:1 [binder, in Coq.ZArith.Zwf]
c:1 [binder, in Coq.micromega.ZifyComparison]
C:1 [binder, in Coq.setoid_ring.Ncring_polynom]
c:10 [binder, in Coq.Reals.MVT]
c:10 [binder, in Coq.ssr.ssrbool]
c:10 [binder, in Coq.Reals.Machin]
c:10 [binder, in Coq.ZArith.Zwf]
C:10 [binder, in Coq.Sets.Powerset_facts]
c:100 [binder, in Coq.ZArith.Zquot]
c:101 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
c:101 [binder, in Coq.NArith.Ndec]
c:102 [binder, in Coq.setoid_ring.Ncring_polynom]
C:102 [binder, in Coq.Logic.ClassicalFacts]
c:103 [binder, in Coq.setoid_ring.Field_theory]
c:103 [binder, in Coq.ZArith.Zquot]
c:104 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
c:104 [binder, in Coq.NArith.Ndec]
C:1041 [binder, in Coq.Init.Specif]
c:105 [binder, in Coq.Reals.NewtonInt]
c:105 [binder, in Coq.setoid_ring.Ncring_polynom]
C:106 [binder, in Coq.Logic.ClassicalFacts]
c:107 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
c:107 [binder, in Coq.setoid_ring.Field_theory]
c:11 [binder, in Coq.Reals.MVT]
c:11 [binder, in Coq.ZArith.Zpow_facts]
c:110 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
c:110 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
C:1107 [binder, in Coq.Init.Specif]
c:111 [binder, in Coq.Reals.NewtonInt]
c:112 [binder, in Coq.ZArith.Znumtheory]
c:113 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
c:113 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
c:113 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:113 [binder, in Coq.Init.Datatypes]
C:113 [binder, in Coq.Logic.ClassicalFacts]
C:114 [binder, in Coq.ssr.ssrbool]
c:114 [binder, in Coq.Arith.PeanoNat]
c:116 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
C:116 [binder, in Coq.ssr.ssrbool]
c:116 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:117 [binder, in Coq.Init.Datatypes]
C:118 [binder, in Coq.ssr.ssrbool]
c:118 [binder, in Coq.Init.Datatypes]
c:119 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
c:119 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
c:119 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:12 [binder, in Coq.Reals.R_Ifp]
c:12 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:12 [binder, in Coq.ssr.ssrbool]
c:12 [binder, in Coq.Reals.PSeries_reg]
C:120 [binder, in Coq.ssr.ssrbool]
c:120 [binder, in Coq.MSets.MSetGenTree]
c:120 [binder, in Coq.Init.Datatypes]
c:121 [binder, in Coq.Numbers.NatInt.NZDiv]
c:122 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
C:122 [binder, in Coq.ssr.ssrbool]
c:122 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:122 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
c:122 [binder, in Coq.ZArith.Znumtheory]
c:124 [binder, in Coq.Numbers.NatInt.NZDiv]
c:125 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:125 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
c:125 [binder, in Coq.ZArith.Znumtheory]
C:126 [binder, in Coq.ssr.ssrbool]
c:126 [binder, in Coq.ZArith.Zdiv]
c:126 [binder, in Coq.ZArith.Zquot]
C:127 [binder, in Coq.Classes.CMorphisms]
c:127 [binder, in Coq.Numbers.NatInt.NZDiv]
C:127 [binder, in Coq.Init.Logic]
c:128 [binder, in Coq.setoid_ring.Ring_polynom]
c:128 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:128 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
c:128 [binder, in Coq.ZArith.Znumtheory]
c:129 [binder, in Coq.ZArith.Zdiv]
c:129 [binder, in Coq.ZArith.Zquot]
c:13 [binder, in Coq.ssr.ssrbool]
c:13 [binder, in Coq.Numbers.NatInt.NZLog]
c:13 [binder, in Coq.Reals.Rtopology]
C:130 [binder, in Coq.Vectors.VectorSpec]
c:131 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:131 [binder, in Coq.Reals.Rbasic_fun]
c:131 [binder, in Coq.Numbers.NatInt.NZDiv]
c:131 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
c:132 [binder, in Coq.ZArith.Zdiv]
c:132 [binder, in Coq.ZArith.Zquot]
c:133 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
c:134 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:134 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
c:135 [binder, in Coq.Init.Datatypes]
c:135 [binder, in Coq.Numbers.NatInt.NZDiv]
c:136 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
c:136 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c:137 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:137 [binder, in Coq.Logic.Hurkens]
c:137 [binder, in Coq.omega.OmegaLemmas]
c:137 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
c:138 [binder, in Coq.Numbers.NatInt.NZDiv]
c:139 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
c:14 [binder, in Coq.Numbers.NatInt.NZSqrt]
c:140 [binder, in Coq.setoid_ring.Ring_polynom]
c:140 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:140 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
c:141 [binder, in Coq.Numbers.NatInt.NZDiv]
c:143 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c:143 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
C:143 [binder, in Coq.Logic.ClassicalFacts]
c:144 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
c:144 [binder, in Coq.Reals.PSeries_reg]
c:144 [binder, in Coq.Numbers.NatInt.NZDiv]
c:145 [binder, in Coq.Reals.MVT]
c:146 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
C:147 [binder, in Coq.Logic.ClassicalFacts]
c:149 [binder, in Coq.MSets.MSetGenTree]
c:15 [binder, in Coq.Wellfounded.Inverse_Image]
c:15 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:15 [binder, in Coq.Reals.MVT]
C:15 [binder, in Coq.Logic.JMeq]
c:15 [binder, in Coq.ssr.ssrbool]
C:15 [binder, in Coq.Bool.DecBool]
c:151 [binder, in Coq.Init.Datatypes]
c:151 [binder, in Coq.Reals.PSeries_reg]
C:151 [binder, in Coq.setoid_ring.Ncring]
c:152 [binder, in Coq.Reals.MVT]
c:1523 [binder, in Coq.FSets.FMapAVL]
c:1527 [binder, in Coq.FSets.FMapAVL]
c:153 [binder, in Coq.Reals.MVT]
c:153 [binder, in Coq.micromega.Tauto]
c:154 [binder, in Coq.Reals.MVT]
C:154 [binder, in Coq.Logic.ClassicalFacts]
c:155 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c:155 [binder, in Coq.ZArith.Zdiv]
c:155 [binder, in Coq.micromega.Tauto]
c:158 [binder, in Coq.ZArith.Zdiv]
c:158 [binder, in Coq.Reals.PSeries_reg]
c:159 [binder, in Coq.Reals.Rtopology]
c:16 [binder, in Coq.Reals.Rtrigo_facts]
C:16 [binder, in Coq.Sets.Ensembles]
c:16 [binder, in Coq.Reals.MVT]
C:16 [binder, in Coq.Numbers.NaryFunctions]
c:16 [binder, in Coq.btauto.Algebra]
C:16 [binder, in Coq.Program.Combinators]
C:16 [binder, in Coq.Program.Basics]
C:160 [binder, in Coq.Vectors.VectorSpec]
c:161 [binder, in Coq.ZArith.Zdiv]
c:162 [binder, in Coq.micromega.RingMicromega]
c:162 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c:162 [binder, in Coq.Reals.Rtopology]
c:163 [binder, in Coq.setoid_ring.Ring_polynom]
c:163 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
c:164 [binder, in Coq.ZArith.Zdiv]
c:165 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c:165 [binder, in Coq.Reals.Rtopology]
c:166 [binder, in Coq.micromega.RingMicromega]
c:166 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
c:168 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c:17 [binder, in Coq.Reals.MVT]
c:17 [binder, in Coq.ssr.ssrbool]
c:17 [binder, in Coq.Reals.Rtopology]
c:171 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c:171 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
c:172 [binder, in Coq.setoid_ring.Ring_theory]
c:173 [binder, in Coq.Vectors.VectorSpec]
c:174 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c:174 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c:174 [binder, in Coq.Reals.RiemannInt_SF]
c:175 [binder, in Coq.setoid_ring.Ring_theory]
c:175 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
c:177 [binder, in Coq.Reals.MVT]
c:177 [binder, in Coq.ZArith.Znumtheory]
c:179 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
c:18 [binder, in Coq.Reals.MVT]
C:18 [binder, in Coq.Logic.ClassicalUniqueChoice]
c:18 [binder, in Coq.Reals.PSeries_reg]
C:180 [binder, in Coq.Classes.Morphisms]
c:180 [binder, in Coq.Reals.Rtopology]
c:181 [binder, in Coq.Reals.Rpower]
c:181 [binder, in Coq.Reals.Rtopology]
c:181 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c:182 [binder, in Coq.ZArith.Znumtheory]
c:184 [binder, in Coq.Reals.Rpower]
c:185 [binder, in Coq.ZArith.Znumtheory]
c:187 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:188 [binder, in Coq.ZArith.BinInt]
c:19 [binder, in Coq.micromega.Ztac]
c:19 [binder, in Coq.Reals.Rtrigo_facts]
c:19 [binder, in Coq.Reals.MVT]
c:19 [binder, in Coq.ZArith.Zpow_facts]
c:19 [binder, in Coq.ssr.ssrbool]
C:19 [binder, in Coq.Classes.CMorphisms]
C:19 [binder, in Coq.Program.Combinators]
c:190 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:191 [binder, in Coq.NArith.BinNat]
C:191 [binder, in Coq.Logic.ClassicalFacts]
c:193 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:193 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c:194 [binder, in Coq.QArith.QArith_base]
c:195 [binder, in Coq.Reals.MVT]
c:196 [binder, in Coq.Reals.MVT]
c:196 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:196 [binder, in Coq.MSets.MSetPositive]
c:197 [binder, in Coq.Reals.Rtopology]
C:197 [binder, in Coq.Logic.ClassicalFacts]
c:197 [binder, in Coq.QArith.QArith_base]
c:198 [binder, in Coq.Reals.Rtopology]
c:199 [binder, in Coq.ssr.ssrbool]
c:199 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:2 [binder, in Coq.ssr.ssreflect]
c:2 [binder, in Coq.Reals.Ratan]
C:20 [binder, in Coq.Classes.Morphisms]
c:20 [binder, in Coq.Reals.Rpower]
c:20 [binder, in Coq.Reals.Rtopology]
c:20 [binder, in Coq.Reals.Rgeom]
c:200 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c:202 [binder, in Coq.ssr.ssrbool]
c:202 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:202 [binder, in Coq.ZArith.Zdiv]
c:203 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c:204 [binder, in Coq.MSets.MSetPositive]
c:206 [binder, in Coq.ZArith.Zdiv]
c:206 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c:207 [binder, in Coq.Reals.Rfunctions]
c:207 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
C:207 [binder, in Coq.Vectors.VectorDef]
c:209 [binder, in Coq.ssr.ssrbool]
c:209 [binder, in Coq.MSets.MSetRBT]
c:209 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c:21 [binder, in Coq.Reals.MVT]
C:21 [binder, in Coq.Init.Logic]
C:210 [binder, in Coq.Classes.CMorphisms]
c:211 [binder, in Coq.Reals.Rfunctions]
c:211 [binder, in Coq.ZArith.Zdiv]
c:212 [binder, in Coq.ssr.ssrbool]
c:212 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c:214 [binder, in Coq.ZArith.Zdiv]
c:214 [binder, in Coq.MSets.MSetRBT]
C:218 [binder, in Coq.Logic.ClassicalFacts]
c:219 [binder, in Coq.micromega.ZMicromega]
c:22 [binder, in Coq.ZArith.Zpow_facts]
c:22 [binder, in Coq.Reals.Rpower]
C:22 [binder, in Coq.Program.Combinators]
c:220 [binder, in Coq.FSets.FSetPositive]
c:220 [binder, in Coq.Reals.Rtopology]
c:221 [binder, in Coq.setoid_ring.Ring_polynom]
c:222 [binder, in Coq.Reals.Rtopology]
c:224 [binder, in Coq.micromega.EnvRing]
c:224 [binder, in Coq.ZArith.Zdiv]
c:227 [binder, in Coq.setoid_ring.Ring_polynom]
c:228 [binder, in Coq.FSets.FSetPositive]
c:228 [binder, in Coq.Reals.Rtopology]
c:229 [binder, in Coq.ZArith.Zdiv]
C:23 [binder, in Coq.Sets.Constructive_sets]
c:23 [binder, in Coq.Numbers.NatInt.NZPow]
c:23 [binder, in Coq.Reals.MVT]
c:23 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
c:23 [binder, in Coq.ssr.ssrbool]
c:23 [binder, in Coq.setoid_ring.Ncring_polynom]
c:230 [binder, in Coq.setoid_ring.Ring_polynom]
c:230 [binder, in Coq.micromega.EnvRing]
c:230 [binder, in Coq.Reals.Rtopology]
c:231 [binder, in Coq.QArith.QArith_base]
c:232 [binder, in Coq.Reals.Rtopology]
c:233 [binder, in Coq.setoid_ring.Ring_polynom]
c:233 [binder, in Coq.micromega.EnvRing]
c:234 [binder, in Coq.Reals.Rtopology]
c:234 [binder, in Coq.QArith.QArith_base]
c:235 [binder, in Coq.Reals.Rtopology]
c:235 [binder, in Coq.micromega.ZMicromega]
c:235 [binder, in Coq.micromega.Tauto]
C:235 [binder, in Coq.Vectors.VectorDef]
c:236 [binder, in Coq.setoid_ring.Ring_polynom]
c:236 [binder, in Coq.micromega.EnvRing]
c:236 [binder, in Coq.Reals.Rtopology]
c:237 [binder, in Coq.MSets.MSetRBT]
c:237 [binder, in Coq.Reals.Rtopology]
c:237 [binder, in Coq.Vectors.VectorDef]
c:238 [binder, in Coq.Reals.Rtopology]
c:239 [binder, in Coq.micromega.EnvRing]
c:24 [binder, in Coq.Numbers.Natural.Abstract.NPow]
C:24 [binder, in Coq.Sets.Ensembles]
c:24 [binder, in Coq.Reals.MVT]
c:24 [binder, in Coq.btauto.Algebra]
c:24 [binder, in Coq.Reals.Rpower]
c:24 [binder, in Coq.Floats.FloatAxioms]
c:240 [binder, in Coq.Reals.Rtopology]
c:242 [binder, in Coq.Reals.Rtopology]
c:243 [binder, in Coq.Reals.Rtopology]
c:243 [binder, in Coq.micromega.ZMicromega]
C:243 [binder, in Coq.Vectors.VectorDef]
c:244 [binder, in Coq.Reals.Rtopology]
c:245 [binder, in Coq.Reals.Rtopology]
C:245 [binder, in Coq.Init.Logic]
c:246 [binder, in Coq.ssr.ssrbool]
c:246 [binder, in Coq.MSets.MSetRBT]
c:246 [binder, in Coq.Reals.Rtopology]
c:247 [binder, in Coq.micromega.ZMicromega]
c:249 [binder, in Coq.Reals.Rtopology]
c:25 [binder, in Coq.ssr.ssrbool]
c:25 [binder, in Coq.Reals.Rpower]
c:250 [binder, in Coq.micromega.ZMicromega]
c:251 [binder, in Coq.PArith.BinPos]
c:252 [binder, in Coq.Reals.Rtopology]
c:253 [binder, in Coq.Reals.Rtopology]
c:254 [binder, in Coq.Reals.Rtopology]
c:255 [binder, in Coq.MSets.MSetRBT]
c:256 [binder, in Coq.PArith.BinPos]
c:256 [binder, in Coq.micromega.ZMicromega]
c:257 [binder, in Coq.Reals.Rtopology]
c:258 [binder, in Coq.micromega.ZMicromega]
c:259 [binder, in Coq.PArith.BinPos]
c:26 [binder, in Coq.Numbers.NatInt.NZPow]
C:26 [binder, in Coq.Logic.FunctionalExtensionality]
c:26 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
c:26 [binder, in Coq.Reals.Rpower]
C:26 [binder, in Coq.Init.Logic]
c:260 [binder, in Coq.Reals.Rtopology]
c:260 [binder, in Coq.micromega.ZMicromega]
c:261 [binder, in Coq.Reals.Rtopology]
c:262 [binder, in Coq.Reals.Rtopology]
c:262 [binder, in Coq.micromega.ZMicromega]
c:265 [binder, in Coq.Reals.Rtopology]
c:268 [binder, in Coq.Reals.Rtopology]
c:269 [binder, in Coq.Reals.Rtopology]
c:27 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:27 [binder, in Coq.ssr.ssrbool]
c:27 [binder, in Coq.Reals.Rpower]
c:270 [binder, in Coq.Reals.Rtopology]
c:271 [binder, in Coq.Reals.Rtopology]
c:272 [binder, in Coq.Reals.Rtopology]
c:274 [binder, in Coq.setoid_ring.Ring_polynom]
c:274 [binder, in Coq.Reals.Ratan]
c:276 [binder, in Coq.Reals.Rtopology]
c:277 [binder, in Coq.Reals.Ratan]
c:278 [binder, in Coq.setoid_ring.Ncring_tac]
c:278 [binder, in Coq.Reals.Rtopology]
c:278 [binder, in Coq.Reals.Ratan]
c:279 [binder, in Coq.Reals.Rtopology]
c:28 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
c:28 [binder, in Coq.Structures.OrderedTypeAlt]
C:28 [binder, in Coq.Sets.Powerset_facts]
c:280 [binder, in Coq.Reals.Rtopology]
c:281 [binder, in Coq.setoid_ring.Ring_polynom]
c:287 [binder, in Coq.MSets.MSetGenTree]
C:29 [binder, in Coq.Sets.Constructive_sets]
c:29 [binder, in Coq.Numbers.NatInt.NZPow]
c:29 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
c:29 [binder, in Coq.ssr.ssrbool]
c:29 [binder, in Coq.Reals.Ratan]
C:29 [binder, in Coq.Init.Logic]
c:293 [binder, in Coq.MSets.MSetGenTree]
c:295 [binder, in Coq.PArith.BinPos]
C:295 [binder, in Coq.setoid_ring.Ring_theory]
c:297 [binder, in Coq.micromega.RingMicromega]
c:298 [binder, in Coq.PArith.BinPos]
C:298 [binder, in Coq.Logic.ChoiceFacts]
C:3 [binder, in Coq.Sets.Constructive_sets]
c:3 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c:3 [binder, in Coq.ssr.ssreflect]
c:3 [binder, in Coq.Strings.Ascii]
c:3 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
C:3 [binder, in Coq.Program.Basics]
c:3 [binder, in Coq.Reals.ClassicalConstructiveReals]
C:3 [binder, in Coq.Init.Tactics]
C:3 [binder, in Coq.Bool.DecBool]
c:309 [binder, in Coq.Reals.RiemannInt]
c:31 [binder, in Coq.Reals.MVT]
C:31 [binder, in Coq.Logic.ExtensionalityFacts]
c:31 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
c:31 [binder, in Coq.ssr.ssrbool]
C:31 [binder, in Coq.Sets.Powerset_facts]
c:310 [binder, in Coq.micromega.Tauto]
c:312 [binder, in Coq.Reals.RiemannInt]
C:315 [binder, in Coq.Logic.ChoiceFacts]
c:315 [binder, in Coq.micromega.Tauto]
c:317 [binder, in Coq.Reals.RiemannInt_SF]
c:319 [binder, in Coq.micromega.Tauto]
c:32 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:32 [binder, in Coq.Reals.MVT]
c:32 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
c:32 [binder, in Coq.Reals.Ratan]
C:32 [binder, in Coq.Init.Logic]
c:323 [binder, in Coq.Reals.RIneq]
c:325 [binder, in Coq.Reals.RiemannInt_SF]
c:33 [binder, in Coq.Reals.Abstract.ConstructiveReals]
c:33 [binder, in Coq.Reals.MVT]
C:33 [binder, in Coq.Logic.FunctionalExtensionality]
c:33 [binder, in Coq.setoid_ring.Integral_domain]
c:33 [binder, in Coq.ZArith.Znumtheory]
c:330 [binder, in Coq.Reals.Ratan]
c:331 [binder, in Coq.Reals.Ratan]
c:332 [binder, in Coq.Reals.Ratan]
c:332 [binder, in Coq.Reals.RiemannInt_SF]
c:333 [binder, in Coq.Reals.Ratan]
c:334 [binder, in Coq.Reals.Ratan]
c:335 [binder, in Coq.Reals.Ratan]
c:336 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c:336 [binder, in Coq.Reals.Ratan]
c:337 [binder, in Coq.Reals.Ratan]
c:339 [binder, in Coq.Reals.RiemannInt_SF]
c:34 [binder, in Coq.Reals.MVT]
C:34 [binder, in Coq.Sets.Powerset_facts]
C:340 [binder, in Coq.Logic.ChoiceFacts]
c:344 [binder, in Coq.Reals.RiemannInt_SF]
c:346 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c:346 [binder, in Coq.FSets.FMapFullAVL]
c:349 [binder, in Coq.MSets.MSetGenTree]
c:35 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:35 [binder, in Coq.Reals.MVT]
c:35 [binder, in Coq.setoid_ring.Field_theory]
C:35 [binder, in Coq.Init.Logic]
c:350 [binder, in Coq.FSets.FMapFullAVL]
c:351 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c:352 [binder, in Coq.Reals.RiemannInt_SF]
c:353 [binder, in Coq.MSets.MSetGenTree]
c:354 [binder, in Coq.MSets.MSetInterface]
c:357 [binder, in Coq.Reals.Ratan]
c:359 [binder, in Coq.Reals.RiemannInt_SF]
c:36 [binder, in Coq.Numbers.NatInt.NZPow]
c:36 [binder, in Coq.Reals.MVT]
c:360 [binder, in Coq.Reals.Ratan]
c:363 [binder, in Coq.QArith.QArith_base]
c:364 [binder, in Coq.Reals.RiemannInt_SF]
c:365 [binder, in Coq.QArith.QArith_base]
c:367 [binder, in Coq.micromega.ZMicromega]
c:368 [binder, in Coq.QArith.QArith_base]
c:37 [binder, in Coq.Reals.MVT]
C:37 [binder, in Coq.Logic.ExtensionalityFacts]
c:37 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
c:370 [binder, in Coq.QArith.QArith_base]
c:372 [binder, in Coq.Reals.RiemannInt_SF]
c:374 [binder, in Coq.QArith.QArith_base]
c:376 [binder, in Coq.QArith.QArith_base]
C:377 [binder, in Coq.FSets.FMapWeakList]
c:379 [binder, in Coq.Reals.RiemannInt_SF]
c:379 [binder, in Coq.QArith.QArith_base]
c:38 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:38 [binder, in Coq.Reals.MVT]
C:38 [binder, in Coq.Init.Logic]
c:381 [binder, in Coq.QArith.QArith_base]
c:388 [binder, in Coq.MSets.MSetRBT]
c:39 [binder, in Coq.Numbers.NatInt.NZPow]
c:39 [binder, in Coq.Reals.MVT]
C:4 [binder, in Coq.micromega.EnvRing]
c:4 [binder, in Coq.Reals.PSeries_reg]
C:40 [binder, in Coq.Sets.Ensembles]
C:40 [binder, in Coq.Logic.FunctionalExtensionality]
C:40 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]
c:400 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c:406 [binder, in Coq.setoid_ring.Ring_polynom]
c:408 [binder, in Coq.setoid_ring.Ring_polynom]
c:41 [binder, in Coq.Reals.Runcountable]
c:41 [binder, in Coq.Structures.OrdersAlt]
C:41 [binder, in Coq.Init.Logic]
c:411 [binder, in Coq.setoid_ring.Ring_polynom]
c:411 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c:415 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c:42 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:420 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
C:422 [binder, in Coq.Lists.List]
c:43 [binder, in Coq.ZArith.Znumtheory]
C:43 [binder, in Coq.rtauto.Rtauto]
c:434 [binder, in Coq.Logic.ChoiceFacts]
C:434 [binder, in Coq.Init.Logic]
c:436 [binder, in Coq.Logic.ChoiceFacts]
c:438 [binder, in Coq.Reals.Ranalysis1]
c:44 [binder, in Coq.Numbers.NatInt.NZPow]
c:44 [binder, in Coq.Reals.MVT]
c:444 [binder, in Coq.Reals.Ranalysis1]
c:445 [binder, in Coq.Reals.RiemannInt]
C:445 [binder, in Coq.FSets.FMapList]
c:446 [binder, in Coq.Reals.Ranalysis5]
C:45 [binder, in Coq.Sets.Ensembles]
c:45 [binder, in Coq.Reals.MVT]
c:45 [binder, in Coq.Reals.Ratan]
c:450 [binder, in Coq.Logic.ChoiceFacts]
c:452 [binder, in Coq.Reals.Ranalysis1]
c:452 [binder, in Coq.Logic.ChoiceFacts]
c:453 [binder, in Coq.Reals.RiemannInt]
c:453 [binder, in Coq.Reals.Ranalysis5]
c:454 [binder, in Coq.Reals.Ranalysis5]
c:455 [binder, in Coq.Reals.Ranalysis5]
c:456 [binder, in Coq.Reals.Ranalysis5]
c:457 [binder, in Coq.Reals.RiemannInt]
c:457 [binder, in Coq.Reals.Ranalysis5]
c:458 [binder, in Coq.setoid_ring.Ring_polynom]
c:458 [binder, in Coq.Reals.Ranalysis5]
c:459 [binder, in Coq.Reals.Ranalysis5]
c:46 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:46 [binder, in Coq.Reals.MVT]
c:46 [binder, in Coq.ZArith.Znumtheory]
c:460 [binder, in Coq.setoid_ring.Ring_polynom]
c:460 [binder, in Coq.Reals.Ranalysis5]
c:461 [binder, in Coq.Reals.RiemannInt]
c:461 [binder, in Coq.Reals.Ranalysis5]
c:462 [binder, in Coq.Reals.Ranalysis5]
c:463 [binder, in Coq.setoid_ring.Ring_polynom]
c:463 [binder, in Coq.Reals.Ranalysis5]
c:464 [binder, in Coq.Reals.Ranalysis5]
c:465 [binder, in Coq.Reals.RiemannInt]
c:465 [binder, in Coq.Reals.Ranalysis5]
c:466 [binder, in Coq.Reals.Ranalysis5]
c:467 [binder, in Coq.Reals.Ranalysis5]
c:468 [binder, in Coq.Reals.Ranalysis5]
c:47 [binder, in Coq.Numbers.NatInt.NZPow]
c:47 [binder, in Coq.Reals.MVT]
C:47 [binder, in Coq.Init.Logic]
c:48 [binder, in Coq.Reals.MVT]
c:48 [binder, in Coq.Reals.Ratan]
C:48 [binder, in Coq.Logic.ClassicalFacts]
C:48 [binder, in Coq.rtauto.Rtauto]
c:49 [binder, in Coq.Reals.Ranalysis1]
c:49 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:49 [binder, in Coq.Reals.MVT]
c:49 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
C:492 [binder, in Coq.ssr.ssrbool]
c:5 [binder, in Coq.Numbers.DecimalString]
C:5 [binder, in Coq.Sets.Ensembles]
c:5 [binder, in Coq.Reals.MVT]
c:5 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
c:5 [binder, in Coq.Numbers.HexadecimalString]
c:50 [binder, in Coq.Numbers.NatInt.NZPow]
c:50 [binder, in Coq.setoid_ring.Ring_polynom]
c:50 [binder, in Coq.Reals.MVT]
C:50 [binder, in Coq.Init.Logic]
C:50 [binder, in Coq.Logic.ClassicalFacts]
c:500 [binder, in Coq.Reals.RiemannInt]
C:506 [binder, in Coq.ssr.ssrbool]
c:51 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
c:51 [binder, in Coq.Reals.MVT]
C:514 [binder, in Coq.ssr.ssrbool]
c:52 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:52 [binder, in Coq.Reals.MVT]
c:52 [binder, in Coq.micromega.EnvRing]
c:52 [binder, in Coq.Reals.Ratan]
c:52 [binder, in Coq.micromega.RMicromega]
c:52 [binder, in Coq.NArith.Ndec]
C:524 [binder, in Coq.ssr.ssrbool]
c:53 [binder, in Coq.Reals.MVT]
c:53 [binder, in Coq.Reals.R_sqrt]
c:54 [binder, in Coq.Reals.Ranalysis2]
c:54 [binder, in Coq.Numbers.NatInt.NZPow]
C:54 [binder, in Coq.Sets.Ensembles]
c:54 [binder, in Coq.setoid_ring.Ring_polynom]
c:54 [binder, in Coq.Reals.MVT]
C:54 [binder, in Coq.Logic.ClassicalFacts]
c:55 [binder, in Coq.Reals.Runcountable]
c:55 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:55 [binder, in Coq.Reals.MVT]
c:55 [binder, in Coq.setoid_ring.Ncring_polynom]
C:55 [binder, in Coq.Init.Logic]
c:55 [binder, in Coq.NArith.Ndec]
C:56 [binder, in Coq.Sets.Ensembles]
c:56 [binder, in Coq.Reals.MVT]
c:56 [binder, in Coq.micromega.EnvRing]
c:57 [binder, in Coq.Reals.MVT]
c:57 [binder, in Coq.Reals.R_sqrt]
c:57 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
c:58 [binder, in Coq.Reals.Ranalysis2]
c:58 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:58 [binder, in Coq.Numbers.NatInt.NZPow]
C:58 [binder, in Coq.Init.Logic]
c:58 [binder, in Coq.NArith.Ndec]
c:6 [binder, in Coq.Structures.OrdersAlt]
c:6 [binder, in Coq.Numbers.Natural.Abstract.NBits]
c:6 [binder, in Coq.Numbers.Cyclic.Abstract.DoubleType]
c:6 [binder, in Coq.Structures.OrderedTypeAlt]
C:6 [binder, in Coq.Classes.CRelationClasses]
c:6 [binder, in Coq.Numbers.Integer.Abstract.ZBits]
c:60 [binder, in Coq.Reals.R_sqrt]
c:60 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
c:604 [binder, in Coq.Reals.RIneq]
c:607 [binder, in Coq.Reals.RIneq]
c:61 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:61 [binder, in Coq.Numbers.NatInt.NZPow]
C:61 [binder, in Coq.Init.Logic]
c:61 [binder, in Coq.NArith.Ndec]
c:62 [binder, in Coq.setoid_ring.Field_theory]
C:62 [binder, in Coq.ssr.ssreflect]
c:63 [binder, in Coq.Reals.Runcountable]
c:63 [binder, in Coq.Reals.MVT]
c:63 [binder, in Coq.Reals.R_sqrt]
c:63 [binder, in Coq.ZArith.Zquot]
c:64 [binder, in Coq.Numbers.NatInt.NZPow]
c:64 [binder, in Coq.Reals.MVT]
C:64 [binder, in Coq.Logic.ClassicalFacts]
c:64 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
c:65 [binder, in Coq.Reals.MVT]
c:65 [binder, in Coq.Numbers.NatInt.NZDiv]
C:65 [binder, in Coq.Logic.ClassicalFacts]
c:66 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:66 [binder, in Coq.Reals.R_sqrt]
c:66 [binder, in Coq.setoid_ring.Field_theory]
C:66 [binder, in Coq.Init.Logic]
c:67 [binder, in Coq.Numbers.NatInt.NZPow]
c:67 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
C:68 [binder, in Coq.Logic.ClassicalFacts]
c:68 [binder, in Coq.Reals.R_sqr]
c:68 [binder, in Coq.ZArith.Znumtheory]
c:69 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:69 [binder, in Coq.Reals.R_sqrt]
c:69 [binder, in Coq.Init.Specif]
c:7 [binder, in Coq.Reals.MVT]
c:7 [binder, in Coq.Reals.Machin]
C:7 [binder, in Coq.Init.Tactics]
c:70 [binder, in Coq.Numbers.NatInt.NZPow]
C:70 [binder, in Coq.Numbers.NaryFunctions]
c:70 [binder, in Coq.Reals.NewtonInt]
C:71 [binder, in Coq.Logic.ClassicalFacts]
c:72 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
c:72 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
c:72 [binder, in Coq.Reals.MVT]
c:73 [binder, in Coq.Numbers.NatInt.NZPow]
c:73 [binder, in Coq.Reals.R_sqrt]
c:73 [binder, in Coq.setoid_ring.Field_theory]
c:73 [binder, in Coq.omega.OmegaLemmas]
c:73 [binder, in Coq.setoid_ring.Ncring_polynom]
C:74 [binder, in Coq.Init.Datatypes]
c:75 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
C:75 [binder, in Coq.Logic.ClassicalFacts]
c:75 [binder, in Coq.Reals.RiemannInt_SF]
C:76 [binder, in Coq.Classes.Morphisms]
c:77 [binder, in Coq.setoid_ring.Ncring_polynom]
C:779 [binder, in Coq.Init.Specif]
c:78 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
c:78 [binder, in Coq.Numbers.NatInt.NZPow]
C:78 [binder, in Coq.Logic.ClassicalFacts]
c:78 [binder, in Coq.Reals.RiemannInt_SF]
c:8 [binder, in Coq.ZArith.Zpow_facts]
c:8 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
c:8 [binder, in Coq.Reals.Cauchy.PosExtra]
c:80 [binder, in Coq.setoid_ring.Field_theory]
C:80 [binder, in Coq.Init.Datatypes]
c:81 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
c:81 [binder, in Coq.Numbers.NatInt.NZPow]
c:81 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
c:81 [binder, in Coq.Reals.Ratan]
c:82 [binder, in Coq.Reals.Ratan]
c:83 [binder, in Coq.Reals.Ratan]
c:84 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
c:84 [binder, in Coq.Numbers.NatInt.NZPow]
c:84 [binder, in Coq.setoid_ring.Field_theory]
c:84 [binder, in Coq.Reals.Ratan]
c:85 [binder, in Coq.ZArith.Zquot]
c:85 [binder, in Coq.Reals.Ratan]
C:85 [binder, in Coq.Logic.ClassicalFacts]
c:86 [binder, in Coq.MSets.MSetGenTree]
C:86 [binder, in Coq.Init.Datatypes]
c:86 [binder, in Coq.Reals.Ratan]
c:86 [binder, in Coq.Numbers.NatInt.NZDiv]
c:87 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
c:87 [binder, in Coq.Numbers.NatInt.NZPow]
C:87 [binder, in Coq.Classes.CMorphisms]
c:87 [binder, in Coq.Reals.Ratan]
C:88 [binder, in Coq.micromega.RingMicromega]
c:88 [binder, in Coq.ZArith.Zquot]
c:88 [binder, in Coq.Reals.Ratan]
C:88 [binder, in Coq.Logic.ClassicalFacts]
c:89 [binder, in Coq.Reals.NewtonInt]
C:89 [binder, in Coq.Init.Datatypes]
c:89 [binder, in Coq.Numbers.NatInt.NZDiv]
c:9 [binder, in Coq.Numbers.Natural.Abstract.NPow]
c:9 [binder, in Coq.Reals.MVT]
C:9 [binder, in Coq.Program.Combinators]
C:9 [binder, in Coq.Bool.DecBool]
c:90 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
c:90 [binder, in Coq.setoid_ring.Field_theory]
c:90 [binder, in Coq.MSets.MSetGenTree]
c:91 [binder, in Coq.ZArith.Zquot]
c:92 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
c:92 [binder, in Coq.Init.Specif]
c:92 [binder, in Coq.Numbers.NatInt.NZDiv]
c:92 [binder, in Coq.NArith.Ndec]
c:93 [binder, in Coq.setoid_ring.Ring_polynom]
c:94 [binder, in Coq.setoid_ring.Field_theory]
c:94 [binder, in Coq.MSets.MSetGenTree]
c:94 [binder, in Coq.ZArith.Zquot]
C:946 [binder, in Coq.Init.Logic]
c:95 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
c:95 [binder, in Coq.micromega.EnvRing]
c:95 [binder, in Coq.Reals.NewtonInt]
c:95 [binder, in Coq.Numbers.NatInt.NZDiv]
c:95 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
c:95 [binder, in Coq.NArith.Ndec]
c:96 [binder, in Coq.ZArith.Zdiv]
c:97 [binder, in Coq.setoid_ring.Ring_polynom]
c:97 [binder, in Coq.ZArith.Zquot]
c:97 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
c:98 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
c:98 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
c:98 [binder, in Coq.Numbers.NatInt.NZDiv]
c:98 [binder, in Coq.NArith.Ndec]
c:99 [binder, in Coq.micromega.EnvRing]
c:99 [binder, in Coq.ZArith.Zdiv]
c:99 [binder, in Coq.Reals.NewtonInt]
c:99 [binder, in Coq.setoid_ring.Ncring_polynom]
| 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 | (72487 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1049 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (47021 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 | (788 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1537 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (588 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11841 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1025 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (634 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (306 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (473 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (486 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (881 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1465 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4229 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (164 entries) |