A
A [constructor, in Coq.Init.Datatypes]
a [constructor, in Coq.ZArith.Znumtheory]
A [constructor, in Coq.Init.Logic]
A [constructor, in Coq.Init.Logic]
A [constructor, in Coq.Init.Specif]
A [constructor, in Coq.Init.Specif]
a [constructor, in Coq.ZArith.Znumtheory]
A [constructor, in Coq.Init.Specif]
A [constructor, in Coq.Init.Logic]
A [constructor, in Coq.Init.Specif]
A [definition, in Coq.Lists.MonoList]
A [constructor, in Coq.Init.Specif]
aapp [definition, in Coq.IntMap.Mapiter]
aapp_length [lemma, in Coq.IntMap.Lsort]
AbsList [definition, in Coq.Reals.RList]
AbsList_P1 [lemma, in Coq.Reals.RList]
AbsList_P2 [lemma, in Coq.Reals.RList]
absoption_andb [lemma, in Coq.Bool.Bool]
absoption_orb [lemma, in Coq.Bool.Bool]
absurd [lemma, in Coq.Init.Logic]
absurd_set [lemma, in Coq.Init.Specif]
AC [lemma, in Coq.Logic.Diaconescu]
AC [lemma, in Coq.Logic.Berardi]
Acc [inductive, in Coq.Init.Wf]
acc_app [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]
acc_A_B_lexprod [lemma, in Coq.Wellfounded.Lexicographic_Product]
acc_A_sum [lemma, in Coq.Wellfounded.Disjoint_Union]
acc_B_sum [lemma, in Coq.Wellfounded.Disjoint_Union]
Acc_clos_trans [lemma, in Coq.Wellfounded.Transitive_Closure]
Acc_incl [lemma, in Coq.Wellfounded.Inclusion]
Acc_intro [constructor, in Coq.Init.Wf]
Acc_inv [lemma, in Coq.Init.Wf]
Acc_inverse_image [lemma, in Coq.Wellfounded.Inverse_Image]
Acc_inverse_rel [lemma, in Coq.Wellfounded.Inverse_Image]
Acc_inv_trans [lemma, in Coq.Wellfounded.Transitive_Closure]
Acc_iter [definition, in Coq.Init.Wf]
Acc_iter_2 [definition, in Coq.Init.Wf]
Acc_rec [definition, in Coq.Init.Wf]
Acc_rect [definition, in Coq.Init.Wf]
Acc_swapprod [lemma, in Coq.Wellfounded.Lexicographic_Product]
Acc_symprod [lemma, in Coq.Wellfounded.Lexicographic_Product]
Acc_union [lemma, in Coq.Wellfounded.Union]
acons [definition, in Coq.IntMap.Mapiter]
AC_IF [lemma, in Coq.Logic.Berardi]
ad [inductive, in Coq.IntMap.Addr]
Adalloc [library]
adapted_couple [definition, in Coq.Reals.RiemannInt_SF]
adapted_couple_opt [definition, in Coq.Reals.RiemannInt_SF]
Add [definition, in Coq.Sets.Ensembles]
Addec [library]
Addr [library]
Add_commutative [lemma, in Coq.Sets.Powerset_facts]
Add_commutative' [lemma, in Coq.Sets.Powerset_facts]
Add_covers [lemma, in Coq.Sets.Powerset_Classical_facts]
Add_distributes [lemma, in Coq.Sets.Powerset_facts]
Add_intro1 [lemma, in Coq.Sets.Constructive_sets]
Add_intro2 [lemma, in Coq.Sets.Constructive_sets]
Add_inv [lemma, in Coq.Sets.Constructive_sets]
Add_not_Empty [lemma, in Coq.Sets.Constructive_sets]
Add_preserves_Finite [lemma, in Coq.Sets.Finite_sets_facts]
add_soustr_xy [lemma, in Coq.Sets.Powerset_Classical_facts]
add_soustr_1 [lemma, in Coq.Sets.Powerset_Classical_facts]
add_soustr_2 [lemma, in Coq.Sets.Powerset_Classical_facts]
adf_xor [definition, in Coq.IntMap.Addr]
adf_xor_assoc [lemma, in Coq.IntMap.Addr]
adf_xor_eq [lemma, in Coq.IntMap.Addr]
adhDa [definition, in Coq.Reals.Rlimit]
adherence [definition, in Coq.Reals.Rtopology]
adherence_P1 [lemma, in Coq.Reals.Rtopology]
adherence_P2 [lemma, in Coq.Reals.Rtopology]
adherence_P3 [lemma, in Coq.Reals.Rtopology]
adherence_P4 [lemma, in Coq.Reals.Rtopology]
Adist [library]
ad_alloc_opt [definition, in Coq.IntMap.Adalloc]
ad_alloc_opt_allocates [lemma, in Coq.IntMap.Adalloc]
ad_alloc_opt_allocates_1 [lemma, in Coq.IntMap.Adalloc]
ad_alloc_opt_optimal [lemma, in Coq.IntMap.Adalloc]
ad_alloc_opt_optimal_1 [lemma, in Coq.IntMap.Adalloc]
ad_bit [definition, in Coq.IntMap.Addr]
ad_bit_0 [definition, in Coq.IntMap.Addr]
ad_bit_0_correct [lemma, in Coq.IntMap.Addr]
ad_bit_0_gt [lemma, in Coq.IntMap.Lsort]
ad_bit_0_less [lemma, in Coq.IntMap.Lsort]
ad_bit_0_neq [lemma, in Coq.IntMap.Addec]
ad_bit_0_0_not_double_plus_un [lemma, in Coq.IntMap.Addec]
ad_bit_0_1_not_double [lemma, in Coq.IntMap.Addec]
ad_bit_1 [definition, in Coq.IntMap.Addr]
ad_comp_double_inj [lemma, in Coq.IntMap.Mapiter]
ad_comp_double_monotonic [lemma, in Coq.IntMap.Lsort]
ad_comp_double_plus_un_inj [lemma, in Coq.IntMap.Mapiter]
ad_comp_double_plus_un_monotonic [lemma, in Coq.IntMap.Lsort]
ad_comp_monotonic [lemma, in Coq.IntMap.Lsort]
ad_div_bit_eq [lemma, in Coq.IntMap.Addec]
ad_div_bit_neq [lemma, in Coq.IntMap.Addec]
ad_div_eq [lemma, in Coq.IntMap.Addec]
ad_div_neq [lemma, in Coq.IntMap.Addec]
ad_div_2 [definition, in Coq.IntMap.Addr]
ad_div_2_correct [lemma, in Coq.IntMap.Addr]
ad_div_2_double [lemma, in Coq.IntMap.Addr]
ad_div_2_double_plus_un [lemma, in Coq.IntMap.Addr]
ad_double [definition, in Coq.IntMap.Addr]
ad_double_bit_0 [lemma, in Coq.IntMap.Addr]
ad_double_div_2 [lemma, in Coq.IntMap.Addr]
ad_double_inj [lemma, in Coq.IntMap.Addr]
ad_double_monotonic [lemma, in Coq.IntMap.Lsort]
ad_double_or_double_plus_un [lemma, in Coq.IntMap.Addec]
ad_double_plus_un [definition, in Coq.IntMap.Addr]
ad_double_plus_un_bit_0 [lemma, in Coq.IntMap.Addr]
ad_double_plus_un_div_2 [lemma, in Coq.IntMap.Addr]
ad_double_plus_un_inj [lemma, in Coq.IntMap.Addr]
ad_double_plus_un_monotonic [lemma, in Coq.IntMap.Lsort]
ad_eq [definition, in Coq.IntMap.Addec]
ad_eq_comm [lemma, in Coq.IntMap.Addec]
ad_eq_complete [lemma, in Coq.IntMap.Addec]
ad_eq_correct [lemma, in Coq.IntMap.Addec]
ad_eq_1 [definition, in Coq.IntMap.Addec]
ad_faithful [lemma, in Coq.IntMap.Addr]
ad_faithful_1 [lemma, in Coq.IntMap.Addr]
ad_faithful_2 [lemma, in Coq.IntMap.Addr]
ad_faithful_3 [lemma, in Coq.IntMap.Addr]
ad_faithful_4 [lemma, in Coq.IntMap.Addr]
ad_ind_double [lemma, in Coq.IntMap.Lsort]
ad_inj [definition, in Coq.IntMap.Mapiter]
ad_in_elems_in_list [lemma, in Coq.IntMap.Maplists]
ad_in_list [definition, in Coq.IntMap.Maplists]
ad_in_list_app [lemma, in Coq.IntMap.Maplists]
ad_in_list_app_1 [lemma, in Coq.IntMap.Maplists]
ad_in_list_forms_circuit [lemma, in Coq.IntMap.Maplists]
ad_in_list_l [lemma, in Coq.IntMap.Maplists]
ad_in_list_of_dom_in_dom [lemma, in Coq.IntMap.Maplists]
ad_in_list_r [lemma, in Coq.IntMap.Maplists]
ad_in_list_rev [lemma, in Coq.IntMap.Maplists]
ad_le [definition, in Coq.IntMap.Adalloc]
ad_less [definition, in Coq.IntMap.Lsort]
ad_less_def_1 [lemma, in Coq.IntMap.Lsort]
ad_less_def_2 [lemma, in Coq.IntMap.Lsort]
ad_less_def_3 [lemma, in Coq.IntMap.Lsort]
ad_less_def_4 [lemma, in Coq.IntMap.Lsort]
ad_less_not_refl [lemma, in Coq.IntMap.Lsort]
ad_less_total [lemma, in Coq.IntMap.Lsort]
ad_less_trans [lemma, in Coq.IntMap.Lsort]
ad_less_z [lemma, in Coq.IntMap.Lsort]
ad_less_1 [definition, in Coq.IntMap.Lsort]
ad_le_antisym [lemma, in Coq.IntMap.Adalloc]
ad_le_double_mono [lemma, in Coq.IntMap.Adalloc]
ad_le_double_mono_conv [lemma, in Coq.IntMap.Adalloc]
ad_le_double_plus_un_mono [lemma, in Coq.IntMap.Adalloc]
ad_le_double_plus_un_mono_conv [lemma, in Coq.IntMap.Adalloc]
ad_le_lt_trans [lemma, in Coq.IntMap.Adalloc]
ad_le_refl [lemma, in Coq.IntMap.Adalloc]
ad_le_trans [lemma, in Coq.IntMap.Adalloc]
ad_list_app_length [lemma, in Coq.IntMap.Maplists]
ad_list_app_rev [lemma, in Coq.IntMap.Maplists]
ad_list_card [lemma, in Coq.IntMap.Maplists]
ad_list_Elems [lemma, in Coq.IntMap.Maplists]
ad_list_has_circuit_stutters [lemma, in Coq.IntMap.Maplists]
ad_list_not_stutters_card [lemma, in Coq.IntMap.Maplists]
ad_list_not_stutters_card_conv [lemma, in Coq.IntMap.Maplists]
ad_list_of_dom [definition, in Coq.IntMap.Maplists]
ad_list_of_dom_card [lemma, in Coq.IntMap.Maplists]
ad_list_of_dom_card_1 [lemma, in Coq.IntMap.Maplists]
ad_list_of_dom_Dom [lemma, in Coq.IntMap.Maplists]
ad_list_of_dom_Dom_1 [lemma, in Coq.IntMap.Maplists]
ad_list_of_dom_not_stutters [lemma, in Coq.IntMap.Maplists]
ad_list_rev_length [lemma, in Coq.IntMap.Maplists]
ad_list_stutters [definition, in Coq.IntMap.Maplists]
ad_list_stutters_app_conv_l [lemma, in Coq.IntMap.Maplists]
ad_list_stutters_app_conv_r [lemma, in Coq.IntMap.Maplists]
ad_list_stutters_app_l [lemma, in Coq.IntMap.Maplists]
ad_list_stutters_app_r [lemma, in Coq.IntMap.Maplists]
ad_list_stutters_card [lemma, in Coq.IntMap.Maplists]
ad_list_stutters_card_conv [lemma, in Coq.IntMap.Maplists]
ad_list_stutters_has_circuit [lemma, in Coq.IntMap.Maplists]
ad_list_stutters_permute [lemma, in Coq.IntMap.Maplists]
ad_list_stutters_prev_conv_l [lemma, in Coq.IntMap.Maplists]
ad_list_stutters_prev_conv_r [lemma, in Coq.IntMap.Maplists]
ad_list_stutters_prev_l [lemma, in Coq.IntMap.Maplists]
ad_list_stutters_prev_r [lemma, in Coq.IntMap.Maplists]
ad_list_stutters_rev [lemma, in Coq.IntMap.Maplists]
ad_lt_double_mono [lemma, in Coq.IntMap.Adalloc]
ad_lt_double_mono_conv [lemma, in Coq.IntMap.Adalloc]
ad_lt_double_plus_un_mono [lemma, in Coq.IntMap.Adalloc]
ad_lt_double_plus_un_mono_conv [lemma, in Coq.IntMap.Adalloc]
ad_lt_le_trans [lemma, in Coq.IntMap.Adalloc]
ad_lt_le_weak [lemma, in Coq.IntMap.Adalloc]
ad_lt_trans [lemma, in Coq.IntMap.Adalloc]
ad_min [definition, in Coq.IntMap.Adalloc]
ad_min_choice [lemma, in Coq.IntMap.Adalloc]
ad_min_le_1 [lemma, in Coq.IntMap.Adalloc]
ad_min_le_2 [lemma, in Coq.IntMap.Adalloc]
ad_min_le_3 [lemma, in Coq.IntMap.Adalloc]
ad_min_le_4 [lemma, in Coq.IntMap.Adalloc]
ad_min_le_5 [lemma, in Coq.IntMap.Adalloc]
ad_min_lt_3 [lemma, in Coq.IntMap.Adalloc]
ad_min_lt_4 [lemma, in Coq.IntMap.Adalloc]
ad_monotonic [definition, in Coq.IntMap.Lsort]
ad_neg_bit_0 [lemma, in Coq.IntMap.Addr]
ad_neg_bit_0_1 [lemma, in Coq.IntMap.Addr]
ad_neg_bit_0_2 [lemma, in Coq.IntMap.Addr]
ad_neq [lemma, in Coq.IntMap.Addec]
ad_not_div_2_not_double [lemma, in Coq.IntMap.Addec]
ad_not_div_2_not_double_plus_un [lemma, in Coq.IntMap.Addec]
ad_of_nat [definition, in Coq.IntMap.Adalloc]
ad_of_nat_of_ad [lemma, in Coq.IntMap.Adalloc]
ad_pdist [definition, in Coq.IntMap.Adist]
ad_pdist_comm [lemma, in Coq.IntMap.Adist]
ad_pdist_eq_1 [lemma, in Coq.IntMap.Adist]
ad_pdist_eq_2 [lemma, in Coq.IntMap.Adist]
ad_pdist_ultra [lemma, in Coq.IntMap.Adist]
ad_plength [definition, in Coq.IntMap.Adist]
ad_plength_first_one [lemma, in Coq.IntMap.Adist]
ad_plength_infty [lemma, in Coq.IntMap.Adist]
ad_plength_lb [lemma, in Coq.IntMap.Adist]
ad_plength_one [lemma, in Coq.IntMap.Adist]
ad_plength_ub [lemma, in Coq.IntMap.Adist]
ad_plength_ultra [lemma, in Coq.IntMap.Adist]
ad_plength_ultra_1 [lemma, in Coq.IntMap.Adist]
ad_plength_zeros [lemma, in Coq.IntMap.Adist]
ad_plength_1 [definition, in Coq.IntMap.Adist]
ad_rec_double [lemma, in Coq.IntMap.Lsort]
ad_same_bit_0 [lemma, in Coq.IntMap.Addr]
ad_sum [lemma, in Coq.IntMap.Addr]
ad_x [constructor, in Coq.IntMap.Addr]
ad_xor [definition, in Coq.IntMap.Addr]
ad_xor_assoc [lemma, in Coq.IntMap.Addr]
ad_xor_bit_0 [lemma, in Coq.IntMap.Addr]
ad_xor_comm [lemma, in Coq.IntMap.Addr]
ad_xor_div_2 [lemma, in Coq.IntMap.Addr]
ad_xor_eq [lemma, in Coq.IntMap.Addr]
ad_xor_eq_false [lemma, in Coq.IntMap.Addec]
ad_xor_eq_true [lemma, in Coq.IntMap.Addec]
ad_xor_neutral_left [lemma, in Coq.IntMap.Addr]
ad_xor_neutral_right [lemma, in Coq.IntMap.Addr]
ad_xor_nilpotent [lemma, in Coq.IntMap.Addr]
ad_xor_semantics [lemma, in Coq.IntMap.Addr]
ad_xor_sem_1 [lemma, in Coq.IntMap.Addr]
ad_xor_sem_2 [lemma, in Coq.IntMap.Addr]
ad_xor_sem_3 [lemma, in Coq.IntMap.Addr]
ad_xor_sem_4 [lemma, in Coq.IntMap.Addr]
ad_xor_sem_5 [lemma, in Coq.IntMap.Addr]
ad_xor_sem_6 [lemma, in Coq.IntMap.Addr]
ad_z [constructor, in Coq.IntMap.Addr]
ad_z_less_1 [lemma, in Coq.IntMap.Lsort]
ad_z_less_2 [lemma, in Coq.IntMap.Lsort]
Alembert [library]
AlembertC3_step1 [lemma, in Coq.Reals.Alembert]
AlembertC3_step2 [lemma, in Coq.Reals.Alembert]
Alembert_cos [lemma, in Coq.Reals.Rtrigo_def]
Alembert_C1 [lemma, in Coq.Reals.Alembert]
Alembert_C2 [lemma, in Coq.Reals.Alembert]
Alembert_C3 [lemma, in Coq.Reals.Alembert]
Alembert_C4 [lemma, in Coq.Reals.Alembert]
Alembert_C5 [lemma, in Coq.Reals.Alembert]
Alembert_C6 [lemma, in Coq.Reals.Alembert]
Alembert_exp [lemma, in Coq.Reals.Rtrigo_fun]
Alembert_sin [lemma, in Coq.Reals.Rtrigo_def]
alist [definition, in Coq.IntMap.Mapiter]
alist_canonical [lemma, in Coq.IntMap.Lsort]
alist_conc_sorted [lemma, in Coq.IntMap.Lsort]
alist_MapMerge_semantics [lemma, in Coq.IntMap.Mapiter]
alist_MapMerge_semantics_disjoint [lemma, in Coq.IntMap.Mapiter]
alist_nth_ad [definition, in Coq.IntMap.Lsort]
alist_nth_ad_aapp_1 [lemma, in Coq.IntMap.Lsort]
alist_nth_ad_aapp_2 [lemma, in Coq.IntMap.Lsort]
alist_nth_ad_semantics [lemma, in Coq.IntMap.Lsort]
alist_of_Map [definition, in Coq.IntMap.Mapiter]
alist_of_Map_nth_ad [lemma, in Coq.IntMap.Lsort]
alist_of_Map_of_alist [lemma, in Coq.IntMap.Mapiter]
alist_of_Map_of_alist_c [lemma, in Coq.IntMap.Mapc]
alist_of_Map_semantics [lemma, in Coq.IntMap.Mapiter]
alist_of_Map_semantics_1 [lemma, in Coq.IntMap.Mapiter]
alist_of_Map_semantics_1_1 [lemma, in Coq.IntMap.Mapiter]
alist_of_Map_sorts [lemma, in Coq.IntMap.Lsort]
alist_of_Map_sorts1 [lemma, in Coq.IntMap.Lsort]
alist_of_Map_sorts2 [lemma, in Coq.IntMap.Lsort]
alist_of_Map_sorts_1 [lemma, in Coq.IntMap.Lsort]
alist_semantics [definition, in Coq.IntMap.Mapiter]
alist_semantics_app [lemma, in Coq.IntMap.Mapiter]
alist_semantics_disjoint_comm [lemma, in Coq.IntMap.Mapiter]
alist_semantics_nth_ad [lemma, in Coq.IntMap.Lsort]
alist_semantics_same_tail [lemma, in Coq.IntMap.Lsort]
alist_semantics_tail [lemma, in Coq.IntMap.Lsort]
alist_sorted [definition, in Coq.IntMap.Lsort]
alist_sorted_imp_1 [lemma, in Coq.IntMap.Lsort]
alist_sorted_tail [lemma, in Coq.IntMap.Lsort]
alist_sorted_1 [definition, in Coq.IntMap.Lsort]
alist_sorted_1_imp_2 [lemma, in Coq.IntMap.Lsort]
alist_sorted_2 [definition, in Coq.IntMap.Lsort]
alist_sorted_2_imp [lemma, in Coq.IntMap.Lsort]
alist_too_low [lemma, in Coq.IntMap.Lsort]
all [definition, in Coq.Init.Logic]
Allmaps [library]
AllS [inductive, in Coq.Lists.TheoryList]
AllS_assoc [inductive, in Coq.Lists.TheoryList]
allS_assoc_cons [constructor, in Coq.Lists.TheoryList]
allS_assoc_nil [constructor, in Coq.Lists.TheoryList]
allS_cons [constructor, in Coq.Lists.TheoryList]
allS_nil [constructor, in Coq.Lists.TheoryList]
all_not_not_ex [lemma, in Coq.Logic.Classical_Pred_Type]
all_not_not_ex [lemma, in Coq.Logic.Classical_Pred_Set]
alternated_series [lemma, in Coq.Reals.AltSeries]
alternated_series_ineq [lemma, in Coq.Reals.AltSeries]
AltSeries [library]
and [inductive, in Coq.Init.Logic]
andb [definition, in Coq.Bool.Bool]
andb_assoc [lemma, in Coq.Bool.Bool]
andb_b_false [lemma, in Coq.Bool.Bool]
andb_b_true [lemma, in Coq.Bool.Bool]
andb_comm [lemma, in Coq.Bool.Bool]
andb_false_b [lemma, in Coq.Bool.Bool]
andb_false_elim [definition, in Coq.Bool.Bool]
andb_false_intro1 [lemma, in Coq.Bool.Bool]
andb_false_intro2 [lemma, in Coq.Bool.Bool]
andb_neg_b [lemma, in Coq.Bool.Bool]
andb_prop [lemma, in Coq.Bool.Bool]
andb_prop2 [lemma, in Coq.Bool.Bool]
andb_true_b [lemma, in Coq.Bool.Bool]
andb_true_eq [definition, in Coq.Bool.Bool]
andb_true_intro [lemma, in Coq.Bool.Bool]
andb_true_intro2 [lemma, in Coq.Bool.Bool]
and_not_or [lemma, in Coq.Logic.Classical_Prop]
anil [definition, in Coq.IntMap.Mapiter]
antiderivative [definition, in Coq.Reals.Ranalysis1]
antiderivative_P1 [lemma, in Coq.Reals.NewtonInt]
antiderivative_P2 [lemma, in Coq.Reals.NewtonInt]
antiderivative_P3 [lemma, in Coq.Reals.NewtonInt]
antiderivative_P4 [lemma, in Coq.Reals.NewtonInt]
antiderivative_Ucte [lemma, in Coq.Reals.MVT]
antisymmetric [definition, in Coq.Relations.Relation_Definitions]
Antisymmetric [definition, in Coq.Sets.Relations_1]
app [definition, in Coq.Lists.MonoList]
app [definition, in Coq.Lists.List]
Approximant [inductive, in Coq.Sets.Infinite_sets]
approximants_grow [lemma, in Coq.Sets.Infinite_sets]
approximants_grow' [lemma, in Coq.Sets.Infinite_sets]
approximant_can_be_any_size [lemma, in Coq.Sets.Infinite_sets]
approx_maj [lemma, in Coq.Reals.SeqProp]
approx_min [lemma, in Coq.Reals.SeqProp]
AppVar [axiom, in Coq.Reals.Ranalysis]
app_ass [lemma, in Coq.Lists.List]
app_ass [lemma, in Coq.Lists.MonoList]
app_comm_cons [lemma, in Coq.Lists.List]
app_cons_not_nil [lemma, in Coq.Lists.List]
app_eq_nil [lemma, in Coq.Lists.List]
app_eq_unit [lemma, in Coq.Lists.List]
app_inj_tail [lemma, in Coq.Lists.List]
app_length [lemma, in Coq.IntMap.Lsort]
app_nil_end [lemma, in Coq.Lists.List]
app_nil_end [lemma, in Coq.Lists.MonoList]
app_Rlist [definition, in Coq.Reals.RList]
archimed [axiom, in Coq.Reals.Raxioms]
archimed_cor1 [lemma, in Coq.Reals.Rtrigo_def]
Arith [library]
ArithProp [library]
assoc [definition, in Coq.Lists.TheoryList]
Assoc [lemma, in Coq.Lists.TheoryList]
ass_app [lemma, in Coq.Lists.MonoList]
ass_app [lemma, in Coq.Lists.List]
aux [lemma, in Coq.Logic.ClassicalFacts]
auxiliary [library]
A1 [definition, in Coq.Reals.Cos_rel]
A1_cvg [lemma, in Coq.Reals.Cos_rel]
This page has been generated by coqdoc