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 | (21446 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 | (889 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 | (714 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 | (1464 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 | (482 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 | (10031 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 | (663 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 | (537 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 | (374 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 | (285 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 | (457 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 | (616 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 | (1328 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 | (3469 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 | (137 entries) |

## C

C [definition, in Coq.Reals.Binomial]cancel [definition, in Coq.ssr.ssrfun]

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_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]

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]

cardinal [inductive, in Coq.Sets.Finite_sets]

cardinalO_empty [lemma, in Coq.Sets.Finite_sets_facts]

cardinal_decreases [lemma, in Coq.Sets.Image]

cardinal_Im_intro [lemma, in Coq.Sets.Image]

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]

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 [inductive, in Coq.Numbers.Cyclic.Abstract.DoubleType]

Carry [section, in Coq.Numbers.Cyclic.Abstract.DoubleType]

Carry.A [variable, in Coq.Numbers.Cyclic.Abstract.DoubleType]

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]

cast [definition, in Coq.Vectors.Fin]

cast [definition, in Coq.Vectors.VectorEq]

CAST [section, in Coq.Vectors.VectorEq]

catcomp [definition, in Coq.ssr.ssrfun]

cauchy_finite [lemma, in Coq.Reals.Cauchy_prod]

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_bound [lemma, in Coq.Reals.Rseries]

Cauchy_crit [definition, in Coq.Reals.Rseries]

Cauchy_prod [library]

ceiling [definition, in Coq.micromega.ZMicromega]

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_spec [lemma, in Coq.setoid_ring.Ring_polynom]

CEquivalence [library]

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]

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

checker_nf_sound [lemma, in Coq.micromega.RingMicromega]

check_normalised_formulas [definition, in Coq.micromega.RingMicromega]

check_inconsistent_sound [lemma, in Coq.micromega.RingMicromega]

check_inconsistent [definition, in Coq.micromega.RingMicromega]

check_correct [lemma, in Coq.nsatz.Nsatz]

check_proof [definition, in Coq.rtauto.Rtauto]

Choice [lemma, in Coq.Init.Specif]

choice [lemma, in Coq.Logic.ClassicalChoice]

choice [lemma, in Coq.Logic.ClassicalEpsilon]

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]

cI [definition, in Coq.setoid_ring.Ncring_polynom]

CInv [constructor, in Coq.micromega.RMicromega]

Cj [constructor, in Coq.micromega.Tauto]

classic [axiom, in Coq.Logic.Classical_Prop]

Classical [library]

ClassicalChoice [library]

ClassicalDescription [library]

ClassicalEpsilon [library]

ClassicalFacts [library]

classically [definition, in Coq.ssr.ssrbool]

ClassicalUniqueChoice [library]

classical_denumerable_description_imp_fun_choice [lemma, in Coq.Logic.ChoiceFacts]

classical_proof_irrelevence [lemma, in Coq.Logic.Berardi]

classical_indefinite_description [lemma, in Coq.Logic.ClassicalEpsilon]

classical_definite_description [lemma, in Coq.Logic.ClassicalDescription]

Classical_Prop [library]

Classical_Pred_Type [library]

Classical_sets [library]

classicP [lemma, in Coq.ssr.ssrbool]

classicW [lemma, in Coq.ssr.ssrbool]

classic_set [abbreviation, in Coq.Logic.ClassicalUniqueChoice]

classic_set_in_prop_context [lemma, in Coq.Logic.ClassicalUniqueChoice]

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]

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]

CMinus [constructor, in Coq.micromega.RMicromega]

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]

cmt [constructor, in Coq.funind.Recdef]

CMult [constructor, in Coq.micromega.RMicromega]

cneqb [definition, in Coq.micromega.RingMicromega]

cneqb_sound [lemma, in Coq.micromega.RingMicromega]

cnf [definition, in Coq.micromega.Tauto]

cnf_checker_sound [lemma, in Coq.micromega.Tauto]

cnf_checker [definition, in Coq.micromega.Tauto]

cnf_negate_correct [lemma, in Coq.micromega.RingMicromega]

cnf_negate [definition, in Coq.micromega.RingMicromega]

cnf_normalise_correct [lemma, in Coq.micromega.RingMicromega]

cnf_normalise [definition, in Coq.micromega.RingMicromega]

cO [definition, in Coq.setoid_ring.Ncring_polynom]

coherent [definition, in Coq.Sets.Relations_3]

coherent_symmetric [lemma, in Coq.Sets.Relations_3_facts]

COHERENT_VALUE [section, in Coq.ZArith.Zdigits]

collective_pred [definition, in Coq.ssr.ssrbool]

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_nth [lemma, in Coq.Lists.List]

combine_length [lemma, in Coq.Lists.List]

combine_split [lemma, 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 [abbreviation, in Coq.ssr.ssrfun]

comp [abbreviation, 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 [definition, in Coq.Init.Nat]

Compare [inductive, in Coq.Structures.OrderedType]

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]

CompareSpec [inductive, in Coq.Init.Datatypes]

CompareSpecT [inductive, in Coq.Init.Datatypes]

CompareSpec2Type [lemma, in Coq.Init.Datatypes]

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_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.Sets.Relations_1_facts]

complement [definition, in Coq.Classes.CRelationClasses]

complement [definition, in Coq.Classes.RelationClasses]

Complement [definition, in Coq.Sets.Ensembles]

complementary [definition, in Coq.Reals.Rtopology]

complementary_P1 [lemma, in Coq.Reals.Rtopology]

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_Complement [lemma, in Coq.Sets.Classical_sets]

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

complement_Symmetric [definition, in Coq.Classes.RelationClasses]

complement_Irreflexive [definition, in Coq.Classes.RelationClasses]

complement_inverse [lemma, in Coq.Classes.RelationClasses]

Complete [section, in Coq.setoid_ring.Field_theory]

Complete [inductive, in Coq.Sets.Cpo]

completeness [axiom, 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_assoc [lemma, in Coq.Program.Combinators]

compose_id_right [lemma, in Coq.Program.Combinators]

compose_id_left [lemma, in Coq.Program.Combinators]

compose_proper [instance, in Coq.Classes.CMorphisms]

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

compute_list [definition, in Coq.nsatz.Nsatz]

concat [definition, 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]

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_positivity [definition, in Coq.Reals.Rsqrt_def]

cond_pos_sum [lemma, in Coq.Reals.PartSum]

cond_D2 [projection, in Coq.Reals.Ranalysis1]

cond_D1 [projection, in Coq.Reals.Ranalysis1]

cond_diff [projection, in Coq.Reals.Ranalysis1]

cond_fam [projection, in Coq.Reals.Rtopology]

cond_eq [lemma, in Coq.Reals.SeqProp]

Cond0 [definition, in Coq.nsatz.Nsatz]

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 [constructor, in Coq.Reals.RList]

cons [constructor, in Coq.Init.Datatypes]

cons [constructor, in Coq.Vectors.VectorDef]

cons [abbreviation, in Coq.Lists.List]

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]

ConstructiveDefiniteDescription [abbreviation, in Coq.Logic.ChoiceFacts]

ConstructiveDefiniteDescription_on [definition, in Coq.Logic.ChoiceFacts]

ConstructiveEpsilon [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]

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 [axiom, in Coq.Logic.Description]

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

constructive_indefinite_description [axiom, in Coq.Logic.IndefiniteDescription]

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_sets [library]

const_nth [lemma, in Coq.Vectors.VectorSpec]

cons_inj [definition, in Coq.Vectors.VectorSpec]

cons_ORlist [definition, in Coq.Reals.RList]

cons_Rlist [definition, in Coq.Reals.RList]

cons_sort [abbreviation, in Coq.Sorting.Sorted]

cons_leA [abbreviation, in Coq.Sorting.Sorted]

contains [definition, in Coq.Sets.Relations_1]

contains_is_preorder [lemma, in Coq.Sets.Relations_1_facts]

contents [definition, in Coq.Sorting.Heap]

contents [projection, in Coq.rtauto.Bintree]

continue_in [definition, in Coq.Reals.Rderiv]

continuity [definition, in Coq.Reals.Ranalysis1]

continuity_seq [lemma, in Coq.Reals.Rsqrt_def]

continuity_implies_RiemannInt [lemma, in Coq.Reals.RiemannInt]

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_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_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_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]

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]

contraNT [definition, in Coq.ssr.ssrbool]

contrapositive [lemma, in Coq.Logic.Decidable]

contraR [lemma, in Coq.ssr.ssrbool]

contraT [lemma, in Coq.ssr.ssrbool]

contraTF [lemma, in Coq.ssr.ssrbool]

contraTN [definition, in Coq.ssr.ssrbool]

contraTT [definition, in Coq.ssr.ssrbool]

cont_deriv [lemma, in Coq.Reals.Rderiv]

cont1 [projection, in Coq.Reals.RiemannInt]

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]

Coq85 [library]

Coq86 [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_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_PI4 [lemma, in Coq.Reals.Rtrigo_calc]

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_approx [definition, in Coq.Reals.Rtrigo_alt]

cos_term [definition, in Coq.Reals.Rtrigo_alt]

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_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_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]

cos3PI4 [lemma, in Coq.Reals.Rtrigo_calc]

count_occ_map [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]

CPlus [constructor, in Coq.micromega.RMicromega]

Cpo [record, in Coq.Sets.Cpo]

Cpo [library]

Cpo_cond [projection, in Coq.Sets.Cpo]

CQ [constructor, in Coq.micromega.RMicromega]

crelation [definition, in Coq.Classes.CRelationClasses]

CRelationClasses [library]

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]

cross_product_eq [lemma, in Coq.setoid_ring.Field_theory]

Cst [constructor, in Coq.btauto.Algebra]

cstlist [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]

ctx [definition, in Coq.rtauto.Rtauto]

Cut [constructor, in Coq.rtauto.Rtauto]

CutProof [constructor, in Coq.micromega.ZMicromega]

Cutting [section, 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_pow_half [lemma, in Coq.Reals.Rsqrt_def]

cv_dicho [lemma, in Coq.Reals.Rsqrt_def]

cv_cauchy_2 [lemma, in Coq.Reals.PartSum]

cv_cauchy_1 [lemma, in Coq.Reals.PartSum]

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_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_shift' [lemma, in Coq.Reals.Rseries]

CV_shift [lemma, in Coq.Reals.Rseries]

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]

CZ [constructor, in Coq.micromega.RMicromega]

C_maj [lemma, in Coq.Reals.Rprod]

c_sqrt [constructor, in Coq.ZArith.Zsqrt_compat]

C0 [constructor, in Coq.micromega.RMicromega]

C0 [constructor, in Coq.Numbers.Cyclic.Abstract.DoubleType]

C1 [constructor, in Coq.micromega.RMicromega]

c1 [projection, in Coq.Reals.RiemannInt]

C1 [constructor, in Coq.Numbers.Cyclic.Abstract.DoubleType]

C1 [definition, in Coq.Reals.Cos_rel]

C1_fun [record, in Coq.Reals.RiemannInt]

C1_cvg [lemma, in Coq.Reals.Cos_rel]

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 | (21446 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 | (889 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 | (714 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 | (1464 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 | (482 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 | (10031 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 | (663 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 | (537 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 | (374 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 | (285 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 | (457 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 | (616 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 | (1328 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 | (3469 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 | (137 entries) |