| 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 | (26016 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 | (1003 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 | (811 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 | (1771 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) |
| 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 | (961 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 | (11981 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 | (508 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (308 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (479 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 | (496 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 | (905 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 | (1199 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 | (4840 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (166 entries) |
C (lemma)
cancel_to_of [in Stdlib.Arith.Cantor]cancel_of_to [in Stdlib.Arith.Cantor]
canLR [in Stdlib.ssr.ssrfun]
canLR_on [in Stdlib.ssr.ssrbool]
canLR_in [in Stdlib.ssr.ssrbool]
canonical_Rsqr [in Stdlib.Reals.R_sqr]
canRL [in Stdlib.ssr.ssrfun]
canRL_on [in Stdlib.ssr.ssrbool]
canRL_in [in Stdlib.ssr.ssrbool]
can_mono_in [in Stdlib.ssr.ssrbool]
can_mono [in Stdlib.ssr.ssrbool]
can_in_comp [in Stdlib.ssr.ssrbool]
can_in_pcan [in Stdlib.ssr.ssrbool]
can_in_inj [in Stdlib.ssr.ssrbool]
can_comp [in Stdlib.ssr.ssrfun]
can_inj [in Stdlib.ssr.ssrfun]
can_pcan [in Stdlib.ssr.ssrfun]
can_inj [in Stdlib.Numbers.Cyclic.Int63.Uint63]
cardinalO_empty [in Stdlib.Sets.Finite_sets_facts]
cardinal_elim [in Stdlib.Sets.Finite_sets]
cardinal_invert [in Stdlib.Sets.Finite_sets]
cardinal_unicity [in Stdlib.Sets.Finite_sets_facts]
cardinal_is_functional [in Stdlib.Sets.Finite_sets_facts]
cardinal_Empty [in Stdlib.Sets.Finite_sets_facts]
cardinal_finite [in Stdlib.Sets.Finite_sets_facts]
cardinal_decreases [in Stdlib.Sets.Image]
cardinal_Im_intro [in Stdlib.Sets.Image]
card_Add_gen [in Stdlib.Sets.Finite_sets_facts]
card_soustr_1 [in Stdlib.Sets.Finite_sets_facts]
case_L_R [in Stdlib.Vectors.Fin]
case_L_R' [in Stdlib.Vectors.Fin]
cast_diff [in Stdlib.Numbers.Cyclic.Int63.Uint63]
cast_refl [in Stdlib.Numbers.Cyclic.Int63.Uint63]
cat_assoc [in Stdlib.Strings.PString]
cat_empty_r [in Stdlib.Strings.PString]
cat_empty_l [in Stdlib.Strings.PString]
cat_get_spec_r [in Stdlib.Strings.PString]
cat_get_spec_l [in Stdlib.Strings.PString]
cat_length_spec_no_overflow [in Stdlib.Strings.PString]
cat_length_spec [in Stdlib.Strings.PString]
cat_spec_valid_length [in Stdlib.Strings.PString]
CauchyMorph_rat [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
cauchy_bound [in Stdlib.Reals.Rseries]
cauchy_finite [in Stdlib.Reals.Cauchy_prod]
cauchy_abs [in Stdlib.Reals.PartSum]
cauchy_min [in Stdlib.Reals.SeqProp]
cauchy_opp [in Stdlib.Reals.SeqProp]
cauchy_maj [in Stdlib.Reals.SeqProp]
ceqb_spec [in Stdlib.micromega.EnvRing]
ceqb_spec' [in Stdlib.setoid_ring.Field_theory]
ceqb_spec [in Stdlib.setoid_ring.Field_theory]
ceqb_spec [in Stdlib.setoid_ring.Ring_polynom]
Cesaro [in Stdlib.Reals.SeqSeries]
Cesaro_1 [in Stdlib.Reals.SeqSeries]
char63_compare_trans [in Stdlib.Strings.PString]
char63_compare_antisym [in Stdlib.Strings.PString]
char63_compare_refl [in Stdlib.Strings.PString]
checker_nf_sound [in Stdlib.micromega.RingMicromega]
check_inconsistent_sound [in Stdlib.micromega.RingMicromega]
check_correct [in Stdlib.nsatz.NsatzTactic]
choice [in Stdlib.Logic.ClassicalEpsilon]
Choice [in Stdlib.Init.Specif]
choice [in Stdlib.Logic.ClassicalChoice]
Choice2 [in Stdlib.Init.Specif]
classical_definite_description [in Stdlib.Logic.ClassicalDescription]
classical_proof_irrelevance [in Stdlib.Logic.Berardi]
classical_denumerable_description_imp_fun_choice [in Stdlib.Logic.ChoiceFacts]
classical_indefinite_description [in Stdlib.Logic.ClassicalEpsilon]
classicP [in Stdlib.ssr.ssrbool]
classicW [in Stdlib.ssr.ssrbool]
classic_ex [in Stdlib.ssr.ssrbool]
classic_sigW [in Stdlib.ssr.ssrbool]
classic_imply [in Stdlib.ssr.ssrbool]
classic_pick [in Stdlib.ssr.ssrbool]
classic_EM [in Stdlib.ssr.ssrbool]
classic_bind [in Stdlib.ssr.ssrbool]
classic_set_in_prop_context [in Stdlib.Logic.ClassicalUniqueChoice]
cleb_sound [in Stdlib.micromega.RingMicromega]
closed_set_P1 [in Stdlib.Reals.Rtopology]
clos_trans_list_ext_app_r [in Stdlib.Wellfounded.List_Extension]
clos_trans_list_ext_app_l [in Stdlib.Wellfounded.List_Extension]
clos_refl_trans_list_ext_app_l [in Stdlib.Wellfounded.List_Extension]
clos_refl_trans_list_ext_app_r [in Stdlib.Wellfounded.List_Extension]
clos_trans_list_ext_nil_l [in Stdlib.Wellfounded.List_Extension]
clos_trans_transp_permute [in Stdlib.Relations.Operators_Properties]
clos_rst_rstn1_iff [in Stdlib.Relations.Operators_Properties]
clos_rst_rstn1 [in Stdlib.Relations.Operators_Properties]
clos_rstn1_sym [in Stdlib.Relations.Operators_Properties]
clos_rstn1_trans [in Stdlib.Relations.Operators_Properties]
clos_rstn1_rst [in Stdlib.Relations.Operators_Properties]
clos_rst_rst1n_iff [in Stdlib.Relations.Operators_Properties]
clos_rst_rst1n [in Stdlib.Relations.Operators_Properties]
clos_rst1n_sym [in Stdlib.Relations.Operators_Properties]
clos_rst1n_trans [in Stdlib.Relations.Operators_Properties]
clos_rst1n_rst [in Stdlib.Relations.Operators_Properties]
clos_refl_trans_ind_right [in Stdlib.Relations.Operators_Properties]
clos_refl_trans_ind_left [in Stdlib.Relations.Operators_Properties]
clos_rt_rtn1_iff [in Stdlib.Relations.Operators_Properties]
clos_rt_rtn1 [in Stdlib.Relations.Operators_Properties]
clos_rtn1_rt [in Stdlib.Relations.Operators_Properties]
clos_rt_rt1n_iff [in Stdlib.Relations.Operators_Properties]
clos_rt_rt1n [in Stdlib.Relations.Operators_Properties]
clos_rt1n_rt [in Stdlib.Relations.Operators_Properties]
clos_rtn1_step [in Stdlib.Relations.Operators_Properties]
clos_rt1n_step [in Stdlib.Relations.Operators_Properties]
clos_trans_tn1_iff [in Stdlib.Relations.Operators_Properties]
clos_trans_tn1 [in Stdlib.Relations.Operators_Properties]
clos_tn1_trans [in Stdlib.Relations.Operators_Properties]
clos_trans_t1n_iff [in Stdlib.Relations.Operators_Properties]
clos_trans_t1n [in Stdlib.Relations.Operators_Properties]
clos_t1n_trans [in Stdlib.Relations.Operators_Properties]
clos_rst_idempotent [in Stdlib.Relations.Operators_Properties]
clos_rst_is_equiv [in Stdlib.Relations.Operators_Properties]
clos_rt_t [in Stdlib.Relations.Operators_Properties]
clos_t_clos_rt [in Stdlib.Relations.Operators_Properties]
clos_r_clos_rt [in Stdlib.Relations.Operators_Properties]
clos_rt_clos_rst [in Stdlib.Relations.Operators_Properties]
clos_rt_idempotent [in Stdlib.Relations.Operators_Properties]
clos_rt_is_preorder [in Stdlib.Relations.Operators_Properties]
cltb_sound [in Stdlib.micromega.RingMicromega]
clt_morph [in Stdlib.micromega.ZCoeff]
clt_pos_morph [in Stdlib.micromega.ZCoeff]
cmod_small [in Stdlib.Numbers.Cyclic.Int63.Sint63]
cmod_mod [in Stdlib.Numbers.Cyclic.Int63.Sint63]
cneqb_sound [in Stdlib.micromega.RingMicromega]
cnf_of_list_correct [in Stdlib.micromega.ZMicromega]
cnf_negate_correct [in Stdlib.micromega.RingMicromega]
cnf_normalise_correct [in Stdlib.micromega.RingMicromega]
cnf_of_list_correct [in Stdlib.micromega.RingMicromega]
cnf_checker_sound [in Stdlib.micromega.Tauto]
coherent_symmetric [in Stdlib.Sets.Relations_3_facts]
combine_firstn [in Stdlib.Lists.List]
combine_firstn_r [in Stdlib.Lists.List]
combine_firstn_l [in Stdlib.Lists.List]
combine_nil [in Stdlib.Lists.List]
combine_nth [in Stdlib.Lists.List]
combine_split [in Stdlib.Lists.List]
comm [in Stdlib.setoid_ring.Ncring_tac]
comm_left [in Stdlib.Sets.Permut]
comm_right [in Stdlib.Sets.Permut]
compA [in Stdlib.ssr.ssrfun]
compact_P6 [in Stdlib.Reals.Rtopology]
compact_carac [in Stdlib.Reals.Rtopology]
compact_P5 [in Stdlib.Reals.Rtopology]
compact_P4 [in Stdlib.Reals.Rtopology]
compact_P3 [in Stdlib.Reals.Rtopology]
compact_eqDom [in Stdlib.Reals.Rtopology]
compact_EMP [in Stdlib.Reals.Rtopology]
compact_P2 [in Stdlib.Reals.Rtopology]
compact_P1 [in Stdlib.Reals.Rtopology]
CompareBasedOrderFacts.compare_nge_iff [in Stdlib.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_nle_iff [in Stdlib.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_nlt_iff [in Stdlib.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_ngt_iff [in Stdlib.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_ge_iff [in Stdlib.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_gt_iff [in Stdlib.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_refl [in Stdlib.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_eq [in Stdlib.Structures.OrdersFacts]
CompareBasedOrderFacts.compare_spec [in Stdlib.Structures.OrdersFacts]
CompareBasedOrderFacts.lt_eq_cases [in Stdlib.Structures.OrdersFacts]
CompareBasedOrderFacts.lt_irrefl [in Stdlib.Structures.OrdersFacts]
CompareFacts.compare_antisym [in Stdlib.Structures.OrdersFacts]
CompareFacts.compare_refl [in Stdlib.Structures.OrdersFacts]
CompareFacts.compare_ngt_iff [in Stdlib.Structures.OrdersFacts]
CompareFacts.compare_nlt_iff [in Stdlib.Structures.OrdersFacts]
CompareFacts.compare_gt_iff [in Stdlib.Structures.OrdersFacts]
CompareFacts.compare_lt_iff [in Stdlib.Structures.OrdersFacts]
CompareFacts.compare_eq [in Stdlib.Structures.OrdersFacts]
CompareFacts.compare_eq_iff [in Stdlib.Structures.OrdersFacts]
CompareSpec2Type [in Stdlib.Init.Datatypes]
compare_eq_iff [in Stdlib.Strings.Ascii]
compare_antisym [in Stdlib.Strings.Ascii]
compare_lt_spec [in Stdlib.Strings.PString]
compare_eq [in Stdlib.Strings.PString]
compare_spec [in Stdlib.Strings.PString]
compare_eq_correct [in Stdlib.Strings.PString]
compare_trans [in Stdlib.Strings.PString]
compare_antisym [in Stdlib.Strings.PString]
compare_refl [in Stdlib.Strings.PString]
compare_spec [in Stdlib.Bool.Bool]
compare_eq_iff [in Stdlib.Strings.String]
compare_antisym [in Stdlib.Strings.String]
compare_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
Compare2EqBool.eqb_eq [in Stdlib.Structures.Orders]
comparison_eq_stable [in Stdlib.Init.Datatypes]
complementary_P1 [in Stdlib.Reals.Rtopology]
complement_Symmetric [in Stdlib.Classes.RelationClasses]
complement_Irreflexive [in Stdlib.Classes.RelationClasses]
complement_inverse [in Stdlib.Classes.RelationClasses]
Complement_Complement [in Stdlib.Sets.Classical_sets]
complement_Symmetric [in Stdlib.Classes.CRelationClasses]
complement_Irreflexive [in Stdlib.Classes.CRelationClasses]
complement_inverse [in Stdlib.Classes.CRelationClasses]
completeness [in Stdlib.Reals.Raxioms]
CompOpp_iff [in Stdlib.Init.Datatypes]
CompOpp_inj [in Stdlib.Init.Datatypes]
CompOpp_involutive [in Stdlib.Init.Datatypes]
compose_assoc [in Stdlib.Program.Combinators]
compose_id_right [in Stdlib.Program.Combinators]
compose_id_left [in Stdlib.Program.Combinators]
compose0 [in Stdlib.rtauto.Rtauto]
compose1 [in Stdlib.rtauto.Rtauto]
compose2 [in Stdlib.rtauto.Rtauto]
compose3 [in Stdlib.rtauto.Rtauto]
CompSpec2Type [in Stdlib.Init.Datatypes]
compute_list_correct [in Stdlib.nsatz.NsatzTactic]
concat_nil_Forall [in Stdlib.Lists.List]
concat_filter_map [in Stdlib.Lists.List]
concat_map [in Stdlib.Lists.List]
concat_app [in Stdlib.Lists.List]
concat_cons [in Stdlib.Lists.List]
concat_nil [in Stdlib.Lists.List]
cond_pos_sum [in Stdlib.Reals.Abstract.ConstructiveSum]
cond_pos_sum [in Stdlib.Reals.PartSum]
cond_eq [in Stdlib.Reals.SeqProp]
cong_transitive_same_relation [in Stdlib.Sets.Relations_1_facts]
cong_antisymmetric_same_relation [in Stdlib.Sets.Relations_1_facts]
cong_symmetric_same_relation [in Stdlib.Sets.Relations_1_facts]
cong_reflexive_same_relation [in Stdlib.Sets.Relations_1_facts]
cong_congr [in Stdlib.Sets.Permut]
constructive_indefinite_ground_description_Z [in Stdlib.Reals.Cauchy.ConstructiveExtra]
constructive_definite_ground_description [in Stdlib.Logic.ConstructiveEpsilon]
constructive_indefinite_ground_description [in Stdlib.Logic.ConstructiveEpsilon]
constructive_indefinite_ground_description_nat_Acc [in Stdlib.Logic.ConstructiveEpsilon]
constructive_definite_description [in Stdlib.Logic.IndefiniteDescription]
constructive_definite_descr_excluded_middle [in Stdlib.Logic.ChoiceFacts]
constructive_definite_descr_fun_reification [in Stdlib.Logic.ChoiceFacts]
constructive_indefinite_descr_fun_choice [in Stdlib.Logic.ChoiceFacts]
constructive_indefinite_description_and_small_drinker_iff_epsilon [in Stdlib.Logic.ChoiceFacts]
constructive_indefinite_description_and_small_drinker_imp_epsilon [in Stdlib.Logic.ChoiceFacts]
constructive_definite_description [in Stdlib.Logic.Epsilon]
constructive_indefinite_description [in Stdlib.Logic.Epsilon]
constructive_definite_description [in Stdlib.Logic.ClassicalEpsilon]
const_nth [in Stdlib.Vectors.VectorSpec]
cons_seq [in Stdlib.Lists.List]
contains_is_preorder [in Stdlib.Sets.Relations_1_facts]
continuity_comp [in Stdlib.Reals.Ranalysis1]
continuity_div [in Stdlib.Reals.Ranalysis1]
continuity_inv [in Stdlib.Reals.Ranalysis1]
continuity_scal [in Stdlib.Reals.Ranalysis1]
continuity_const [in Stdlib.Reals.Ranalysis1]
continuity_mult [in Stdlib.Reals.Ranalysis1]
continuity_minus [in Stdlib.Reals.Ranalysis1]
continuity_opp [in Stdlib.Reals.Ranalysis1]
continuity_plus [in Stdlib.Reals.Ranalysis1]
continuity_pt_comp [in Stdlib.Reals.Ranalysis1]
continuity_pt_div [in Stdlib.Reals.Ranalysis1]
continuity_pt_inv [in Stdlib.Reals.Ranalysis1]
continuity_pt_scal [in Stdlib.Reals.Ranalysis1]
continuity_pt_const [in Stdlib.Reals.Ranalysis1]
continuity_pt_mult [in Stdlib.Reals.Ranalysis1]
continuity_pt_minus [in Stdlib.Reals.Ranalysis1]
continuity_pt_opp [in Stdlib.Reals.Ranalysis1]
continuity_pt_plus [in Stdlib.Reals.Ranalysis1]
continuity_pt_locally_ext [in Stdlib.Reals.Ranalysis1]
continuity_ab_min [in Stdlib.Reals.Rtopology]
continuity_ab_maj [in Stdlib.Reals.Rtopology]
continuity_compact [in Stdlib.Reals.Rtopology]
continuity_P3 [in Stdlib.Reals.Rtopology]
continuity_P2 [in Stdlib.Reals.Rtopology]
continuity_P1 [in Stdlib.Reals.Rtopology]
continuity_pt_recip_interv [in Stdlib.Reals.Ranalysis5]
continuity_pt_recip_prelim [in Stdlib.Reals.Ranalysis5]
continuity_seq [in Stdlib.Reals.Rsqrt_def]
continuity_pt_finite_SF [in Stdlib.Reals.PSeries_reg]
continuity_pt_sqrt [in Stdlib.Reals.Sqrt_reg]
continuity_sin [in Stdlib.Reals.Rtrigo_reg]
continuity_cos [in Stdlib.Reals.Rtrigo1]
continuity_implies_RiemannInt [in Stdlib.Reals.RiemannInt]
continuity_finite_sum [in Stdlib.Reals.Ranalysis4]
continuous_neq_0 [in Stdlib.Reals.Ranalysis2]
contra [in Stdlib.ssr.ssrbool]
contraFF [in Stdlib.ssr.ssrbool]
contraFN [in Stdlib.ssr.ssrbool]
contraFnot [in Stdlib.ssr.ssrbool]
contraFT [in Stdlib.ssr.ssrbool]
contraL [in Stdlib.ssr.ssrbool]
contraLR [in Stdlib.ssr.ssrbool]
contraNF [in Stdlib.ssr.ssrbool]
contraNnot [in Stdlib.ssr.ssrbool]
contraPF [in Stdlib.ssr.ssrbool]
contraPN [in Stdlib.ssr.ssrbool]
contraPnot [in Stdlib.ssr.ssrbool]
contrapositive [in Stdlib.Logic.Decidable]
contraPT [in Stdlib.ssr.ssrbool]
contraR [in Stdlib.ssr.ssrbool]
contraT [in Stdlib.ssr.ssrbool]
contraTF [in Stdlib.ssr.ssrbool]
contraTnot [in Stdlib.ssr.ssrbool]
contra_notF [in Stdlib.ssr.ssrbool]
contra_notN [in Stdlib.ssr.ssrbool]
contra_notT [in Stdlib.ssr.ssrbool]
contra_not [in Stdlib.ssr.ssrbool]
cont_deriv [in Stdlib.Reals.Rderiv]
COS [in Stdlib.Reals.Rtrigo1]
cosh_0 [in Stdlib.Reals.Rtrigo_def]
cosn_no_R0 [in Stdlib.Reals.Rtrigo_def]
cos_plus_form [in Stdlib.Reals.Cos_rel]
cos_pi_plus [in Stdlib.Reals.Rtrigo_facts]
cos_pi_minus [in Stdlib.Reals.Rtrigo_facts]
cos_tan [in Stdlib.Reals.Rtrigo_facts]
cos_sin_Rabs [in Stdlib.Reals.Rtrigo_facts]
cos_sin_opp [in Stdlib.Reals.Rtrigo_facts]
cos_sin [in Stdlib.Reals.Rtrigo_facts]
cos_0 [in Stdlib.Reals.Rtrigo_def]
cos_sym [in Stdlib.Reals.Rtrigo_def]
cos_acos [in Stdlib.Reals.Ratan]
cos_asin [in Stdlib.Reals.Ratan]
cos_atan [in Stdlib.Reals.Ratan]
cos_5PI4 [in Stdlib.Reals.Rtrigo_calc]
cos_2PI3 [in Stdlib.Reals.Rtrigo_calc]
cos_PI3 [in Stdlib.Reals.Rtrigo_calc]
cos_PI6 [in Stdlib.Reals.Rtrigo_calc]
cos_3PI4 [in Stdlib.Reals.Rtrigo_calc]
cos_PI4 [in Stdlib.Reals.Rtrigo_calc]
cos_eq_0_2PI_1 [in Stdlib.Reals.Rtrigo1]
cos_eq_0_2PI_0 [in Stdlib.Reals.Rtrigo1]
cos_eq_0_1 [in Stdlib.Reals.Rtrigo1]
cos_eq_0_0 [in Stdlib.Reals.Rtrigo1]
cos_decr_1 [in Stdlib.Reals.Rtrigo1]
cos_decr_0 [in Stdlib.Reals.Rtrigo1]
cos_incr_1 [in Stdlib.Reals.Rtrigo1]
cos_incr_0 [in Stdlib.Reals.Rtrigo1]
cos_inj [in Stdlib.Reals.Rtrigo1]
cos_decreasing_1 [in Stdlib.Reals.Rtrigo1]
cos_decreasing_0 [in Stdlib.Reals.Rtrigo1]
cos_increasing_1 [in Stdlib.Reals.Rtrigo1]
cos_increasing_0 [in Stdlib.Reals.Rtrigo1]
cos_ge_0_3PI2 [in Stdlib.Reals.Rtrigo1]
cos_lt_0 [in Stdlib.Reals.Rtrigo1]
cos_le_0 [in Stdlib.Reals.Rtrigo1]
cos_ge_0 [in Stdlib.Reals.Rtrigo1]
cos_gt_0 [in Stdlib.Reals.Rtrigo1]
cos_sin_0_var [in Stdlib.Reals.Rtrigo1]
cos_sin_0 [in Stdlib.Reals.Rtrigo1]
COS_bound [in Stdlib.Reals.Rtrigo1]
cos_sin [in Stdlib.Reals.Rtrigo1]
cos_shift [in Stdlib.Reals.Rtrigo1]
cos_period [in Stdlib.Reals.Rtrigo1]
cos_2PI [in Stdlib.Reals.Rtrigo1]
cos_3PI2 [in Stdlib.Reals.Rtrigo1]
cos_neg [in Stdlib.Reals.Rtrigo1]
cos_2a_sin [in Stdlib.Reals.Rtrigo1]
cos_2a_cos [in Stdlib.Reals.Rtrigo1]
cos_2a [in Stdlib.Reals.Rtrigo1]
cos_bound [in Stdlib.Reals.Rtrigo1]
cos_PI [in Stdlib.Reals.Rtrigo1]
cos_PI2 [in Stdlib.Reals.Rtrigo1]
cos_minus [in Stdlib.Reals.Rtrigo1]
cos_pi2 [in Stdlib.Reals.Rtrigo1]
cos_plus [in Stdlib.Reals.Cos_plus]
cos2 [in Stdlib.Reals.Rtrigo1]
cos2_bound [in Stdlib.Reals.Rtrigo_facts]
count_occ_sgt [in Stdlib.Lists.List]
count_occ_repeat_excl [in Stdlib.Lists.List]
count_occ_unique [in Stdlib.Lists.List]
count_occ_repeat_neq [in Stdlib.Lists.List]
count_occ_repeat_eq [in Stdlib.Lists.List]
count_occ_alt [in Stdlib.Lists.List]
count_occ_map [in Stdlib.Lists.List]
count_occ_rev [in Stdlib.Lists.List]
count_occ_bound [in Stdlib.Lists.List]
count_occ_elt_neq [in Stdlib.Lists.List]
count_occ_elt_eq [in Stdlib.Lists.List]
count_occ_app [in Stdlib.Lists.List]
count_occ_cons_neq [in Stdlib.Lists.List]
count_occ_cons_eq [in Stdlib.Lists.List]
count_occ_inv_nil [in Stdlib.Lists.List]
count_occ_nil [in Stdlib.Lists.List]
count_occ_not_In [in Stdlib.Lists.List]
count_occ_In [in Stdlib.Lists.List]
Couple_as_union [in Stdlib.Sets.Powerset_facts]
Couple_inv [in Stdlib.Sets.Constructive_sets]
covers_is_Add [in Stdlib.Sets.Powerset_Classical_facts]
covers_Add [in Stdlib.Sets.Powerset_Classical_facts]
CPermutation_Forall2 [in Stdlib.Sorting.CPermutation]
CPermutation_image [in Stdlib.Sorting.CPermutation]
CPermutation_map_inv [in Stdlib.Sorting.CPermutation]
CPermutation_vs_cons_inv [in Stdlib.Sorting.CPermutation]
CPermutation_vs_elt_inv [in Stdlib.Sorting.CPermutation]
CPermutation_length_2_inv [in Stdlib.Sorting.CPermutation]
CPermutation_length_2 [in Stdlib.Sorting.CPermutation]
CPermutation_swap [in Stdlib.Sorting.CPermutation]
CPermutation_length_1_inv [in Stdlib.Sorting.CPermutation]
CPermutation_length_1 [in Stdlib.Sorting.CPermutation]
CPermutation_morph_cons [in Stdlib.Sorting.CPermutation]
CPermutation_cons_append [in Stdlib.Sorting.CPermutation]
CPermutation_app_rot [in Stdlib.Sorting.CPermutation]
CPermutation_app_comm [in Stdlib.Sorting.CPermutation]
CPermutation_app [in Stdlib.Sorting.CPermutation]
CPermutation_trans [in Stdlib.Sorting.CPermutation]
CPermutation_sym [in Stdlib.Sorting.CPermutation]
CPermutation_refl [in Stdlib.Sorting.CPermutation]
CPermutation_split [in Stdlib.Sorting.CPermutation]
CPermutation_nil_app_cons [in Stdlib.Sorting.CPermutation]
CPermutation_nil_cons [in Stdlib.Sorting.CPermutation]
CPermutation_nil [in Stdlib.Sorting.CPermutation]
CRabs_def2 [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRabs_def1 [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRabs_lt [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRabs_mult [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRabs_appart_0 [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRabs_pos [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRabs_triang_inv2 [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRabs_triang_inv [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRabs_le [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRabs_triang [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRabs_left [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRabs_minus_sym [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRabs_opp [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRabs_right [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRealAbsLUB [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CRealArchimedean [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CRealComplete [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CRealEq_trans [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealEq_sym [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealEq_refl [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealEq_diff [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLe_proper_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLe_proper_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLe_refl [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLe_not_lt [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLe_0R_to_single_dist [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CRealLowerBoundSpec [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CRealLowerBound_lt_scale [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CRealLtDisjunctEpsilon [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CRealLtEpsilon [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLtForget [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLtIsLinear [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CRealLt_0_1 [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_proper_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_proper_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_dec [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_irrefl [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_asym [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_above_same [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_above [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_aboveSig' [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_aboveSig [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_lpo_dec [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CRealLt_RQ_to_single_dist [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CRealLt_QR_to_single_dist [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CRealLt_QR_from_single_dist [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CRealLt_RQ_from_single_dist [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_opp_ge_le_contravar [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_gt_lt_contravar [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_involutive [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_plus_distr [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_0 [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_eq_reg_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_proper_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_proper_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_opp_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_opp_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_le_compat [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_le_lt_compat [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_le_compat_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_le_reg_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_le_reg_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_lt_reg_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_lt_reg_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_lt_compat_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_lt_compat_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_0_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_0_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_comm [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_assoc [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_red_seq [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_bound [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_opp_cauchy [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_bound [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_plus_cauchy [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_injectQPos [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_lt_trans [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_le_trans [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_lt_le_trans [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_le_lt_trans [in Stdlib.Reals.Cauchy.ConstructiveCauchyReals]
CReal_from_cauchy_bound [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CReal_from_cauchy_seq_bound [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CReal_abs_Qabs_diff [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CReal_abs_Qabs_seq [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CReal_abs_Qabs [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CReal_abs_upper_bound [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CReal_from_cauchy_cauchy [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CReal_from_cauchy_cm_mono [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CReal_cv_self' [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CReal_cv_self [in Stdlib.Reals.Cauchy.ConstructiveRcomplete]
CReal_min_contract [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_contract [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_lub_lt [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_assoc [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_max_mult_neg [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_assoc [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_lt [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_plus [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_plus [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_mult [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_sym [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_sym [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_lt_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_right [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_left [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_right [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_left [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_min_glb [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_max_lub [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_double [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_def2 [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_mult [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_gt [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_triang_inv2 [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_triang_inv [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_triang [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_lt [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_minus_sym [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_le [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_appart_0 [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_left [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_opp [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_pos [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_le_abs [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_right [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_bound [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_abs_cauchy [in Stdlib.Reals.Cauchy.ConstructiveCauchyAbs]
CReal_of_DReal_bound [in Stdlib.Reals.ClassicalDedekindReals]
CReal_of_DReal_seq_bound [in Stdlib.Reals.ClassicalDedekindReals]
CReal_of_DReal_seq_max_prec_1 [in Stdlib.Reals.ClassicalDedekindReals]
CReal_of_DReal_cauchy [in Stdlib.Reals.ClassicalDedekindReals]
CReal_mult_le_reg_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_le_reg_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_le_compat_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_le_compat_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_le_0_compat [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_invQ [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_le_compat_l_half [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_pos_appart_zero [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_eq_compat_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_eq_compat_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_eq_reg_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_lt_reg_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_lt_reg_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_mult_distr [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_1 [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_l_pos [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_0_lt_compat [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_pos_bound [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_inv_pos_cauchy [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_abs_appart_zero [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_eq_reg_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_lt_compat_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_lt_compat_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_opp_mult_distr_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_1_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_isRing [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_isRingExt [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_1_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_assoc [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_proper_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_proper_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_opp_mult_distr_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_plus_distr_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_plus_distr_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_lt_0_compat_correct [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_scale_sep0_limit [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_0_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_0_r [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_proper_0_l [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_red_scale [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_comm [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_bound [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReal_mult_cauchy [in Stdlib.Reals.Cauchy.ConstructiveCauchyRealsMult]
CReq_trans [in Stdlib.Reals.Abstract.ConstructiveReals]
CReq_sym [in Stdlib.Reals.Abstract.ConstructiveReals]
CReq_refl [in Stdlib.Reals.Abstract.ConstructiveReals]
cring_div_theory [in Stdlib.setoid_ring.Cring]
cring_power_theory [in Stdlib.setoid_ring.Cring]
cring_morph [in Stdlib.setoid_ring.Cring]
cring_almost_ring_theory [in Stdlib.setoid_ring.Cring]
cring_eq_ext [in Stdlib.setoid_ring.Cring]
CRinv_morph [in Stdlib.Reals.Abstract.ConstructiveReals]
CRinv_mult_distr [in Stdlib.Reals.Abstract.ConstructiveReals]
CRinv_1 [in Stdlib.Reals.Abstract.ConstructiveReals]
CRinv_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRle_minus [in Stdlib.Reals.Abstract.ConstructiveReals]
CRle_trans [in Stdlib.Reals.Abstract.ConstructiveReals]
CRle_lt_trans [in Stdlib.Reals.Abstract.ConstructiveReals]
CRle_refl [in Stdlib.Reals.Abstract.ConstructiveReals]
CRle_abs [in Stdlib.Reals.Abstract.ConstructiveAbs]
CRlt_minus [in Stdlib.Reals.Abstract.ConstructiveReals]
CRlt_trans_flip [in Stdlib.Reals.Abstract.ConstructiveReals]
CRlt_trans [in Stdlib.Reals.Abstract.ConstructiveReals]
CRlt_le_trans [in Stdlib.Reals.Abstract.ConstructiveReals]
CRlt_proper [in Stdlib.Reals.Abstract.ConstructiveReals]
CRlt_asym [in Stdlib.Reals.Abstract.ConstructiveReals]
CRlt_lpo_dec [in Stdlib.Reals.Abstract.ConstructiveLUB]
CRlt_max [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRlt_min [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmax_mult [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmax_min_mult_neg [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmax_assoc [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmax_lub_lt [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmax_contract [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmax_right [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmax_left [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmax_plus [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmax_sym [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmax_r [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmax_l [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmax_lub [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmin_max_mult_neg [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmin_assoc [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmin_glb [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmin_contract [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmin_lt [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmin_right [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmin_left [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmin_plus [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmin_mult [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmin_sym [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmin_r [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmin_l [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmin_lt_r [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmorph_cauchy_reverse [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_cv [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_abs [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_rat_cv [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_inv [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_appart_zero [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_appart [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult_pos_pos [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult_pos_pos_le [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult_rat [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult_inv [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult_int [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_mult_pos [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_plus [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_plus_rat [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_opp [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_one [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_zero [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_le_inv [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_le [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_proper [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_unique [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_increasing_inv [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRmorph_series_cv [in Stdlib.Reals.Abstract.ConstructiveSum]
CRmorph_INR [in Stdlib.Reals.Abstract.ConstructiveSum]
CRmorph_sum [in Stdlib.Reals.Abstract.ConstructiveSum]
CRmorph_min [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRmult_appart_reg_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_appart_reg_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_le_reg_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_le_reg_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_pos_appart_zero [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_pos_pos [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_le_compat_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_le_compat_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_le_0_compat [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_eq_reg_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_eq_reg_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_le_compat_r_half [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_le_compat_l_half [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_lt_reg_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_lt_reg_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_lt_compat_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_lt_compat_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_0_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_0_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_plus_distr_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_plus_distr_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_comm [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_assoc [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_1_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRmult_1_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRnegPartAbsMin [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRopp_mult_distr_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRopp_mult_distr_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRopp_plus_distr [in Stdlib.Reals.Abstract.ConstructiveReals]
CRopp_ge_le_contravar [in Stdlib.Reals.Abstract.ConstructiveReals]
CRopp_lt_cancel [in Stdlib.Reals.Abstract.ConstructiveReals]
CRopp_gt_lt_contravar [in Stdlib.Reals.Abstract.ConstructiveReals]
CRopp_involutive [in Stdlib.Reals.Abstract.ConstructiveReals]
CRopp_0 [in Stdlib.Reals.Abstract.ConstructiveReals]
cross_product_eq [in Stdlib.setoid_ring.Field_theory]
CRplus_appart_reg_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_appart_reg_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_comm [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_assoc [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_eq_reg_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_eq_reg_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_le_lt_compat [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_lt_le_compat [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_le_reg_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_le_reg_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_le_compat [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_le_compat_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_le_compat_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_lt_reg_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_lt_compat_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_opp_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_opp_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_0_r [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_0_l [in Stdlib.Reals.Abstract.ConstructiveReals]
CRplus_neg_rat_lt [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRplus_pos_rat_lt [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CRposPartAbsMax [in Stdlib.Reals.Abstract.ConstructiveMinMax]
CRpow_plus_distr [in Stdlib.Reals.Abstract.ConstructivePower]
CRpow_inv [in Stdlib.Reals.Abstract.ConstructivePower]
CRpow_proper [in Stdlib.Reals.Abstract.ConstructivePower]
CRpow_one [in Stdlib.Reals.Abstract.ConstructivePower]
CRpow_mult [in Stdlib.Reals.Abstract.ConstructivePower]
CRpow_gt_zero [in Stdlib.Reals.Abstract.ConstructivePower]
CRpow_ge_zero [in Stdlib.Reals.Abstract.ConstructivePower]
CRpow_ge_one [in Stdlib.Reals.Abstract.ConstructivePower]
CRsum_eq [in Stdlib.Reals.Abstract.ConstructiveSum]
CRzero_double [in Stdlib.Reals.Abstract.ConstructiveReals]
CR_cv_shift' [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_shift [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_dist_cont [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_abs_cont [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_le [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_bound_up [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_bound_down [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_open_above [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_open_below [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_growing_transit [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_const [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_scale [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_nonneg [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_minus [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_proper [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cauchy_eq [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_eq [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_unique [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_plus [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_opp [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_cv_extens [in Stdlib.Reals.Abstract.ConstructiveLimits]
CR_double [in Stdlib.Reals.Abstract.ConstructivePower]
CR_of_Q_inv [in Stdlib.Reals.Abstract.ConstructiveReals]
CR_of_Q_pos [in Stdlib.Reals.Abstract.ConstructiveReals]
CR_of_Q_opp [in Stdlib.Reals.Abstract.ConstructiveReals]
CR_of_Q_le [in Stdlib.Reals.Abstract.ConstructiveReals]
CR_Q_limit_cv [in Stdlib.Reals.Abstract.ConstructiveRealsMorphisms]
CR_of_Q_abs [in Stdlib.Reals.Abstract.ConstructiveAbs]
CR_sig_lub [in Stdlib.Reals.Abstract.ConstructiveLUB]
curry_uncurry [in Stdlib.Program.Combinators]
cutting_plane_sound [in Stdlib.micromega.ZMicromega]
CVN_R_CVS [in Stdlib.Reals.PSeries_reg]
CVN_CVU [in Stdlib.Reals.PSeries_reg]
CVN_R_sin [in Stdlib.Reals.Rtrigo_reg]
CVN_R_cos [in Stdlib.Reals.Rtrigo1]
CVU_derivable [in Stdlib.Reals.PSeries_reg]
CVU_ext_lim [in Stdlib.Reals.PSeries_reg]
CVU_cv [in Stdlib.Reals.PSeries_reg]
CVU_continuity [in Stdlib.Reals.PSeries_reg]
CV_shift' [in Stdlib.Reals.Rseries]
CV_shift [in Stdlib.Reals.Rseries]
cv_pow_half [in Stdlib.Reals.Rsqrt_def]
cv_dicho [in Stdlib.Reals.Rsqrt_def]
CV_ALT [in Stdlib.Reals.AltSeries]
CV_ALT_step4 [in Stdlib.Reals.AltSeries]
CV_ALT_step3 [in Stdlib.Reals.AltSeries]
CV_ALT_step2 [in Stdlib.Reals.AltSeries]
CV_ALT_step1 [in Stdlib.Reals.AltSeries]
CV_ALT_step0 [in Stdlib.Reals.AltSeries]
cv_cauchy_2 [in Stdlib.Reals.PartSum]
cv_cauchy_1 [in Stdlib.Reals.PartSum]
cv_speed_pow_fact [in Stdlib.Reals.SeqProp]
cv_infty_cv_R0_depr [in Stdlib.Reals.SeqProp]
cv_infty_cv_0 [in Stdlib.Reals.SeqProp]
CV_minus [in Stdlib.Reals.SeqProp]
CV_opp [in Stdlib.Reals.SeqProp]
CV_mult [in Stdlib.Reals.SeqProp]
CV_Cauchy [in Stdlib.Reals.SeqProp]
cv_cvabs [in Stdlib.Reals.SeqProp]
CV_plus [in Stdlib.Reals.SeqProp]
CyclicRing.add_opp_diag_r [in Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.add_opp_r [in Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.add_assoc [in Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.add_comm [in Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.add_0_l [in Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.CyclicRing [in Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.eqb_correct [in Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.eqb_eq [in Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.mul_add_distr_r [in Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.mul_assoc [in Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.mul_comm [in Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms]
CyclicRing.mul_1_l [in Stdlib.Numbers.Cyclic.Abstract.CyclicAxioms]
C_maj [in Stdlib.Reals.Rprod]
C1_cvg [in Stdlib.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 | (26016 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 | (1003 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 | (811 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 | (1771 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) |
| 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 | (961 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 | (11981 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 | (508 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (308 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (479 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 | (496 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 | (905 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 | (1199 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 | (4840 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (166 entries) |