A
AbsList [definition, in AbsList]
AbsList_P1 [lemma, in AbsList_P1]
AbsList_P2 [lemma, in AbsList_P2]
absoption_orb [lemma, in absoption_orb]
absoption_andb [lemma, in absoption_andb]
absurd [lemma, in absurd]
absurd_eq_bool [lemma, in absurd_eq_bool]
absurd_set [lemma, in absurd_set]
absurd_eq_true [lemma, in absurd_eq_true]
abs_IZR [lemma, in abs_IZR]
AC [lemma, in AC]
acc [abbreviation, in acc]
Acc [inductive, in Acc]
acc_A_sum [lemma, in acc_A_sum]
acc_implies_P_eventually [lemma, in acc_implies_P_eventually]
Acc_inv [lemma, in Acc_inv]
Acc_iter_2 [abbreviation, in Acc_iter_2]
Acc_symprod [lemma, in Acc_symprod]
Acc_intro [constructor, in Acc_intro]
Acc_pt_morphism [instance, in Acc_pt_morphism]
Acc_incl [lemma, in Acc_incl]
Acc_lemma [lemma, in Acc_lemma]
Acc_inverse_rel [lemma, in Acc_inverse_rel]
Acc_iter [abbreviation, in Acc_iter]
Acc_inverse_image [lemma, in Acc_inverse_image]
Acc_inv_dep [definition, in Acc_inv_dep]
acc_app [lemma, in acc_app]
acc_B_sum [lemma, in acc_B_sum]
Acc_clos_trans [lemma, in Acc_clos_trans]
acc_lt_rel [lemma, in acc_lt_rel]
Acc_union [lemma, in Acc_union]
acc_A_B_lexprod [lemma, in acc_A_B_lexprod]
Acc_swapprod [lemma, in Acc_swapprod]
Acc_inv_trans [lemma, in Acc_inv_trans]
Acc_rel_morphism [instance, in Acc_rel_morphism]
AC_bool_subset_to_bool [lemma, in AC_bool_subset_to_bool]
AC_IF [lemma, in AC_IF]
adapted_couple [definition, in adapted_couple]
adapted_couple_opt [definition, in adapted_couple_opt]
add [definition, in add]
Add [definition, in Add]
addmuldiv31 [definition, in addmuldiv31]
addmuldiv31_equiv [lemma, in addmuldiv31_equiv]
addmuldiv31_alt [definition, in addmuldiv31_alt]
adds [definition, in adds]
AddS [section, in AddS]
AddSubMul [module, in AddSubMul]
AddSubMulNotation [module, in AddSubMulNotation]
_ - _ [notation, in ::x_'-'_x]
_ * _ [notation, in ::x_'*'_x]
_ + _ [notation, in ::x_'+'_x]
AddSubMul' [module, in AddSubMul']
AddSubMul.add [axiom, in add]
AddSubMul.mul [axiom, in mul]
AddSubMul.sub [axiom, in sub]
AddS.addr [variable, in addr]
AddS.incr [variable, in incr]
AddS.injr [variable, in injr]
AddS.u [variable, in u]
AddS.w [variable, in w]
AddS.wm [variable, in wm]
AddS.w_0 [variable, in w_0]
add_soustr_xy [lemma, in add_soustr_xy]
Add_inv [lemma, in Add_inv]
add_soustr_1 [lemma, in add_soustr_1]
Add_commutative [lemma, in Add_commutative]
add_c [definition, in add_c]
Add_distributes [lemma, in Add_distributes]
add_carry_c [definition, in add_carry_c]
add_mult_mult_2 [lemma, in add_mult_mult_2]
Add_preserves_Finite [lemma, in Add_preserves_Finite]
Add_intro1 [lemma, in Add_intro1]
add_carry [definition, in add_carry]
Add_intro2 [lemma, in Add_intro2]
Add_commutative' [lemma, in Add_commutative']
add_mul_div [definition, in add_mul_div]
Add_not_Empty [lemma, in Add_not_Empty]
add_mult_div_2_plus_1 [lemma, in add_mult_div_2_plus_1]
add_soustr_2 [lemma, in add_soustr_2]
add_mult_div_2 [lemma, in add_mult_div_2]
Add_covers [lemma, in Add_covers]
add31 [definition, in add31]
add31c [definition, in add31c]
add31carryc [definition, in add31carryc]
adhDa [definition, in adhDa]
adherence [definition, in adherence]
adherence_P4 [lemma, in adherence_P4]
adherence_P3 [lemma, in adherence_P3]
adherence_P2 [lemma, in adherence_P2]
adherence_P1 [lemma, in adherence_P1]
Alembert [library]
AlembertC3_step2 [lemma, in AlembertC3_step2]
AlembertC3_step1 [lemma, in AlembertC3_step1]
Alembert_C6 [lemma, in Alembert_C6]
Alembert_C3 [lemma, in Alembert_C3]
Alembert_C4 [lemma, in Alembert_C4]
Alembert_C2 [lemma, in Alembert_C2]
Alembert_C5 [lemma, in Alembert_C5]
Alembert_sin [lemma, in Alembert_sin]
Alembert_cos [lemma, in Alembert_cos]
Alembert_C1 [lemma, in Alembert_C1]
Alembert_exp [lemma, in Alembert_exp]
all [definition, in all]
AllS [abbreviation, in AllS]
all_inverse_impl_morphism [instance, in all_inverse_impl_morphism]
all_not_not_ex [lemma, in all_not_not_ex]
all_not_not_ex [lemma, in all_not_not_ex]
all_iff_morphism [instance, in all_iff_morphism]
all_impl_morphism [instance, in all_impl_morphism]
alternated_series_ineq [lemma, in alternated_series_ineq]
alternated_series [lemma, in alternated_series]
AltSeries [library]
Alt_PI_ineq [lemma, in Alt_PI_ineq]
Alt_PI_tg [lemma, in Alt_PI_tg]
Alt_PI_RGT_0 [lemma, in Alt_PI_RGT_0]
Alt_first_term_bound [lemma, in Alt_first_term_bound]
Alt_PI [definition, in Alt_PI]
Alt_PI_eq [lemma, in Alt_PI_eq]
Alt_CVU [lemma, in Alt_CVU]
and [inductive, in and]
andb [definition, in andb]
andb_true_intro [lemma, in andb_true_intro]
andb_false_intro2 [lemma, in andb_false_intro2]
andb_if [lemma, in andb_if]
andb_orb_distrib_r [lemma, in andb_orb_distrib_r]
andb_false_b [abbreviation, in andb_false_b]
andb_false_intro1 [lemma, in andb_false_intro1]
andb_b_false [abbreviation, in andb_b_false]
andb_assoc [lemma, in andb_assoc]
andb_negb_r [lemma, in andb_negb_r]
andb_false_iff [lemma, in andb_false_iff]
andb_prop2 [abbreviation, in andb_prop2]
andb_false_elim [lemma, in andb_false_elim]
andb_orb_distrib_l [lemma, in andb_orb_distrib_l]
andb_prop_intro [lemma, in andb_prop_intro]
andb_diag [lemma, in andb_diag]
andb_true_intro2 [abbreviation, in andb_true_intro2]
andb_true_l [lemma, in andb_true_l]
andb_prop [lemma, in andb_prop]
andb_neg_b [abbreviation, in andb_neg_b]
andb_prop_elim [lemma, in andb_prop_elim]
andb_true_r [lemma, in andb_true_r]
andb_true_b [abbreviation, in andb_true_b]
andb_false_r [lemma, in andb_false_r]
andb_true_eq [lemma, in andb_true_eq]
andb_false_l [lemma, in andb_false_l]
andb_comm [lemma, in andb_comm]
andb_b_true [abbreviation, in andb_b_true]
andb_lazy_alt [lemma, in andb_lazy_alt]
andb_true_iff [lemma, in andb_true_iff]
and_iff_compat_l [lemma, in and_iff_compat_l]
and_impl_morphism [instance, in and_impl_morphism]
and_comm [lemma, in and_comm]
and_iff_compat_r [lemma, in and_iff_compat_r]
and_cancel_r [lemma, in and_cancel_r]
and_cancel_l [lemma, in and_cancel_l]
and_iff_morphism [instance, in and_iff_morphism]
and_indd [definition, in and_indd]
and_not_or [lemma, in and_not_or]
and_assoc [lemma, in and_assoc]
antiderivative [definition, in antiderivative]
antiderivative_P3 [lemma, in antiderivative_P3]
antiderivative_Ucte [lemma, in antiderivative_Ucte]
antiderivative_P4 [lemma, in antiderivative_P4]
antiderivative_P1 [lemma, in antiderivative_P1]
antiderivative_P2 [lemma, in antiderivative_P2]
Antisymmetric [record, in Antisymmetric]
Antisymmetric [inductive, in Antisymmetric]
Antisymmetric [definition, in Antisymmetric]
antisymmetric [definition, in antisymmetric]
antisymmetry [projection, in antisymmetry]
antisymmetry [constructor, in antisymmetry]
app [abbreviation, in app]
app [definition, in app]
append [definition, in append]
append [definition, in append]
append [definition, in append]
append_assoc_0 [lemma, in append_assoc_0]
append_neutral_l [lemma, in append_neutral_l]
append_correct1 [lemma, in append_correct1]
append_neutral_r [lemma, in append_neutral_r]
append_assoc_1 [lemma, in append_assoc_1]
append_correct2 [lemma, in append_correct2]
apply [definition, in apply]
apply_subrelation [inductive, in apply_subrelation]
Approx [section, in Approx]
Approximant [inductive, in Approximant]
approximants_grow' [lemma, in approximants_grow']
approximants_grow [lemma, in approximants_grow]
approximant_can_be_any_size [lemma, in approximant_can_be_any_size]
approx_maj [lemma, in approx_maj]
approx_min [lemma, in approx_min]
Approx.U [variable, in U]
AppVar [axiom, in AppVar]
app_Rlist [definition, in app_Rlist]
app_inv_head [lemma, in app_inv_head]
app_comm_cons [lemma, in app_comm_cons]
app_cons_not_nil [lemma, in app_cons_not_nil]
app_nth2 [lemma, in app_nth2]
app_nil_end [lemma, in app_nil_end]
app_length [lemma, in app_length]
app_nil_l [lemma, in app_nil_l]
app_inv_tail [lemma, in app_inv_tail]
app_ass [abbreviation, in app_ass]
app_eq_nil [lemma, in app_eq_nil]
app_eq_unit [lemma, in app_eq_unit]
app_inj_tail [lemma, in app_inj_tail]
app_removelast_last [lemma, in app_removelast_last]
app_eqlistA_compat [instance, in app_eqlistA_compat]
app_assoc_reverse [lemma, in app_assoc_reverse]
app_assoc [lemma, in app_assoc]
app_nth1 [lemma, in app_nth1]
app_nil_r [lemma, in app_nil_r]
archimed [axiom, in archimed]
archimed_cor1 [lemma, in archimed_cor1]
Arith [library]
Arithmetical_dec.P [variable, in P]
Arithmetical_dec.HP [variable, in HP]
Arithmetical_dec.f [variable, in f]
Arithmetical_dec.ge_fun_sums_ge [variable, in ge_fun_sums_ge]
Arithmetical_dec [section, in Arithmetical_dec]
Arithmetical_dec.ge_fun_sums_ge_lemma [variable, in ge_fun_sums_ge_lemma]
ArithProp [library]
Arith_base [library]
arrow [definition, in arrow]
arrows [definition, in arrows]
Ascii [constructor, in Ascii]
ascii [inductive, in ascii]
Ascii [library]
ascii_of_pos [definition, in ascii_of_pos]
ascii_of_N [definition, in ascii_of_N]
ascii_nat_embedding [lemma, in ascii_nat_embedding]
ascii_N_embedding [lemma, in ascii_N_embedding]
ascii_dec [definition, in ascii_dec]
ascii_of_nat [definition, in ascii_of_nat]
ass_app [abbreviation, in ass_app]
Asymmetric [record, in Asymmetric]
Asymmetric [inductive, in Asymmetric]
asymmetry [projection, in asymmetry]
asymmetry [constructor, in asymmetry]
atan [definition, in atan]
atan_eq_ps_atan [lemma, in atan_eq_ps_atan]
atan_right_inv [lemma, in atan_right_inv]
atan_sub [definition, in atan_sub]
atan_opp [lemma, in atan_opp]
atan_1 [lemma, in atan_1]
atan_sub_correct [lemma, in atan_sub_correct]
atan_bound [lemma, in atan_bound]
atan_increasing [lemma, in atan_increasing]
atan_0 [lemma, in atan_0]
aux [lemma, in aux]
auxiliary [library]
AvlProofs [module, in AvlProofs]
AvlProofs.add_avl [lemma, in add_avl]
AvlProofs.add_avl_1 [lemma, in add_avl_1]
AvlProofs.avl [inductive, in avl]
AvlProofs.avl_node [lemma, in avl_node]
AvlProofs.bal_avl [lemma, in bal_avl]
AvlProofs.bal_height_2 [lemma, in bal_height_2]
AvlProofs.bal_height_1 [lemma, in bal_height_1]
AvlProofs.concat_avl [lemma, in concat_avl]
AvlProofs.create_avl [lemma, in create_avl]
AvlProofs.create_height [lemma, in create_height]
AvlProofs.Elt [section, in Elt]
AvlProofs.Elt.elt [variable, in elt]
AvlProofs.empty_avl [lemma, in empty_avl]
AvlProofs.height_0 [lemma, in height_0]
AvlProofs.height_non_negative [lemma, in height_non_negative]
AvlProofs.II [module, in AvlProofs.II]
AvlProofs.join_avl [lemma, in join_avl]
AvlProofs.join_avl_1 [lemma, in join_avl_1]
AvlProofs.Map [section, in Map]
AvlProofs.Mapi [section, in Mapi]
AvlProofs.mapi_avl [lemma, in mapi_avl]
AvlProofs.mapi_height [lemma, in mapi_height]
AvlProofs.Mapi.elt [variable, in elt]
AvlProofs.Mapi.elt' [variable, in elt']
AvlProofs.Mapi.f [variable, in f]
AvlProofs.Map_option.elt' [variable, in elt']
AvlProofs.Map_option.f [variable, in f]
AvlProofs.Map_option.elt [variable, in elt]
AvlProofs.map_height [lemma, in map_height]
AvlProofs.Map_option [section, in Map_option]
AvlProofs.map_option_avl [lemma, in map_option_avl]
AvlProofs.map_avl [lemma, in map_avl]
AvlProofs.Map.elt [variable, in elt]
AvlProofs.Map.elt' [variable, in elt']
AvlProofs.Map.f [variable, in f]
AvlProofs.Map2 [section, in Map2]
AvlProofs.Map2_opt.mapr_avl [variable, in mapr_avl]
AvlProofs.map2_avl [lemma, in map2_avl]
AvlProofs.Map2_opt [section, in Map2_opt]
AvlProofs.map2_opt [abbreviation, in map2_opt]
AvlProofs.Map2_opt.elt' [variable, in elt']
AvlProofs.Map2_opt.f [variable, in f]
AvlProofs.Map2_opt.elt [variable, in elt]
AvlProofs.Map2_opt.mapl [variable, in mapl]
AvlProofs.Map2_opt.mapl_avl [variable, in mapl_avl]
AvlProofs.map2_opt_avl [lemma, in map2_opt_avl]
AvlProofs.Map2_opt.elt'' [variable, in elt'']
AvlProofs.Map2_opt.mapr [variable, in mapr]
AvlProofs.Map2.elt [variable, in elt]
AvlProofs.Map2.elt' [variable, in elt']
AvlProofs.Map2.elt'' [variable, in elt'']
AvlProofs.Map2.f [variable, in f]
AvlProofs.merge_avl_1 [lemma, in merge_avl_1]
AvlProofs.merge_avl [lemma, in merge_avl]
AvlProofs.Raw [module, in AvlProofs.Raw]
AvlProofs.RBLeaf [constructor, in RBLeaf]
AvlProofs.RBNode [constructor, in RBNode]
AvlProofs.remove_min_avl_1 [lemma, in remove_min_avl_1]
AvlProofs.remove_min_avl [lemma, in remove_min_avl]
AvlProofs.remove_avl [lemma, in remove_avl]
AvlProofs.remove_avl_1 [lemma, in remove_avl_1]
AvlProofs.split_avl [lemma, in split_avl]
Axiomatisation [section, in Axiomatisation]
Axiomatisation.cong [variable, in cong]
Axiomatisation.cong_left [variable, in cong_left]
Axiomatisation.cong_sym [variable, in cong_sym]
Axiomatisation.cong_right [variable, in cong_right]
Axiomatisation.cong_trans [variable, in cong_trans]
Axiomatisation.op [variable, in op]
Axiomatisation.op_comm [variable, in op_comm]
Axiomatisation.op_ass [variable, in op_ass]
Axiomatisation.U [variable, in U]
A' [definition, in A']
A1 [definition, in A1]
A1_cvg [lemma, in A1_cvg]
a1' [definition, in a1']
a2' [definition, in a2']