A (lemma)
aapp_length [in Coq.IntMap.Lsort]
AbsList_P1 [in Coq.Reals.RList]
AbsList_P2 [in Coq.Reals.RList]
absoption_andb [in Coq.Bool.Bool]
absoption_orb [in Coq.Bool.Bool]
absurd [in Coq.Init.Logic]
absurd_set [in Coq.Init.Specif]
AC [in Coq.Logic.Diaconescu]
AC [in Coq.Logic.Berardi]
acc_app [in Coq.Wellfounded.Lexicographic_Exponentiation]
acc_A_B_lexprod [in Coq.Wellfounded.Lexicographic_Product]
acc_A_sum [in Coq.Wellfounded.Disjoint_Union]
acc_B_sum [in Coq.Wellfounded.Disjoint_Union]
Acc_clos_trans [in Coq.Wellfounded.Transitive_Closure]
Acc_incl [in Coq.Wellfounded.Inclusion]
Acc_inv [in Coq.Init.Wf]
Acc_inverse_image [in Coq.Wellfounded.Inverse_Image]
Acc_inverse_rel [in Coq.Wellfounded.Inverse_Image]
Acc_inv_trans [in Coq.Wellfounded.Transitive_Closure]
Acc_swapprod [in Coq.Wellfounded.Lexicographic_Product]
Acc_symprod [in Coq.Wellfounded.Lexicographic_Product]
Acc_union [in Coq.Wellfounded.Union]
AC_IF [in Coq.Logic.Berardi]
Add_commutative [in Coq.Sets.Powerset_facts]
Add_commutative' [in Coq.Sets.Powerset_facts]
Add_covers [in Coq.Sets.Powerset_Classical_facts]
Add_distributes [in Coq.Sets.Powerset_facts]
Add_intro1 [in Coq.Sets.Constructive_sets]
Add_intro2 [in Coq.Sets.Constructive_sets]
Add_inv [in Coq.Sets.Constructive_sets]
Add_not_Empty [in Coq.Sets.Constructive_sets]
Add_preserves_Finite [in Coq.Sets.Finite_sets_facts]
add_soustr_xy [in Coq.Sets.Powerset_Classical_facts]
add_soustr_1 [in Coq.Sets.Powerset_Classical_facts]
add_soustr_2 [in Coq.Sets.Powerset_Classical_facts]
adf_xor_assoc [in Coq.IntMap.Addr]
adf_xor_eq [in Coq.IntMap.Addr]
adherence_P1 [in Coq.Reals.Rtopology]
adherence_P2 [in Coq.Reals.Rtopology]
adherence_P3 [in Coq.Reals.Rtopology]
adherence_P4 [in Coq.Reals.Rtopology]
ad_alloc_opt_allocates [in Coq.IntMap.Adalloc]
ad_alloc_opt_allocates_1 [in Coq.IntMap.Adalloc]
ad_alloc_opt_optimal [in Coq.IntMap.Adalloc]
ad_alloc_opt_optimal_1 [in Coq.IntMap.Adalloc]
ad_bit_0_correct [in Coq.IntMap.Addr]
ad_bit_0_gt [in Coq.IntMap.Lsort]
ad_bit_0_less [in Coq.IntMap.Lsort]
ad_bit_0_neq [in Coq.IntMap.Addec]
ad_bit_0_0_not_double_plus_un [in Coq.IntMap.Addec]
ad_bit_0_1_not_double [in Coq.IntMap.Addec]
ad_comp_double_inj [in Coq.IntMap.Mapiter]
ad_comp_double_monotonic [in Coq.IntMap.Lsort]
ad_comp_double_plus_un_inj [in Coq.IntMap.Mapiter]
ad_comp_double_plus_un_monotonic [in Coq.IntMap.Lsort]
ad_comp_monotonic [in Coq.IntMap.Lsort]
ad_div_bit_eq [in Coq.IntMap.Addec]
ad_div_bit_neq [in Coq.IntMap.Addec]
ad_div_eq [in Coq.IntMap.Addec]
ad_div_neq [in Coq.IntMap.Addec]
ad_div_2_correct [in Coq.IntMap.Addr]
ad_div_2_double [in Coq.IntMap.Addr]
ad_div_2_double_plus_un [in Coq.IntMap.Addr]
ad_double_bit_0 [in Coq.IntMap.Addr]
ad_double_div_2 [in Coq.IntMap.Addr]
ad_double_inj [in Coq.IntMap.Addr]
ad_double_monotonic [in Coq.IntMap.Lsort]
ad_double_or_double_plus_un [in Coq.IntMap.Addec]
ad_double_plus_un_bit_0 [in Coq.IntMap.Addr]
ad_double_plus_un_div_2 [in Coq.IntMap.Addr]
ad_double_plus_un_inj [in Coq.IntMap.Addr]
ad_double_plus_un_monotonic [in Coq.IntMap.Lsort]
ad_eq_comm [in Coq.IntMap.Addec]
ad_eq_complete [in Coq.IntMap.Addec]
ad_eq_correct [in Coq.IntMap.Addec]
ad_faithful [in Coq.IntMap.Addr]
ad_faithful_1 [in Coq.IntMap.Addr]
ad_faithful_2 [in Coq.IntMap.Addr]
ad_faithful_3 [in Coq.IntMap.Addr]
ad_faithful_4 [in Coq.IntMap.Addr]
ad_ind_double [in Coq.IntMap.Lsort]
ad_in_elems_in_list [in Coq.IntMap.Maplists]
ad_in_list_app [in Coq.IntMap.Maplists]
ad_in_list_app_1 [in Coq.IntMap.Maplists]
ad_in_list_forms_circuit [in Coq.IntMap.Maplists]
ad_in_list_l [in Coq.IntMap.Maplists]
ad_in_list_of_dom_in_dom [in Coq.IntMap.Maplists]
ad_in_list_r [in Coq.IntMap.Maplists]
ad_in_list_rev [in Coq.IntMap.Maplists]
ad_less_def_1 [in Coq.IntMap.Lsort]
ad_less_def_2 [in Coq.IntMap.Lsort]
ad_less_def_3 [in Coq.IntMap.Lsort]
ad_less_def_4 [in Coq.IntMap.Lsort]
ad_less_not_refl [in Coq.IntMap.Lsort]
ad_less_total [in Coq.IntMap.Lsort]
ad_less_trans [in Coq.IntMap.Lsort]
ad_less_z [in Coq.IntMap.Lsort]
ad_le_antisym [in Coq.IntMap.Adalloc]
ad_le_double_mono [in Coq.IntMap.Adalloc]
ad_le_double_mono_conv [in Coq.IntMap.Adalloc]
ad_le_double_plus_un_mono [in Coq.IntMap.Adalloc]
ad_le_double_plus_un_mono_conv [in Coq.IntMap.Adalloc]
ad_le_lt_trans [in Coq.IntMap.Adalloc]
ad_le_refl [in Coq.IntMap.Adalloc]
ad_le_trans [in Coq.IntMap.Adalloc]
ad_list_app_length [in Coq.IntMap.Maplists]
ad_list_app_rev [in Coq.IntMap.Maplists]
ad_list_card [in Coq.IntMap.Maplists]
ad_list_Elems [in Coq.IntMap.Maplists]
ad_list_has_circuit_stutters [in Coq.IntMap.Maplists]
ad_list_not_stutters_card [in Coq.IntMap.Maplists]
ad_list_not_stutters_card_conv [in Coq.IntMap.Maplists]
ad_list_of_dom_card [in Coq.IntMap.Maplists]
ad_list_of_dom_card_1 [in Coq.IntMap.Maplists]
ad_list_of_dom_Dom [in Coq.IntMap.Maplists]
ad_list_of_dom_Dom_1 [in Coq.IntMap.Maplists]
ad_list_of_dom_not_stutters [in Coq.IntMap.Maplists]
ad_list_rev_length [in Coq.IntMap.Maplists]
ad_list_stutters_app_conv_l [in Coq.IntMap.Maplists]
ad_list_stutters_app_conv_r [in Coq.IntMap.Maplists]
ad_list_stutters_app_l [in Coq.IntMap.Maplists]
ad_list_stutters_app_r [in Coq.IntMap.Maplists]
ad_list_stutters_card [in Coq.IntMap.Maplists]
ad_list_stutters_card_conv [in Coq.IntMap.Maplists]
ad_list_stutters_has_circuit [in Coq.IntMap.Maplists]
ad_list_stutters_permute [in Coq.IntMap.Maplists]
ad_list_stutters_prev_conv_l [in Coq.IntMap.Maplists]
ad_list_stutters_prev_conv_r [in Coq.IntMap.Maplists]
ad_list_stutters_prev_l [in Coq.IntMap.Maplists]
ad_list_stutters_prev_r [in Coq.IntMap.Maplists]
ad_list_stutters_rev [in Coq.IntMap.Maplists]
ad_lt_double_mono [in Coq.IntMap.Adalloc]
ad_lt_double_mono_conv [in Coq.IntMap.Adalloc]
ad_lt_double_plus_un_mono [in Coq.IntMap.Adalloc]
ad_lt_double_plus_un_mono_conv [in Coq.IntMap.Adalloc]
ad_lt_le_trans [in Coq.IntMap.Adalloc]
ad_lt_le_weak [in Coq.IntMap.Adalloc]
ad_lt_trans [in Coq.IntMap.Adalloc]
ad_min_choice [in Coq.IntMap.Adalloc]
ad_min_le_1 [in Coq.IntMap.Adalloc]
ad_min_le_2 [in Coq.IntMap.Adalloc]
ad_min_le_3 [in Coq.IntMap.Adalloc]
ad_min_le_4 [in Coq.IntMap.Adalloc]
ad_min_le_5 [in Coq.IntMap.Adalloc]
ad_min_lt_3 [in Coq.IntMap.Adalloc]
ad_min_lt_4 [in Coq.IntMap.Adalloc]
ad_neg_bit_0 [in Coq.IntMap.Addr]
ad_neg_bit_0_1 [in Coq.IntMap.Addr]
ad_neg_bit_0_2 [in Coq.IntMap.Addr]
ad_neq [in Coq.IntMap.Addec]
ad_not_div_2_not_double [in Coq.IntMap.Addec]
ad_not_div_2_not_double_plus_un [in Coq.IntMap.Addec]
ad_of_nat_of_ad [in Coq.IntMap.Adalloc]
ad_pdist_comm [in Coq.IntMap.Adist]
ad_pdist_eq_1 [in Coq.IntMap.Adist]
ad_pdist_eq_2 [in Coq.IntMap.Adist]
ad_pdist_ultra [in Coq.IntMap.Adist]
ad_plength_first_one [in Coq.IntMap.Adist]
ad_plength_infty [in Coq.IntMap.Adist]
ad_plength_lb [in Coq.IntMap.Adist]
ad_plength_one [in Coq.IntMap.Adist]
ad_plength_ub [in Coq.IntMap.Adist]
ad_plength_ultra [in Coq.IntMap.Adist]
ad_plength_ultra_1 [in Coq.IntMap.Adist]
ad_plength_zeros [in Coq.IntMap.Adist]
ad_rec_double [in Coq.IntMap.Lsort]
ad_same_bit_0 [in Coq.IntMap.Addr]
ad_sum [in Coq.IntMap.Addr]
ad_xor_assoc [in Coq.IntMap.Addr]
ad_xor_bit_0 [in Coq.IntMap.Addr]
ad_xor_comm [in Coq.IntMap.Addr]
ad_xor_div_2 [in Coq.IntMap.Addr]
ad_xor_eq [in Coq.IntMap.Addr]
ad_xor_eq_false [in Coq.IntMap.Addec]
ad_xor_eq_true [in Coq.IntMap.Addec]
ad_xor_neutral_left [in Coq.IntMap.Addr]
ad_xor_neutral_right [in Coq.IntMap.Addr]
ad_xor_nilpotent [in Coq.IntMap.Addr]
ad_xor_semantics [in Coq.IntMap.Addr]
ad_xor_sem_1 [in Coq.IntMap.Addr]
ad_xor_sem_2 [in Coq.IntMap.Addr]
ad_xor_sem_3 [in Coq.IntMap.Addr]
ad_xor_sem_4 [in Coq.IntMap.Addr]
ad_xor_sem_5 [in Coq.IntMap.Addr]
ad_xor_sem_6 [in Coq.IntMap.Addr]
ad_z_less_1 [in Coq.IntMap.Lsort]
ad_z_less_2 [in Coq.IntMap.Lsort]
AlembertC3_step1 [in Coq.Reals.Alembert]
AlembertC3_step2 [in Coq.Reals.Alembert]
Alembert_cos [in Coq.Reals.Rtrigo_def]
Alembert_C1 [in Coq.Reals.Alembert]
Alembert_C2 [in Coq.Reals.Alembert]
Alembert_C3 [in Coq.Reals.Alembert]
Alembert_C4 [in Coq.Reals.Alembert]
Alembert_C5 [in Coq.Reals.Alembert]
Alembert_C6 [in Coq.Reals.Alembert]
Alembert_exp [in Coq.Reals.Rtrigo_fun]
Alembert_sin [in Coq.Reals.Rtrigo_def]
alist_canonical [in Coq.IntMap.Lsort]
alist_conc_sorted [in Coq.IntMap.Lsort]
alist_MapMerge_semantics [in Coq.IntMap.Mapiter]
alist_MapMerge_semantics_disjoint [in Coq.IntMap.Mapiter]
alist_nth_ad_aapp_1 [in Coq.IntMap.Lsort]
alist_nth_ad_aapp_2 [in Coq.IntMap.Lsort]
alist_nth_ad_semantics [in Coq.IntMap.Lsort]
alist_of_Map_nth_ad [in Coq.IntMap.Lsort]
alist_of_Map_of_alist [in Coq.IntMap.Mapiter]
alist_of_Map_of_alist_c [in Coq.IntMap.Mapc]
alist_of_Map_semantics [in Coq.IntMap.Mapiter]
alist_of_Map_semantics_1 [in Coq.IntMap.Mapiter]
alist_of_Map_semantics_1_1 [in Coq.IntMap.Mapiter]
alist_of_Map_sorts [in Coq.IntMap.Lsort]
alist_of_Map_sorts1 [in Coq.IntMap.Lsort]
alist_of_Map_sorts2 [in Coq.IntMap.Lsort]
alist_of_Map_sorts_1 [in Coq.IntMap.Lsort]
alist_semantics_app [in Coq.IntMap.Mapiter]
alist_semantics_disjoint_comm [in Coq.IntMap.Mapiter]
alist_semantics_nth_ad [in Coq.IntMap.Lsort]
alist_semantics_same_tail [in Coq.IntMap.Lsort]
alist_semantics_tail [in Coq.IntMap.Lsort]
alist_sorted_imp_1 [in Coq.IntMap.Lsort]
alist_sorted_tail [in Coq.IntMap.Lsort]
alist_sorted_1_imp_2 [in Coq.IntMap.Lsort]
alist_sorted_2_imp [in Coq.IntMap.Lsort]
alist_too_low [in Coq.IntMap.Lsort]
all_not_not_ex [in Coq.Logic.Classical_Pred_Type]
all_not_not_ex [in Coq.Logic.Classical_Pred_Set]
alternated_series [in Coq.Reals.AltSeries]
alternated_series_ineq [in Coq.Reals.AltSeries]
andb_assoc [in Coq.Bool.Bool]
andb_b_false [in Coq.Bool.Bool]
andb_b_true [in Coq.Bool.Bool]
andb_comm [in Coq.Bool.Bool]
andb_false_b [in Coq.Bool.Bool]
andb_false_intro1 [in Coq.Bool.Bool]
andb_false_intro2 [in Coq.Bool.Bool]
andb_neg_b [in Coq.Bool.Bool]
andb_prop [in Coq.Bool.Bool]
andb_prop2 [in Coq.Bool.Bool]
andb_true_b [in Coq.Bool.Bool]
andb_true_intro [in Coq.Bool.Bool]
andb_true_intro2 [in Coq.Bool.Bool]
and_not_or [in Coq.Logic.Classical_Prop]
antiderivative_P1 [in Coq.Reals.NewtonInt]
antiderivative_P2 [in Coq.Reals.NewtonInt]
antiderivative_P3 [in Coq.Reals.NewtonInt]
antiderivative_P4 [in Coq.Reals.NewtonInt]
antiderivative_Ucte [in Coq.Reals.MVT]
approximants_grow [in Coq.Sets.Infinite_sets]
approximants_grow' [in Coq.Sets.Infinite_sets]
approximant_can_be_any_size [in Coq.Sets.Infinite_sets]
approx_maj [in Coq.Reals.SeqProp]
approx_min [in Coq.Reals.SeqProp]
app_ass [in Coq.Lists.List]
app_ass [in Coq.Lists.MonoList]
app_comm_cons [in Coq.Lists.List]
app_cons_not_nil [in Coq.Lists.List]
app_eq_nil [in Coq.Lists.List]
app_eq_unit [in Coq.Lists.List]
app_inj_tail [in Coq.Lists.List]
app_length [in Coq.IntMap.Lsort]
app_nil_end [in Coq.Lists.List]
app_nil_end [in Coq.Lists.MonoList]
archimed_cor1 [in Coq.Reals.Rtrigo_def]
Assoc [in Coq.Lists.TheoryList]
ass_app [in Coq.Lists.MonoList]
ass_app [in Coq.Lists.List]
aux [in Coq.Logic.ClassicalFacts]
A1_cvg [in Coq.Reals.Cos_rel]
This page has been generated by coqdoc