M
Machin [library]
Machin_2_3 [lemma, in Machin_2_3]
Machin_2_3_7 [lemma, in Machin_2_3_7]
Machin_4_5_239 [lemma, in Machin_4_5_239]
majorant [abbreviation, in majorant]
Majxy [definition, in Majxy]
Majxy_cv_R0 [lemma, in Majxy_cv_R0]
maj_term4 [lemma, in maj_term4]
maj_Reste_cv_R0 [lemma, in maj_Reste_cv_R0]
maj_cv [lemma, in maj_cv]
maj_Reste_E [definition, in maj_Reste_E]
maj_ss [lemma, in maj_ss]
maj_term1 [lemma, in maj_term1]
maj_by_pos [lemma, in maj_by_pos]
maj_min [lemma, in maj_min]
maj_term3 [lemma, in maj_term3]
maj_sup [abbreviation, in maj_sup]
maj_term2 [lemma, in maj_term2]
Make [module, in Make]
Make [module, in Make]
Make [module, in Make]
Make [module, in Make]
Make [module, in Make]
Make [module, in Make]
Make [module, in Make]
Make [module, in Make]
Make [module, in Make]
Make [module, in Make]
Make [module, in Make]
Make [module, in Make]
Make [module, in Make]
MakeListOrdering [module, in MakeListOrdering]
MakeListOrdering.cons_CompSpec [lemma, in cons_CompSpec]
MakeListOrdering.eq [definition, in eq]
MakeListOrdering.eq_cons [lemma, in eq_cons]
MakeListOrdering.eq_equiv [instance, in eq_equiv]
MakeListOrdering.In [abbreviation, in In]
MakeListOrdering.lt [definition, in lt]
MakeListOrdering.lt_nil [constructor, in lt_nil]
MakeListOrdering.lt_cons_lt [constructor, in lt_cons_lt]
MakeListOrdering.lt_strorder [instance, in lt_strorder]
MakeListOrdering.lt_cons_eq [constructor, in lt_cons_eq]
MakeListOrdering.lt_compat' [instance, in lt_compat']
MakeListOrdering.lt_list [inductive, in lt_list]
MakeListOrdering.MO [module, in MakeListOrdering.MO]
MakeListOrdering.t [abbreviation, in t]
MakeOrderTac [module, in MakeOrderTac]
MakeRaw [module, in MakeRaw]
MakeRaw [module, in MakeRaw]
MakeRaw [module, in MakeRaw]
MakeRaw [module, in MakeRaw]
MakeRaw.acc_sorted [projection, in acc_sorted]
MakeRaw.add_ok [instance, in add_ok]
MakeRaw.add_ok [instance, in add_ok]
MakeRaw.add_ok [instance, in add_ok]
MakeRaw.add_spec' [lemma, in add_spec']
MakeRaw.add_spec [lemma, in add_spec]
MakeRaw.add_spec [lemma, in add_spec]
MakeRaw.add_spec [lemma, in add_spec]
MakeRaw.add_inf [lemma, in add_inf]
MakeRaw.append_ok [lemma, in append_ok]
MakeRaw.append_bb_match [lemma, in append_bb_match]
MakeRaw.append_spec [lemma, in append_spec]
MakeRaw.append_rr_match [lemma, in append_rr_match]
MakeRaw.Bk [abbreviation, in Bk]
MakeRaw.cardinal_spec [lemma, in cardinal_spec]
MakeRaw.cardinal_spec [lemma, in cardinal_spec]
MakeRaw.choose_spec3 [lemma, in choose_spec3]
MakeRaw.choose_spec2 [definition, in choose_spec2]
MakeRaw.choose_spec2 [definition, in choose_spec2]
MakeRaw.choose_spec1 [definition, in choose_spec1]
MakeRaw.choose_spec1 [definition, in choose_spec1]
MakeRaw.compare_spec [lemma, in compare_spec]
MakeRaw.compare_spec_aux [lemma, in compare_spec_aux]
MakeRaw.delmin_spec [lemma, in delmin_spec]
MakeRaw.del_spec [lemma, in del_spec]
MakeRaw.del_ok [instance, in del_ok]
MakeRaw.diff_inter_ok [instance, in diff_inter_ok]
MakeRaw.diff_spec [lemma, in diff_spec]
MakeRaw.diff_spec [lemma, in diff_spec]
MakeRaw.diff_spec [lemma, in diff_spec]
MakeRaw.diff_ok [instance, in diff_ok]
MakeRaw.diff_ok [instance, in diff_ok]
MakeRaw.diff_ok [instance, in diff_ok]
MakeRaw.diff_inf [lemma, in diff_inf]
MakeRaw.diff_list_spec [lemma, in diff_list_spec]
MakeRaw.diff_list_ok [lemma, in diff_list_ok]
MakeRaw.elements_spec2w [lemma, in elements_spec2w]
MakeRaw.elements_spec2w [lemma, in elements_spec2w]
MakeRaw.elements_spec2 [lemma, in elements_spec2]
MakeRaw.elements_spec1 [lemma, in elements_spec1]
MakeRaw.elements_spec1 [lemma, in elements_spec1]
MakeRaw.Empty [definition, in Empty]
MakeRaw.Empty [definition, in Empty]
MakeRaw.empty_spec [lemma, in empty_spec]
MakeRaw.empty_spec [lemma, in empty_spec]
MakeRaw.empty_ok [lemma, in empty_ok]
MakeRaw.empty_ok [instance, in empty_ok]
MakeRaw.eq [definition, in eq]
MakeRaw.eq [definition, in eq]
MakeRaw.Equal [definition, in Equal]
MakeRaw.Equal [definition, in Equal]
MakeRaw.equal_spec [lemma, in equal_spec]
MakeRaw.equal_spec [lemma, in equal_spec]
MakeRaw.eq_equiv [instance, in eq_equiv]
MakeRaw.eq_equiv [definition, in eq_equiv]
MakeRaw.Exists [definition, in Exists]
MakeRaw.Exists [definition, in Exists]
MakeRaw.exists_spec [lemma, in exists_spec]
MakeRaw.exists_spec [lemma, in exists_spec]
MakeRaw.filter_aux_elements [lemma, in filter_aux_elements]
MakeRaw.filter_spec [lemma, in filter_spec]
MakeRaw.filter_spec [lemma, in filter_spec]
MakeRaw.filter_spec [lemma, in filter_spec]
MakeRaw.filter_inf [lemma, in filter_inf]
MakeRaw.filter_app [lemma, in filter_app]
MakeRaw.filter_spec' [lemma, in filter_spec']
MakeRaw.filter_ok [instance, in filter_ok]
MakeRaw.filter_ok [instance, in filter_ok]
MakeRaw.filter_ok [instance, in filter_ok]
MakeRaw.filter_elements [lemma, in filter_elements]
MakeRaw.fold_add_spec [lemma, in fold_add_spec]
MakeRaw.fold_remove_spec [lemma, in fold_remove_spec]
MakeRaw.fold_add_ok [instance, in fold_add_ok]
MakeRaw.fold_remove_ok [instance, in fold_remove_ok]
MakeRaw.fold_spec [lemma, in fold_spec]
MakeRaw.fold_spec [lemma, in fold_spec]
MakeRaw.ForNotations [section, in ForNotations]
MakeRaw.ForNotations [section, in ForNotations]
MakeRaw.For_all [definition, in For_all]
MakeRaw.For_all [definition, in For_all]
MakeRaw.for_all_spec [lemma, in for_all_spec]
MakeRaw.for_all_spec [lemma, in for_all_spec]
MakeRaw.ifpred [abbreviation, in ifpred]
MakeRaw.In [definition, in In]
MakeRaw.In [abbreviation, in In]
MakeRaw.In [definition, in In]
MakeRaw.In [abbreviation, in In]
MakeRaw.Inf [abbreviation, in Inf]
MakeRaw.inf [definition, in inf]
MakeRaw.inf_iff [lemma, in inf_iff]
MakeRaw.ins_ok [instance, in ins_ok]
MakeRaw.ins_spec [lemma, in ins_spec]
MakeRaw.inter_inf [lemma, in inter_inf]
MakeRaw.inter_spec [lemma, in inter_spec]
MakeRaw.inter_spec [lemma, in inter_spec]
MakeRaw.inter_spec [lemma, in inter_spec]
MakeRaw.inter_ok [instance, in inter_ok]
MakeRaw.inter_ok [instance, in inter_ok]
MakeRaw.inter_ok [instance, in inter_ok]
MakeRaw.inter_list_ok [lemma, in inter_list_ok]
MakeRaw.inter_list_spec [lemma, in inter_list_spec]
MakeRaw.INV [record, in INV]
MakeRaw.INV_lt [lemma, in INV_lt]
MakeRaw.INV_eq [lemma, in INV_eq]
MakeRaw.INV_rev [lemma, in INV_rev]
MakeRaw.INV_drop [lemma, in INV_drop]
MakeRaw.INV_sym [lemma, in INV_sym]
MakeRaw.INV_init [lemma, in INV_init]
MakeRaw.In_compat [lemma, in In_compat]
MakeRaw.In_compat [instance, in In_compat]
MakeRaw.isblack [definition, in isblack]
MakeRaw.IsOk [definition, in IsOk]
MakeRaw.IsOk [definition, in IsOk]
MakeRaw.isok [definition, in isok]
MakeRaw.isok [definition, in isok]
MakeRaw.isok_Ok [instance, in isok_Ok]
MakeRaw.isok_Ok [instance, in isok_Ok]
MakeRaw.isok_iff [lemma, in isok_iff]
MakeRaw.isok_iff [lemma, in isok_iff]
MakeRaw.is_empty_spec [lemma, in is_empty_spec]
MakeRaw.is_empty_spec [lemma, in is_empty_spec]
MakeRaw.L [module, in MakeRaw.L]
MakeRaw.lbalS_spec [lemma, in lbalS_spec]
MakeRaw.lbalS_match [lemma, in lbalS_match]
MakeRaw.lbalS_ok [instance, in lbalS_ok]
MakeRaw.lbal_match [lemma, in lbal_match]
MakeRaw.lbal_spec [lemma, in lbal_spec]
MakeRaw.lbal_ok [instance, in lbal_ok]
MakeRaw.linear_diff_spec [lemma, in linear_diff_spec]
MakeRaw.linear_inter_ok [instance, in linear_inter_ok]
MakeRaw.linear_union_ok [instance, in linear_union_ok]
MakeRaw.linear_inter_spec [lemma, in linear_inter_spec]
MakeRaw.linear_union_spec [lemma, in linear_union_spec]
MakeRaw.lt [definition, in lt]
MakeRaw.lt_compat [instance, in lt_compat]
MakeRaw.lt_strorder [instance, in lt_strorder]
MakeRaw.l1_lt_acc [projection, in l1_lt_acc]
MakeRaw.l1_sorted [projection, in l1_sorted]
MakeRaw.l2_lt_acc [projection, in l2_lt_acc]
MakeRaw.l2_sorted [projection, in l2_sorted]
MakeRaw.makeBlack_ok [instance, in makeBlack_ok]
MakeRaw.makeBlack_spec [lemma, in makeBlack_spec]
MakeRaw.makeRed_spec [lemma, in makeRed_spec]
MakeRaw.makeRed_ok [instance, in makeRed_ok]
MakeRaw.max_elt_spec3 [lemma, in max_elt_spec3]
MakeRaw.max_elt_spec2 [lemma, in max_elt_spec2]
MakeRaw.max_elt_spec1 [lemma, in max_elt_spec1]
MakeRaw.mem_proper [instance, in mem_proper]
MakeRaw.mem_spec [lemma, in mem_spec]
MakeRaw.mem_spec [lemma, in mem_spec]
MakeRaw.min_elt_spec2 [lemma, in min_elt_spec2]
MakeRaw.min_elt_spec3 [lemma, in min_elt_spec3]
MakeRaw.min_elt_spec1 [lemma, in min_elt_spec1]
MakeRaw.ML [module, in MakeRaw.ML]
MakeRaw.MX [module, in MakeRaw.MX]
MakeRaw.NoDup [abbreviation, in NoDup]
MakeRaw.NoDup_Ok [instance, in NoDup_Ok]
MakeRaw.notblack [definition, in notblack]
MakeRaw.notred [definition, in notred]
MakeRaw.notredred [abbreviation, in notredred]
MakeRaw.Ok [record, in Ok]
MakeRaw.Ok [inductive, in Ok]
MakeRaw.Ok [record, in Ok]
MakeRaw.Ok [inductive, in Ok]
MakeRaw.ok [projection, in ok]
MakeRaw.ok [constructor, in ok]
MakeRaw.ok [projection, in ok]
MakeRaw.ok [constructor, in ok]
MakeRaw.partition_spec2 [lemma, in partition_spec2]
MakeRaw.partition_spec2 [lemma, in partition_spec2]
MakeRaw.partition_spec2 [lemma, in partition_spec2]
MakeRaw.partition_spec1 [lemma, in partition_spec1]
MakeRaw.partition_spec1 [lemma, in partition_spec1]
MakeRaw.partition_spec1 [lemma, in partition_spec1]
MakeRaw.partition_ok2' [lemma, in partition_ok2']
MakeRaw.partition_ok1' [lemma, in partition_ok1']
MakeRaw.partition_ok2 [instance, in partition_ok2]
MakeRaw.partition_ok2 [instance, in partition_ok2]
MakeRaw.partition_ok2 [instance, in partition_ok2]
MakeRaw.partition_aux_spec [lemma, in partition_aux_spec]
MakeRaw.partition_spec [lemma, in partition_spec]
MakeRaw.partition_inf1 [lemma, in partition_inf1]
MakeRaw.partition_ok1 [instance, in partition_ok1]
MakeRaw.partition_ok1 [instance, in partition_ok1]
MakeRaw.partition_ok1 [instance, in partition_ok1]
MakeRaw.partition_inf2 [lemma, in partition_inf2]
MakeRaw.plength_aux_spec [lemma, in plength_aux_spec]
MakeRaw.plength_spec [lemma, in plength_spec]
MakeRaw.rbalS_match [lemma, in rbalS_match]
MakeRaw.rbalS_spec [lemma, in rbalS_spec]
MakeRaw.rbalS_ok [instance, in rbalS_ok]
MakeRaw.rbal_spec [lemma, in rbal_spec]
MakeRaw.rbal_match [lemma, in rbal_match]
MakeRaw.rbal_ok [instance, in rbal_ok]
MakeRaw.rbal'_spec [lemma, in rbal'_spec]
MakeRaw.rbal'_match [lemma, in rbal'_match]
MakeRaw.rbal'_ok [instance, in rbal'_ok]
MakeRaw.rcase [definition, in rcase]
MakeRaw.Rd [abbreviation, in Rd]
MakeRaw.relse [constructor, in relse]
MakeRaw.remove_min_spec1 [lemma, in remove_min_spec1]
MakeRaw.remove_spec [lemma, in remove_spec]
MakeRaw.remove_spec [lemma, in remove_spec]
MakeRaw.remove_spec [lemma, in remove_spec]
MakeRaw.remove_inf [lemma, in remove_inf]
MakeRaw.remove_min_ok [lemma, in remove_min_ok]
MakeRaw.remove_min_spec2 [lemma, in remove_min_spec2]
MakeRaw.remove_ok [instance, in remove_ok]
MakeRaw.remove_ok [instance, in remove_ok]
MakeRaw.remove_ok [instance, in remove_ok]
MakeRaw.rmatch [lemma, in rmatch]
MakeRaw.rrcase [definition, in rrcase]
MakeRaw.rrcase' [definition, in rrcase']
MakeRaw.rred [constructor, in rred]
MakeRaw.rrelse [constructor, in rrelse]
MakeRaw.rrleft [constructor, in rrleft]
MakeRaw.rrmatch [lemma, in rrmatch]
MakeRaw.rrmatch' [lemma, in rrmatch']
MakeRaw.rrright [constructor, in rrright]
MakeRaw.rrspec [inductive, in rrspec]
MakeRaw.rspec [inductive, in rspec]
MakeRaw.singleton_spec [lemma, in singleton_spec]
MakeRaw.singleton_spec [lemma, in singleton_spec]
MakeRaw.singleton_spec [lemma, in singleton_spec]
MakeRaw.singleton_ok [lemma, in singleton_ok]
MakeRaw.singleton_ok [instance, in singleton_ok]
MakeRaw.singleton_ok [instance, in singleton_ok]
MakeRaw.Sort [abbreviation, in Sort]
MakeRaw.Sort_Ok [instance, in Sort_Ok]
MakeRaw.Subset [definition, in Subset]
MakeRaw.Subset [definition, in Subset]
MakeRaw.subset_spec [lemma, in subset_spec]
MakeRaw.subset_spec [lemma, in subset_spec]
MakeRaw.treeify_invariant [definition, in treeify_invariant]
MakeRaw.treeify_one_spec [lemma, in treeify_one_spec]
MakeRaw.treeify_elements [lemma, in treeify_elements]
MakeRaw.treeify_ok [lemma, in treeify_ok]
MakeRaw.treeify_cont_spec [lemma, in treeify_cont_spec]
MakeRaw.treeify_aux_spec [lemma, in treeify_aux_spec]
MakeRaw.treeify_zero_spec [lemma, in treeify_zero_spec]
MakeRaw.treeify_spec [lemma, in treeify_spec]
MakeRaw.union_list_ok [lemma, in union_list_ok]
MakeRaw.union_spec [lemma, in union_spec]
MakeRaw.union_spec [lemma, in union_spec]
MakeRaw.union_spec [lemma, in union_spec]
MakeRaw.union_spec' [lemma, in union_spec']
MakeRaw.union_inf [lemma, in union_inf]
MakeRaw.union_list_spec [lemma, in union_list_spec]
MakeRaw.union_ok [instance, in union_ok]
MakeRaw.union_ok [instance, in union_ok]
MakeRaw.union_ok [instance, in union_ok]
MakeSetOrdering [module, in MakeSetOrdering]
MakeSetOrdering.Above [definition, in Above]
MakeSetOrdering.Add [definition, in Add]
MakeSetOrdering.Below [definition, in Below]
MakeSetOrdering.EmptyBetween [definition, in EmptyBetween]
MakeSetOrdering.eq [definition, in eq]
MakeSetOrdering.EquivBefore [definition, in EquivBefore]
MakeSetOrdering.eq_equiv [instance, in eq_equiv]
MakeSetOrdering.lt [definition, in lt]
MakeSetOrdering.lt_empty_r [lemma, in lt_empty_r]
MakeSetOrdering.lt_compat [instance, in lt_compat]
MakeSetOrdering.lt_strorder [instance, in lt_strorder]
MakeSetOrdering.lt_empty_l [lemma, in lt_empty_l]
MakeSetOrdering.lt_add_lt [lemma, in lt_add_lt]
MakeSetOrdering.lt_add_eq [lemma, in lt_add_eq]
MakeSetOrdering.MO [module, in MakeSetOrdering.MO]
MakeWithLeibniz [module, in MakeWithLeibniz]
MakeWithLeibniz.E [module, in MakeWithLeibniz.E]
MakeWithLeibniz.eq_leibniz [lemma, in eq_leibniz]
MakeWithLeibniz.eq_leibniz_list [lemma, in eq_leibniz_list]
MakeWithLeibniz.Raw [module, in MakeWithLeibniz.Raw]
Make_ord.eq_refl [lemma, in eq_refl]
Make_ord.eq_1 [lemma, in eq_1]
make_kzop [lemma, in make_kzop]
Make_ord.Data [module, in Make_ord.Data]
make_zop [lemma, in make_zop]
Make_ord.eq_equal [lemma, in eq_equal]
Make_ord.t [definition, in t]
make_new_approximant [lemma, in make_new_approximant]
Make_ord.compare [definition, in compare]
Make_ord.eq_2 [lemma, in eq_2]
Make_ord.cmp [definition, in cmp]
Make_UDT [module, in Make_UDT]
Make_UDT [module, in Make_UDT]
Make_UDTF [module, in Make_UDTF]
Make_ord.eq_sym [lemma, in eq_sym]
Make_ord.MapS [module, in Make_ord.MapS]
Make_ord.lt_not_eq [lemma, in lt_not_eq]
Make_ord.lt_trans [lemma, in lt_trans]
Make_ord.eq_trans [lemma, in eq_trans]
Make_ord [module, in Make_ord]
Make_ord [module, in Make_ord]
Make_ord.eq_list [definition, in eq_list]
Make_ord.MD [module, in Make_ord.MD]
Make_ord.lt_list [definition, in lt_list]
Make_ord.lt [definition, in lt]
Make_ord.eq [definition, in eq]
Make.abs [definition, in abs]
Make.add [definition, in add]
Make.add [definition, in add]
Make.add [definition, in add]
Make.add [definition, in add]
Make.add [definition, in add]
Make.addn [abbreviation, in addn]
Make.add_1 [lemma, in add_1]
Make.add_1 [lemma, in add_1]
Make.add_2 [lemma, in add_2]
Make.add_2 [lemma, in add_2]
Make.add_norm [definition, in add_norm]
Make.add_3 [lemma, in add_3]
Make.add_3 [lemma, in add_3]
Make.add_fold [lemma, in add_fold]
Make.cardinal [definition, in cardinal]
Make.cardinal [definition, in cardinal]
Make.cardinal_1 [lemma, in cardinal_1]
Make.cardinal_1 [lemma, in cardinal_1]
Make.check_int [definition, in check_int]
Make.compare [definition, in compare]
Make.compare [definition, in compare]
Make.compare [definition, in compare]
Make.comparenm [definition, in comparenm]
Make.comparen_m [definition, in comparen_m]
Make.compare_folded [abbreviation, in compare_folded]
Make.compare_fold [lemma, in compare_fold]
Make.destr_t [lemma, in destr_t]
Make.digits [definition, in digits]
Make.digitsn [abbreviation, in digitsn]
Make.digits_dom_op_incr [lemma, in digits_dom_op_incr]
Make.digits_level [lemma, in digits_level]
Make.digits_dom_op [lemma, in digits_dom_op]
Make.digits_nmake [lemma, in digits_nmake]
Make.digits_make_op_0 [lemma, in digits_make_op_0]
Make.digits_fold [lemma, in digits_fold]
Make.digits_dom_op_nmake [lemma, in digits_dom_op_nmake]
Make.digits_make_op [lemma, in digits_make_op]
Make.digits_nmake_S [lemma, in digits_nmake_S]
Make.div [definition, in div]
Make.div [definition, in div]
Make.div [definition, in div]
Make.div_eucl [definition, in div_eucl]
Make.div_eucl [definition, in div_eucl]
Make.div_gt_fold [lemma, in div_gt_fold]
Make.div_gt [definition, in div_gt]
Make.div_norm [definition, in div_norm]
Make.div_pow2_bound [lemma, in div_pow2_bound]
Make.div_gtnm [variable, in div_gtnm]
Make.div_gt_folded [abbreviation, in div_gt_folded]
Make.div2 [definition, in div2]
Make.div2 [definition, in div2]
Make.dom_t [definition, in dom_t]
Make.dom_op [instance, in dom_op]
Make.dom_spec [instance, in dom_spec]
Make.double_size_fold [lemma, in double_size_fold]
Make.double_size [definition, in double_size]
Make.double_size_level [lemma, in double_size_level]
Make.double_size_n [abbreviation, in double_size_n]
Make.E [module, in Make.E]
Make.E [module, in Make.E]
Make.E [module, in Make.E]
Make.elements [definition, in elements]
Make.elements [definition, in elements]
Make.elements_3w [lemma, in elements_3w]
Make.elements_3w [lemma, in elements_3w]
Make.elements_3 [lemma, in elements_3]
Make.elements_1 [lemma, in elements_1]
Make.elements_1 [lemma, in elements_1]
Make.elements_2 [lemma, in elements_2]
Make.elements_2 [lemma, in elements_2]
Make.Elt [section, in Elt]
Make.Elt [section, in Elt]
Make.Elt.elt [variable, in elt]
Make.Elt.elt [variable, in elt]
Make.Elt.elt' [variable, in elt']
Make.Elt.elt' [variable, in elt']
Make.Elt.elt'' [variable, in elt'']
Make.Elt.elt'' [variable, in elt'']
Make.empty [definition, in empty]
Make.empty [definition, in empty]
Make.Empty [definition, in Empty]
Make.Empty [definition, in Empty]
Make.empty_1 [lemma, in empty_1]
Make.empty_1 [lemma, in empty_1]
Make.eq [definition, in eq]
Make.eq [definition, in eq]
Make.eq [definition, in eq]
Make.eqb [definition, in eqb]
Make.eqb [definition, in eqb]
Make.equal [definition, in equal]
Make.equal [definition, in equal]
Make.Equal [definition, in Equal]
Make.Equal [definition, in Equal]
Make.equal_2 [lemma, in equal_2]
Make.equal_2 [lemma, in equal_2]
Make.equal_1 [lemma, in equal_1]
Make.equal_1 [lemma, in equal_1]
Make.Equiv [definition, in Equiv]
Make.Equiv [definition, in Equiv]
Make.Equivb [definition, in Equivb]
Make.Equivb [definition, in Equivb]
Make.eq_key_elt [definition, in eq_key_elt]
Make.eq_key_elt [definition, in eq_key_elt]
Make.eq_key [definition, in eq_key]
Make.eq_key [definition, in eq_key]
Make.eq_bool [definition, in eq_bool]
Make.eq00 [definition, in eq00]
Make.eq01 [definition, in eq01]
Make.eq02 [definition, in eq02]
Make.eq03 [definition, in eq03]
Make.eq04 [definition, in eq04]
Make.eq05 [definition, in eq05]
Make.eq06 [definition, in eq06]
Make.eval [variable, in eval]
Make.even [definition, in even]
Make.even [definition, in even]
Make.even_fold [lemma, in even_fold]
Make.extend [definition, in extend]
Make.extend_size [definition, in extend_size]
Make.find [definition, in find]
Make.find [definition, in find]
Make.find_2 [lemma, in find_2]
Make.find_2 [lemma, in find_2]
Make.find_1 [lemma, in find_1]
Make.find_1 [lemma, in find_1]
Make.fold [definition, in fold]
Make.fold [definition, in fold]
Make.fold_1 [lemma, in fold_1]
Make.fold_1 [lemma, in fold_1]
Make.gcd [definition, in gcd]
Make.gcd [definition, in gcd]
Make.gcd_gt [definition, in gcd_gt]
Make.gcd_cont [definition, in gcd_cont]
Make.gcd_gt_aux [definition, in gcd_gt_aux]
Make.gcd_gt_body [definition, in gcd_gt_body]
Make.head0 [definition, in head0]
Make.head0n [abbreviation, in head0n]
Make.head0_fold [lemma, in head0_fold]
Make.head0_zdigits [lemma, in head0_zdigits]
Make.In [definition, in In]
Make.In [definition, in In]
Make.inv [definition, in inv]
Make.inv_norm [definition, in inv_norm]
Make.irred [definition, in irred]
Make.is_reduced [projection, in is_reduced]
Make.is_reduced [constructor, in is_reduced]
Make.is_empty_1 [lemma, in is_empty_1]
Make.is_empty_1 [lemma, in is_empty_1]
Make.is_empty [definition, in is_empty]
Make.is_empty [definition, in is_empty]
Make.is_empty_2 [lemma, in is_empty_2]
Make.is_empty_2 [lemma, in is_empty_2]
Make.iter [definition, in iter]
Make.Iter [section, in Iter]
Make.IterSym [section, in IterSym]
Make.IterSym.f [variable, in f]
Make.IterSym.fg [variable, in fg]
Make.IterSym.fg' [variable, in fg']
Make.IterSym.fnm [variable, in fnm]
Make.IterSym.fn0 [variable, in fn0]
Make.IterSym.fn1 [variable, in fn1]
Make.IterSym.fn2 [variable, in fn2]
Make.IterSym.fn3 [variable, in fn3]
Make.IterSym.fn4 [variable, in fn4]
Make.IterSym.fn5 [variable, in fn5]
Make.IterSym.fn6 [variable, in fn6]
Make.IterSym.f' [variable, in f']
Make.IterSym.f0 [variable, in f0]
Make.IterSym.f1 [variable, in f1]
Make.IterSym.f2 [variable, in f2]
Make.IterSym.f3 [variable, in f3]
Make.IterSym.f4 [variable, in f4]
Make.IterSym.f5 [variable, in f5]
Make.IterSym.f6 [variable, in f6]
Make.IterSym.opp [variable, in opp]
Make.IterSym.P [variable, in P]
Make.IterSym.Pf [variable, in Pf]
Make.IterSym.Pfg [variable, in Pfg]
Make.IterSym.Pfnm [variable, in Pfnm]
Make.IterSym.Popp [variable, in Popp]
Make.IterSym.res [variable, in res]
Make.iter_sym [definition, in iter_sym]
Make.iter_folded [abbreviation, in iter_folded]
Make.iter_t [definition, in iter_t]
Make.iter_mk_t [lemma, in iter_mk_t]
Make.iter_sym_folded [abbreviation, in iter_sym_folded]
Make.Iter.f [variable, in f]
Make.Iter.fd [variable, in fd]
Make.Iter.fg [variable, in fg]
Make.Iter.fnm [variable, in fnm]
Make.Iter.fn0 [variable, in fn0]
Make.Iter.fn1 [variable, in fn1]
Make.Iter.fn2 [variable, in fn2]
Make.Iter.fn3 [variable, in fn3]
Make.Iter.fn4 [variable, in fn4]
Make.Iter.fn5 [variable, in fn5]
Make.Iter.fn6 [variable, in fn6]
Make.Iter.f0 [variable, in f0]
Make.Iter.f0n [variable, in f0n]
Make.Iter.f1 [variable, in f1]
Make.Iter.f1n [variable, in f1n]
Make.Iter.f2 [variable, in f2]
Make.Iter.f2n [variable, in f2n]
Make.Iter.f3 [variable, in f3]
Make.Iter.f3n [variable, in f3n]
Make.Iter.f4 [variable, in f4]
Make.Iter.f4n [variable, in f4n]
Make.Iter.f5 [variable, in f5]
Make.Iter.f5n [variable, in f5n]
Make.Iter.f6 [variable, in f6]
Make.Iter.f6n [variable, in f6n]
Make.Iter.P [variable, in P]
Make.Iter.Pf [variable, in Pf]
Make.Iter.Pfd [variable, in Pfd]
Make.Iter.Pfd' [variable, in Pfd']
Make.Iter.Pfg [variable, in Pfg]
Make.Iter.Pfg' [variable, in Pfg']
Make.Iter.Pfnm [variable, in Pfnm]
Make.Iter.Pf' [variable, in Pf']
Make.Iter.res [variable, in res]
Make.key [definition, in key]
Make.key [definition, in key]
Make.land [definition, in land]
Make.land [definition, in land]
Make.ldiff [definition, in ldiff]
Make.ldiff [definition, in ldiff]
Make.le [definition, in le]
Make.le [definition, in le]
Make.le [definition, in le]
Make.leb [definition, in leb]
Make.leb [definition, in leb]
Make.level [definition, in level]
Make.log2 [definition, in log2]
Make.log2 [definition, in log2]
Make.log2n [abbreviation, in log2n]
Make.log2_fold [lemma, in log2_fold]
Make.log2_digits_head0 [lemma, in log2_digits_head0]
Make.lor [definition, in lor]
Make.lor [definition, in lor]
Make.lt [definition, in lt]
Make.lt [definition, in lt]
Make.lt [definition, in lt]
Make.ltb [definition, in ltb]
Make.ltb [definition, in ltb]
Make.lt_key [definition, in lt_key]
Make.lxor [definition, in lxor]
Make.lxor [definition, in lxor]
Make.make_op_WW [variable, in make_op_WW]
Make.make_op_aux [definition, in make_op_aux]
Make.make_op [instance, in make_op]
Make.Make_op [section, in Make_op]
Make.make_op_omake [lemma, in make_op_omake]
Make.make_op_S [lemma, in make_op_S]
Make.Make_op.mk [variable, in mk]
Make.make_op_list [definition, in make_op_list]
Make.map [definition, in map]
Make.map [definition, in map]
Make.mapi [definition, in mapi]
Make.mapi [definition, in mapi]
Make.mapi_2 [lemma, in mapi_2]
Make.mapi_2 [lemma, in mapi_2]
Make.mapi_1 [lemma, in mapi_1]
Make.mapi_1 [lemma, in mapi_1]
Make.MapsTo [definition, in MapsTo]
Make.MapsTo [definition, in MapsTo]
Make.MapsTo_1 [lemma, in MapsTo_1]
Make.MapsTo_1 [lemma, in MapsTo_1]
Make.map_1 [lemma, in map_1]
Make.map_1 [lemma, in map_1]
Make.map_2 [lemma, in map_2]
Make.map_2 [lemma, in map_2]
Make.map2 [definition, in map2]
Make.map2 [definition, in map2]
Make.map2_2 [lemma, in map2_2]
Make.map2_2 [lemma, in map2_2]
Make.map2_1 [lemma, in map2_1]
Make.map2_1 [lemma, in map2_1]
Make.max [definition, in max]
Make.max [definition, in max]
Make.max [definition, in max]
Make.mem [definition, in mem]
Make.mem [definition, in mem]
Make.mem_1 [lemma, in mem_1]
Make.mem_1 [lemma, in mem_1]
Make.mem_2 [lemma, in mem_2]
Make.mem_2 [lemma, in mem_2]
Make.min [definition, in min]
Make.min [definition, in min]
Make.min [definition, in min]
Make.minus_one [definition, in minus_one]
Make.minus_one [definition, in minus_one]
Make.mk_t_S_level [lemma, in mk_t_S_level]
Make.Mk_t [constructor, in Mk_t]
Make.mk_t_w [definition, in mk_t_w]
Make.mk_t_5w [variable, in mk_t_5w]
Make.mk_opt_t [definition, in mk_opt_t]
Make.mk_t_4w [variable, in mk_t_4w]
Make.mk_t_0w [variable, in mk_t_0w]
Make.mk_t_2w [variable, in mk_t_2w]
Make.mk_t [definition, in mk_t]
Make.mk_t_w' [variable, in mk_t_w']
Make.mk_t_3w [variable, in mk_t_3w]
Make.mk_t_S [definition, in mk_t_S]
Make.mk_t_1w [variable, in mk_t_1w]
Make.modulo [definition, in modulo]
Make.modulo [definition, in modulo]
Make.mod_gt [definition, in mod_gt]
Make.mod_gt_folded [abbreviation, in mod_gt_folded]
Make.mod_gt_fold [lemma, in mod_gt_fold]
Make.mod_gtnm [variable, in mod_gtnm]
Make.MSet [module, in Make.MSet]
Make.MSet [module, in Make.MSet]
Make.mul [definition, in mul]
Make.mul [definition, in mul]
Make.mul [definition, in mul]
Make.mulnm [definition, in mulnm]
Make.mul_norm_Qz_Qq [definition, in mul_norm_Qz_Qq]
Make.mul_fold [lemma, in mul_fold]
Make.mul_norm [definition, in mul_norm]
Make.mul_folded [abbreviation, in mul_folded]
Make.Ndigits [definition, in Ndigits]
Make.Ndigitsn [abbreviation, in Ndigitsn]
Make.Ndigits_fold [lemma, in Ndigits_fold]
Make.Neg [constructor, in Neg]
Make.nmake_op_S [lemma, in nmake_op_S]
Make.nmake_op [definition, in nmake_op]
Make.nmake_WW [lemma, in nmake_WW]
Make.nmake_double [lemma, in nmake_double]
Make.Nn [constructor, in Nn]
Make.NoDup [projection, in NoDup]
Make.norm [definition, in norm]
Make.norm_denum [definition, in norm_denum]
Make.norm_pos [definition, in norm_pos]
Make.N_to_Z_pos [lemma, in N_to_Z_pos]
Make.N0 [constructor, in N0]
Make.N1 [constructor, in N1]
Make.N2 [constructor, in N2]
Make.N3 [constructor, in N3]
Make.N4 [constructor, in N4]
Make.N5 [constructor, in N5]
Make.N6 [constructor, in N6]
Make.odd [definition, in odd]
Make.odd [definition, in odd]
Make.of_Z [definition, in of_Z]
Make.of_Z [definition, in of_Z]
Make.of_Qc [definition, in of_Qc]
Make.of_pos [definition, in of_pos]
Make.of_Q [definition, in of_Q]
Make.of_N [definition, in of_N]
Make.omake_op [definition, in omake_op]
Make.one [definition, in one]
Make.one [definition, in one]
Make.one [definition, in one]
Make.opp [definition, in opp]
Make.opp [definition, in opp]
Make.opt_ok [definition, in opt_ok]
Make.pheight [definition, in pheight]
Make.pheight_correct [lemma, in pheight_correct]
Make.plus_t [definition, in plus_t]
Make.plus_t' [definition, in plus_t']
Make.plus_t_equiv [lemma, in plus_t_equiv]
Make.Pos [constructor, in Pos]
Make.pow [definition, in pow]
Make.pow [definition, in pow]
Make.power [definition, in power]
Make.power_norm [definition, in power_norm]
Make.power_pos [definition, in power_pos]
Make.pow_N [definition, in pow_N]
Make.pow_N [definition, in pow_N]
Make.pow_pos [definition, in pow_pos]
Make.pow_pos [definition, in pow_pos]
Make.pow2_pos_minus_1 [lemma, in pow2_pos_minus_1]
Make.pred [definition, in pred]
Make.pred [definition, in pred]
Make.predn [abbreviation, in predn]
Make.pred_t [definition, in pred_t]
Make.pred_fold [lemma, in pred_fold]
Make.Qq [constructor, in Qq]
Make.quot [definition, in quot]
Make.Qz [constructor, in Qz]
Make.Raw [module, in Make.Raw]
Make.Raw [module, in Make.Raw]
Make.Raw [module, in Make.Raw]
Make.Raw [module, in Make.Raw]
Make.Raw [module, in Make.Raw]
Make.red [definition, in red]
Make.reduce [definition, in reduce]
Make.Reduced [record, in Reduced]
Make.Reduced [inductive, in Reduced]
Make.reduce_3 [definition, in reduce_3]
Make.reduce_2 [definition, in reduce_2]
Make.reduce_equiv [lemma, in reduce_equiv]
Make.reduce_4 [definition, in reduce_4]
Make.reduce_7 [definition, in reduce_7]
Make.reduce_n [definition, in reduce_n]
Make.reduce_6 [definition, in reduce_6]
Make.reduce_0 [definition, in reduce_0]
Make.reduce_1 [definition, in reduce_1]
Make.reduce_5 [definition, in reduce_5]
Make.red_t [definition, in red_t]
Make.rem [definition, in rem]
Make.remove [definition, in remove]
Make.remove [definition, in remove]
Make.remove_min_spec1 [lemma, in remove_min_spec1]
Make.remove_2 [lemma, in remove_2]
Make.remove_2 [lemma, in remove_2]
Make.remove_min_spec2 [lemma, in remove_min_spec2]
Make.remove_1 [lemma, in remove_1]
Make.remove_1 [lemma, in remove_1]
Make.remove_3 [lemma, in remove_3]
Make.remove_3 [lemma, in remove_3]
Make.remove_min [definition, in remove_min]
Make.SameLevel [section, in SameLevel]
Make.SameLevel.f [variable, in f]
Make.SameLevel.fn [variable, in fn]
Make.SameLevel.f0 [variable, in f0]
Make.SameLevel.f1 [variable, in f1]
Make.SameLevel.f2 [variable, in f2]
Make.SameLevel.f3 [variable, in f3]
Make.SameLevel.f4 [variable, in f4]
Make.SameLevel.f5 [variable, in f5]
Make.SameLevel.f6 [variable, in f6]
Make.SameLevel.P [variable, in P]
Make.SameLevel.Pf [variable, in Pf]
Make.SameLevel.Pf' [variable, in Pf']
Make.SameLevel.res [variable, in res]
Make.same_level_folded [abbreviation, in same_level_folded]
Make.same_level [definition, in same_level]
Make.sgn [definition, in sgn]
Make.shiftl [definition, in shiftl]
Make.shiftl [definition, in shiftl]
Make.shiftl_aux [definition, in shiftl_aux]
Make.shiftl_aux_body [definition, in shiftl_aux_body]
Make.shiftr [definition, in shiftr]
Make.shiftr [definition, in shiftr]
Make.shiftrn [abbreviation, in shiftrn]
Make.shiftr_fold [lemma, in shiftr_fold]
Make.Size [abbreviation, in Size]
Make.SizePlus [abbreviation, in SizePlus]
Make.slist [record, in slist]
Make.slist [record, in slist]
Make.sorted [projection, in sorted]
Make.spec_double_size_head0_pos [lemma, in spec_double_size_head0_pos]
Make.spec_oppc_bis [lemma, in spec_oppc_bis]
Make.spec_shiftl_aux_body [lemma, in spec_shiftl_aux_body]
Make.spec_norm_pos [lemma, in spec_norm_pos]
Make.spec_switch [lemma, in spec_switch]
Make.spec_comparec [lemma, in spec_comparec]
Make.spec_of_pos [lemma, in spec_of_pos]
Make.spec_of_Z [lemma, in spec_of_Z]
Make.spec_ltb [lemma, in spec_ltb]
Make.spec_ltb [lemma, in spec_ltb]
Make.spec_shiftl [lemma, in spec_shiftl]
Make.spec_shiftl [lemma, in spec_shiftl]
Make.spec_log2_pos [lemma, in spec_log2_pos]
Make.spec_of_Q [lemma, in spec_of_Q]
Make.spec_pos [lemma, in spec_pos]
Make.spec_pred [lemma, in spec_pred]
Make.spec_pred [lemma, in spec_pred]
Make.spec_sub_norm [lemma, in spec_sub_norm]
Make.spec_norm [lemma, in spec_norm]
Make.spec_head00 [lemma, in spec_head00]
Make.spec_div_normc [lemma, in spec_div_normc]
Make.spec_sub_normc_bis [lemma, in spec_sub_normc_bis]
Make.spec_plus_t [lemma, in spec_plus_t]
Make.spec_shiftr_pow2 [lemma, in spec_shiftr_pow2]
Make.spec_max [lemma, in spec_max]
Make.spec_max [lemma, in spec_max]
Make.spec_max [lemma, in spec_max]
Make.spec_mk_t [lemma, in spec_mk_t]
Make.spec_power_posc [lemma, in spec_power_posc]
Make.spec_sgn [lemma, in spec_sgn]
Make.spec_extend_tr [variable, in spec_extend_tr]
Make.spec_leb [lemma, in spec_leb]
Make.spec_leb [lemma, in spec_leb]
Make.spec_add [lemma, in spec_add]
Make.spec_add [lemma, in spec_add]
Make.spec_add [lemma, in spec_add]
Make.spec_sqrt_aux [lemma, in spec_sqrt_aux]
Make.spec_log2_0 [lemma, in spec_log2_0]
Make.spec_land [lemma, in spec_land]
Make.spec_land [lemma, in spec_land]
Make.spec_oppc [lemma, in spec_oppc]
Make.spec_double_size [lemma, in spec_double_size]
Make.spec_odd [lemma, in spec_odd]
Make.spec_odd [lemma, in spec_odd]
Make.spec_digits [lemma, in spec_digits]
Make.spec_shiftr [lemma, in spec_shiftr]
Make.spec_shiftr [lemma, in spec_shiftr]
Make.spec_divn1 [variable, in spec_divn1]
Make.spec_inv_normc_bis [lemma, in spec_inv_normc_bis]
Make.spec_reduce_n [lemma, in spec_reduce_n]
Make.spec_add_normc [lemma, in spec_add_normc]
Make.spec_div_norm [lemma, in spec_div_norm]
Make.spec_same_level_dep [lemma, in spec_same_level_dep]
Make.spec_2 [lemma, in spec_2]
Make.spec_2 [lemma, in spec_2]
Make.spec_div_normc_bis [lemma, in spec_div_normc_bis]
Make.spec_even_aux [lemma, in spec_even_aux]
Make.spec_eval_size [lemma, in spec_eval_size]
Make.spec_modn1 [variable, in spec_modn1]
Make.spec_mk_t_w [lemma, in spec_mk_t_w]
Make.spec_mod_gt [lemma, in spec_mod_gt]
Make.spec_div2 [lemma, in spec_div2]
Make.spec_div2 [lemma, in spec_div2]
Make.spec_wn_mul [lemma, in spec_wn_mul]
Make.spec_shiftl_aux [lemma, in spec_shiftl_aux]
Make.spec_double_size_head0 [lemma, in spec_double_size_head0]
Make.spec_mul [lemma, in spec_mul]
Make.spec_mul [lemma, in spec_mul]
Make.spec_mul [lemma, in spec_mul]
Make.spec_mul_normc_bis [lemma, in spec_mul_normc_bis]
Make.spec_inv [lemma, in spec_inv]
Make.spec_head0 [lemma, in spec_head0]
Make.spec_testbit [lemma, in spec_testbit]
Make.spec_testbit [lemma, in spec_testbit]
Make.spec_tail00 [lemma, in spec_tail00]
Make.spec_rem [lemma, in spec_rem]
Make.spec_double_size_digits [lemma, in spec_double_size_digits]
Make.spec_divc [lemma, in spec_divc]
Make.spec_plus_t' [lemma, in spec_plus_t']
Make.spec_power_pos [lemma, in spec_power_pos]
Make.spec_extend_size [lemma, in spec_extend_size]
Make.spec_1 [lemma, in spec_1]
Make.spec_1 [lemma, in spec_1]
Make.spec_1 [lemma, in spec_1]
Make.spec_mulc [lemma, in spec_mulc]
Make.spec_quot [lemma, in spec_quot]
Make.spec_irred [lemma, in spec_irred]
Make.spec_add_normc_bis [lemma, in spec_add_normc_bis]
Make.spec_m1 [lemma, in spec_m1]
Make.spec_m1 [lemma, in spec_m1]
Make.spec_eqb [lemma, in spec_eqb]
Make.spec_eqb [lemma, in spec_eqb]
Make.spec_mul_norm [lemma, in spec_mul_norm]
Make.spec_tail0 [lemma, in spec_tail0]
Make.spec_lxor [lemma, in spec_lxor]
Make.spec_lxor [lemma, in spec_lxor]
Make.spec_irred_zero [lemma, in spec_irred_zero]
Make.spec_squarec [lemma, in spec_squarec]
Make.spec_modulo [lemma, in spec_modulo]
Make.spec_modulo [lemma, in spec_modulo]
Make.spec_zeron [lemma, in spec_zeron]
Make.spec_extend [lemma, in spec_extend]
Make.spec_unsafe_shiftl [lemma, in spec_unsafe_shiftl]
Make.spec_compare [lemma, in spec_compare]
Make.spec_compare [lemma, in spec_compare]
Make.spec_compare [lemma, in spec_compare]
Make.spec_muln [lemma, in spec_muln]
Make.spec_subc [lemma, in spec_subc]
Make.spec_iter [lemma, in spec_iter]
Make.spec_same_level [lemma, in spec_same_level]
Make.spec_pow [lemma, in spec_pow]
Make.spec_pow [lemma, in spec_pow]
Make.spec_add_norm [lemma, in spec_add_norm]
Make.spec_mul_norm_Qz_Qq [lemma, in spec_mul_norm_Qz_Qq]
Make.spec_even [lemma, in spec_even]
Make.spec_even [lemma, in spec_even]
Make.spec_ldiff [lemma, in spec_ldiff]
Make.spec_ldiff [lemma, in spec_ldiff]
Make.spec_mul_add_n1 [lemma, in spec_mul_add_n1]
Make.spec_cast_r [variable, in spec_cast_r]
Make.spec_mk_t_w' [lemma, in spec_mk_t_w']
Make.spec_mul_normc [lemma, in spec_mul_normc]
Make.spec_div [lemma, in spec_div]
Make.spec_div [lemma, in spec_div]
Make.spec_div [definition, in spec_div]
Make.spec_div_eucl [lemma, in spec_div_eucl]
Make.spec_div_eucl [lemma, in spec_div_eucl]
Make.spec_pow_pos [lemma, in spec_pow_pos]
Make.spec_pow_pos [lemma, in spec_pow_pos]
Make.spec_iter_sym [lemma, in spec_iter_sym]
Make.spec_pred0 [lemma, in spec_pred0]
Make.spec_lor [lemma, in spec_lor]
Make.spec_lor [lemma, in spec_lor]
Make.spec_eq_bool [lemma, in spec_eq_bool]
Make.spec_sub [lemma, in spec_sub]
Make.spec_sub [lemma, in spec_sub]
Make.spec_sub [lemma, in spec_sub]
Make.spec_mk_t_S [lemma, in spec_mk_t_S]
Make.spec_succ [lemma, in spec_succ]
Make.spec_succ [lemma, in spec_succ]
Make.spec_unsafe_shiftl_aux [lemma, in spec_unsafe_shiftl_aux]
Make.spec_gcd_gt [lemma, in spec_gcd_gt]
Make.spec_succ_t [lemma, in spec_succ_t]
Make.spec_abs [lemma, in spec_abs]
Make.spec_same_level_0 [lemma, in spec_same_level_0]
Make.spec_div_gt_aux [lemma, in spec_div_gt_aux]
Make.spec_power [lemma, in spec_power]
Make.spec_sub_pos [lemma, in spec_sub_pos]
Make.spec_extend_WW [variable, in spec_extend_WW]
Make.spec_power_norm [lemma, in spec_power_norm]
Make.spec_sqrt [lemma, in spec_sqrt]
Make.spec_sqrt [lemma, in spec_sqrt]
Make.spec_comparen_m [variable, in spec_comparen_m]
Make.spec_shiftl_pow2 [lemma, in spec_shiftl_pow2]
Make.spec_sub_normc [lemma, in spec_sub_normc]
Make.spec_norm_pos_pos [lemma, in spec_norm_pos_pos]
Make.spec_norm_denum [lemma, in spec_norm_denum]
Make.spec_inv_normc [lemma, in spec_inv_normc]
Make.spec_min [lemma, in spec_min]
Make.spec_min [lemma, in spec_min]
Make.spec_min [lemma, in spec_min]
Make.spec_opp [lemma, in spec_opp]
Make.spec_opp [lemma, in spec_opp]
Make.spec_log2 [lemma, in spec_log2]
Make.spec_log2 [lemma, in spec_log2]
Make.spec_gcd [lemma, in spec_gcd]
Make.spec_gcd [lemma, in spec_gcd]
Make.spec_reduce [lemma, in spec_reduce]
Make.spec_inv_norm [lemma, in spec_inv_norm]
Make.spec_pred_pos [lemma, in spec_pred_pos]
Make.spec_pow_N [lemma, in spec_pow_N]
Make.spec_pow_N [lemma, in spec_pow_N]
Make.spec_cast_l [variable, in spec_cast_l]
Make.spec_square [lemma, in spec_square]
Make.spec_square [lemma, in spec_square]
Make.spec_square [lemma, in spec_square]
Make.spec_red_t [lemma, in spec_red_t]
Make.spec_Ndigits [lemma, in spec_Ndigits]
Make.spec_get_endn [lemma, in spec_get_endn]
Make.spec_addc [lemma, in spec_addc]
Make.spec_invc [lemma, in spec_invc]
Make.spec_of_Qc [lemma, in spec_of_Qc]
Make.spec_sub0 [lemma, in spec_sub0]
Make.spec_of_N [lemma, in spec_of_N]
Make.spec_0 [lemma, in spec_0]
Make.spec_0 [lemma, in spec_0]
Make.spec_0 [lemma, in spec_0]
Make.spec_red [lemma, in spec_red]
Make.spec_div_gt [lemma, in spec_div_gt]
Make.sqrt [definition, in sqrt]
Make.sqrt [definition, in sqrt]
Make.sqrtn [abbreviation, in sqrtn]
Make.sqrt_fold [lemma, in sqrt_fold]
Make.square [definition, in square]
Make.square [definition, in square]
Make.square [definition, in square]
Make.squaren [abbreviation, in squaren]
Make.square_fold [lemma, in square_fold]
Make.strong_spec_of_Q [lemma, in strong_spec_of_Q]
Make.strong_spec_inv_norm [instance, in strong_spec_inv_norm]
Make.strong_spec_power_pos [instance, in strong_spec_power_pos]
Make.strong_spec_red [lemma, in strong_spec_red]
Make.strong_spec_of_Qc [lemma, in strong_spec_of_Qc]
Make.strong_spec_power_norm [instance, in strong_spec_power_norm]
Make.strong_spec_opp_norm [instance, in strong_spec_opp_norm]
Make.strong_spec_of_Qc_bis [instance, in strong_spec_of_Qc_bis]
Make.strong_spec_sub_norm [instance, in strong_spec_sub_norm]
Make.strong_spec_div_norm [instance, in strong_spec_div_norm]
Make.strong_spec_mul_norm [instance, in strong_spec_mul_norm]
Make.strong_spec_check_int [lemma, in strong_spec_check_int]
Make.strong_spec_irred [lemma, in strong_spec_irred]
Make.strong_spec_mul_norm_Qz_Qq [instance, in strong_spec_mul_norm_Qz_Qq]
Make.strong_spec_opp [lemma, in strong_spec_opp]
Make.strong_spec_add_norm [instance, in strong_spec_add_norm]
Make.strong_spec_norm [lemma, in strong_spec_norm]
Make.sub [definition, in sub]
Make.sub [definition, in sub]
Make.sub [definition, in sub]
Make.subn [abbreviation, in subn]
Make.sub_norm [definition, in sub_norm]
Make.sub_fold [lemma, in sub_fold]
Make.succ [definition, in succ]
Make.succ [definition, in succ]
Make.succn [abbreviation, in succn]
Make.succ_t [definition, in succ_t]
Make.succ_pred_t [lemma, in succ_pred_t]
Make.succ_fold [lemma, in succ_fold]
Make.switch [definition, in switch]
Make.t [definition, in t]
Make.t [definition, in t]
Make.t [definition, in t]
Make.t [definition, in t]
Make.t [definition, in t]
Make.tail0 [definition, in tail0]
Make.tail0n [abbreviation, in tail0n]
Make.tail0_fold [lemma, in tail0_fold]
Make.testbit [definition, in testbit]
Make.testbit [definition, in testbit]
Make.this [projection, in this]
Make.this [projection, in this]
Make.to_N [definition, in to_N]
Make.to_N [definition, in to_N]
Make.to_Qc [definition, in to_Qc]
Make.to_Z [definition, in to_Z]
Make.to_Z [definition, in to_Z]
Make.to_Q [definition, in to_Q]
Make.two [definition, in two]
Make.two [definition, in two]
Make.t_ [inductive, in t_]
Make.t_ [inductive, in t_]
Make.t' [inductive, in t']
Make.unsafe_shiftl_fold [lemma, in unsafe_shiftl_fold]
Make.unsafe_shiftl [definition, in unsafe_shiftl]
Make.unsafe_shiftln [abbreviation, in unsafe_shiftln]
Make.View_t [inductive, in View_t]
Make.wn_mul [definition, in wn_mul]
Make.wn_spec [instance, in wn_spec]
Make.wn_divn1 [definition, in wn_divn1]
Make.wn_modn1 [definition, in wn_modn1]
Make.w0 [abbreviation, in w0]
Make.w0_op [abbreviation, in w0_op]
Make.w0_spec [instance, in w0_spec]
Make.w1 [definition, in w1]
Make.w1_spec [instance, in w1_spec]
Make.w1_op [instance, in w1_op]
Make.w2 [definition, in w2]
Make.w2_spec [instance, in w2_spec]
Make.w2_op [instance, in w2_op]
Make.w3 [definition, in w3]
Make.w3_op [instance, in w3_op]
Make.w3_spec [instance, in w3_spec]
Make.w4 [definition, in w4]
Make.w4_op [instance, in w4_op]
Make.w4_spec [instance, in w4_spec]
Make.w5 [definition, in w5]
Make.w5_spec [instance, in w5_spec]
Make.w5_op [instance, in w5_op]
Make.w6 [definition, in w6]
Make.w6_spec [instance, in w6_spec]
Make.w6_op [instance, in w6_op]
Make.w7_spec [instance, in w7_spec]
Make.w7_op [instance, in w7_op]
Make.w8_op [instance, in w8_op]
Make.w9_op [instance, in w9_op]
Make.X' [module, in Make.X']
Make.X' [module, in Make.X']
Make.zero [definition, in zero]
Make.zero [definition, in zero]
Make.zero [definition, in zero]
Make.zeron [definition, in zeron]
Make.zero0 [definition, in zero0]
Make.Zlnot_alt3 [lemma, in Zlnot_alt3]
Make.Zlnot_alt2 [lemma, in Zlnot_alt2]
Make.Zlnot_alt1 [lemma, in Zlnot_alt1]
Make.zn2z_map [definition, in zn2z_map]
Make.zn2z_map_id [lemma, in zn2z_map_id]
Make.Zspec_gcd_gt_aux [lemma, in Zspec_gcd_gt_aux]
Make.Zspec_gcd_gt_body [lemma, in Zspec_gcd_gt_body]
[ _ ] [notation, in ::'['_x_']']
[ _ ] [notation, in ::'['_x_']']
[ _ ] [notation, in ::'['_x_']']
[[ _ ]] [notation, in ::'[['_x_']]']
map [definition, in map]
map [definition, in map]
map [definition, in map]
Map [section, in Map]
Map [section, in Map]
map_eq_nil [lemma, in map_eq_nil]
map_nth [lemma, in map_nth]
map_length [lemma, in map_length]
map_rev [lemma, in map_rev]
map_app [lemma, in map_app]
map_id [lemma, in map_id]
map_ext [lemma, in map_ext]
map_nth_error [lemma, in map_nth_error]
map_map [lemma, in map_map]
Map.A [variable, in A]
Map.A [variable, in A]
Map.B [variable, in B]
Map.B [variable, in B]
Map.f [variable, in f]
Map.f [variable, in f]
map2 [definition, in map2]
match_eq [definition, in match_eq]
match_eq_rewrite [lemma, in match_eq_rewrite]
max [abbreviation, in max]
max [definition, in max]
Max [library]
MaxLogicalProperties [module, in MaxLogicalProperties]
MaxLogicalProperties.le_max_l [lemma, in le_max_l]
MaxLogicalProperties.le_max_r [lemma, in le_max_r]
MaxLogicalProperties.max_le_compat_l [lemma, in max_le_compat_l]
MaxLogicalProperties.max_r_iff [lemma, in max_r_iff]
MaxLogicalProperties.max_unicity [lemma, in max_unicity]
MaxLogicalProperties.max_lub_iff [lemma, in max_lub_iff]
MaxLogicalProperties.max_id [lemma, in max_id]
MaxLogicalProperties.max_comm [lemma, in max_comm]
MaxLogicalProperties.max_le [lemma, in max_le]
MaxLogicalProperties.max_le_iff [lemma, in max_le_iff]
MaxLogicalProperties.max_lub_lt_iff [lemma, in max_lub_lt_iff]
MaxLogicalProperties.max_lub_lt [lemma, in max_lub_lt]
MaxLogicalProperties.max_lub_r [lemma, in max_lub_r]
MaxLogicalProperties.max_spec [lemma, in max_spec]
MaxLogicalProperties.max_spec_le [lemma, in max_spec_le]
MaxLogicalProperties.max_lt_iff [lemma, in max_lt_iff]
MaxLogicalProperties.max_le_compat_r [lemma, in max_le_compat_r]
MaxLogicalProperties.max_lub_l [lemma, in max_lub_l]
MaxLogicalProperties.max_le_compat [lemma, in max_le_compat]
MaxLogicalProperties.max_mono [lemma, in max_mono]
MaxLogicalProperties.max_lub [lemma, in max_lub]
MaxLogicalProperties.max_l_iff [lemma, in max_l_iff]
MaxLogicalProperties.max_assoc [lemma, in max_assoc]
MaxLogicalProperties.max_compat [instance, in max_compat]
MaxLogicalProperties.max_idempotent [abbreviation, in max_idempotent]
MaxLogicalProperties.max_unicity_ext [lemma, in max_unicity_ext]
MaxLogicalProperties.Private_Tac [module, in MaxLogicalProperties.Private_Tac]
maxN [lemma, in maxN]
MaxRlist [definition, in MaxRlist]
MaxRlist_P1 [lemma, in MaxRlist_P1]
MaxRlist_P2 [lemma, in MaxRlist_P2]
max_dec [definition, in max_dec]
max_case_strong [definition, in max_case_strong]
max_N [definition, in max_N]
max_case [definition, in max_case]
max_comm [definition, in max_comm]
max_0_l [definition, in max_0_l]
max_lub_r [definition, in max_lub_r]
max_case2 [abbreviation, in max_case2]
max_0_r [definition, in max_0_r]
max_spec [definition, in max_spec]
max_lub_l [definition, in max_lub_l]
max_lub [definition, in max_lub]
max_SS [abbreviation, in max_SS]
max_assoc [definition, in max_assoc]
max_r [definition, in max_r]
max_r [lemma, in max_r]
max_min_disassoc [abbreviation, in max_min_disassoc]
max_idempotent [definition, in max_idempotent]
max_l [definition, in max_l]
max_l [lemma, in max_l]
Measure [record, in Measure]
measure_wf [lemma, in measure_wf]
Measure_well_founded.T [variable, in T]
Measure_well_founded [section, in Measure_well_founded]
Measure_well_founded.R [variable, in R]
Measure_well_founded.M [variable, in M]
Measure_well_founded.wf [variable, in wf]
Measure_well_founded.m [variable, in m]
MemoFunction [section, in MemoFunction]
MemoFunction.A [variable, in A]
MemoFunction.f [variable, in f]
MemoFunction.g [variable, in g]
MemoFunction.Hg_correct [variable, in Hg_correct]
memo_get [definition, in memo_get]
memo_get_val [definition, in memo_get_val]
memo_make [definition, in memo_make]
memo_mval [constructor, in memo_mval]
memo_val [inductive, in memo_val]
memo_get_correct [lemma, in memo_get_correct]
memo_list [definition, in memo_list]
meq [definition, in meq]
meq_congr [lemma, in meq_congr]
meq_right [lemma, in meq_right]
meq_refl [lemma, in meq_refl]
meq_trans [lemma, in meq_trans]
meq_left [lemma, in meq_left]
meq_sym [lemma, in meq_sym]
meq_singleton [lemma, in meq_singleton]
merge [lemma, in merge]
Mergesort [library]
merge_lem [inductive, in merge_lem]
merge_exist [constructor, in merge_exist]
Metric_Space [record, in Metric_Space]
mid_Rlist [definition, in mid_Rlist]
min [abbreviation, in min]
min [definition, in min]
Min [library]
MiniDecidableType [module, in MiniDecidableType]
MiniDecidableType [module, in MiniDecidableType]
MiniDecidableType.eq_dec [axiom, in eq_dec]
MiniOrderedType [module, in MiniOrderedType]
MiniOrderedType.compare [axiom, in compare]
MiniOrderedType.eq [axiom, in eq]
MiniOrderedType.eq_refl [axiom, in eq_refl]
MiniOrderedType.eq_sym [axiom, in eq_sym]
MiniOrderedType.eq_trans [axiom, in eq_trans]
MiniOrderedType.lt [axiom, in lt]
MiniOrderedType.lt_not_eq [axiom, in lt_not_eq]
MiniOrderedType.lt_trans [axiom, in lt_trans]
MiniOrderedType.t [axiom, in t]
MinMaxDecProperties [module, in MinMaxDecProperties]
MinMaxDecProperties.max_dec [lemma, in max_dec]
MinMaxDecProperties.max_case_strong [lemma, in max_case_strong]
MinMaxDecProperties.max_case [lemma, in max_case]
MinMaxDecProperties.min_case [lemma, in min_case]
MinMaxDecProperties.min_case_strong [lemma, in min_case_strong]
MinMaxDecProperties.min_dec [lemma, in min_dec]
MinMaxLogicalProperties [module, in MinMaxLogicalProperties]
MinMaxLogicalProperties.le_min_l [lemma, in le_min_l]
MinMaxLogicalProperties.le_min_r [lemma, in le_min_r]
MinMaxLogicalProperties.max_min_antimono [lemma, in max_min_antimono]
MinMaxLogicalProperties.max_min_absorption [lemma, in max_min_absorption]
MinMaxLogicalProperties.max_min_modular [lemma, in max_min_modular]
MinMaxLogicalProperties.max_min_distr [lemma, in max_min_distr]
MinMaxLogicalProperties.max_min_disassoc [lemma, in max_min_disassoc]
MinMaxLogicalProperties.min_spec [lemma, in min_spec]
MinMaxLogicalProperties.min_comm [lemma, in min_comm]
MinMaxLogicalProperties.min_max_modular [lemma, in min_max_modular]
MinMaxLogicalProperties.min_le_compat_r [lemma, in min_le_compat_r]
MinMaxLogicalProperties.min_le_compat [lemma, in min_le_compat]
MinMaxLogicalProperties.min_r_iff [lemma, in min_r_iff]
MinMaxLogicalProperties.min_lt_iff [lemma, in min_lt_iff]
MinMaxLogicalProperties.min_mono [lemma, in min_mono]
MinMaxLogicalProperties.min_le [lemma, in min_le]
MinMaxLogicalProperties.min_max_antimono [lemma, in min_max_antimono]
MinMaxLogicalProperties.min_spec_le [lemma, in min_spec_le]
MinMaxLogicalProperties.min_le_iff [lemma, in min_le_iff]
MinMaxLogicalProperties.min_unicity [lemma, in min_unicity]
MinMaxLogicalProperties.min_assoc [lemma, in min_assoc]
MinMaxLogicalProperties.min_glb_lt_iff [lemma, in min_glb_lt_iff]
MinMaxLogicalProperties.min_glb_iff [lemma, in min_glb_iff]
MinMaxLogicalProperties.min_compat [instance, in min_compat]
MinMaxLogicalProperties.min_le_compat_l [lemma, in min_le_compat_l]
MinMaxLogicalProperties.min_glb [lemma, in min_glb]
MinMaxLogicalProperties.min_glb_r [lemma, in min_glb_r]
MinMaxLogicalProperties.min_glb_l [lemma, in min_glb_l]
MinMaxLogicalProperties.min_unicity_ext [lemma, in min_unicity_ext]
MinMaxLogicalProperties.min_glb_lt [lemma, in min_glb_lt]
MinMaxLogicalProperties.min_id [lemma, in min_id]
MinMaxLogicalProperties.min_max_distr [lemma, in min_max_distr]
MinMaxLogicalProperties.min_l_iff [lemma, in min_l_iff]
MinMaxLogicalProperties.min_max_absorption [lemma, in min_max_absorption]
MinMaxLogicalProperties.min_idempotent [abbreviation, in min_idempotent]
MinMaxLogicalProperties.Private_Rev.MRev.max [definition, in max]
MinMaxLogicalProperties.Private_Rev.MRev [module, in MinMaxLogicalProperties.Private_Rev.MRev]
MinMaxLogicalProperties.Private_Rev.MPRev [module, in MinMaxLogicalProperties.Private_Rev.MPRev]
MinMaxLogicalProperties.Private_Rev [module, in MinMaxLogicalProperties.Private_Rev]
MinMaxLogicalProperties.Private_Rev.MRev.max_r [definition, in max_r]
MinMaxLogicalProperties.Private_Rev.ORev [module, in MinMaxLogicalProperties.Private_Rev.ORev]
MinMaxLogicalProperties.Private_Rev.MRev.max_l [definition, in max_l]
MinMaxProperties [module, in MinMaxProperties]
MinMaxProperties.max_min_antimonotone [abbreviation, in max_min_antimonotone]
MinMaxProperties.max_r [definition, in max_r]
MinMaxProperties.max_monotone [abbreviation, in max_monotone]
MinMaxProperties.max_l [definition, in max_l]
MinMaxProperties.min_r [definition, in min_r]
MinMaxProperties.min_monotone [abbreviation, in min_monotone]
MinMaxProperties.min_l [definition, in min_l]
MinMaxProperties.min_max_antimonotone [abbreviation, in min_max_antimonotone]
MinMaxProperties.OT [module, in MinMaxProperties.OT]
minorant [abbreviation, in minorant]
MinRlist [definition, in MinRlist]
MinRlist_P2 [lemma, in MinRlist_P2]
MinRlist_P1 [lemma, in MinRlist_P1]
minus [definition, in minus]
Minus [library]
minus_Rgt [abbreviation, in minus_Rgt]
minus_plus [lemma, in minus_plus]
minus_le_compat_l [lemma, in minus_le_compat_l]
minus_fct [definition, in minus_fct]
minus_INR [lemma, in minus_INR]
minus_diag_reverse [lemma, in minus_diag_reverse]
minus_one [definition, in minus_one]
minus_le_compat_r [lemma, in minus_le_compat_r]
minus_Sn_m [lemma, in minus_Sn_m]
minus_diag [lemma, in minus_diag]
minus_sum [lemma, in minus_sum]
minus_Rge [abbreviation, in minus_Rge]
minus_n_n [abbreviation, in minus_n_n]
minus_plus_simpl_l_reverse [lemma, in minus_plus_simpl_l_reverse]
minus_n_O [lemma, in minus_n_O]
minus_IZR [lemma, in minus_IZR]
minus_neq_O [lemma, in minus_neq_O]
min_spec [definition, in min_spec]
min_case [definition, in min_case]
min_cv [lemma, in min_cv]
min_comm [definition, in min_comm]
min_SS [abbreviation, in min_SS]
min_case_strong [definition, in min_case_strong]
min_case2 [abbreviation, in min_case2]
min_r [definition, in min_r]
min_r [lemma, in min_r]
min_0_l [definition, in min_0_l]
min_assoc [definition, in min_assoc]
min_l [definition, in min_l]
min_l [lemma, in min_l]
min_maj [lemma, in min_maj]
min_inf [abbreviation, in min_inf]
min_glb [definition, in min_glb]
min_glb_r [definition, in min_glb_r]
min_glb_l [definition, in min_glb_l]
min_dec [definition, in min_dec]
min_ss [lemma, in min_ss]
min_idempotent [definition, in min_idempotent]
min_0_r [definition, in min_0_r]
mkC1 [constructor, in mkC1]
mkDifferential [constructor, in mkDifferential]
mkDifferential_D2 [constructor, in mkDifferential_D2]
mkfamily [constructor, in mkfamily]
mknegreal [constructor, in mknegreal]
mknonnegreal [constructor, in mknonnegreal]
mknonposreal [constructor, in mknonposreal]
mknonzeroreal [constructor, in mknonzeroreal]
mkposreal [constructor, in mkposreal]
mkposreal_lb_ub [definition, in mkposreal_lb_ub]
mkStepFun [constructor, in mkStepFun]
mk_zn2z_specs_karatsuba [instance, in mk_zn2z_specs_karatsuba]
mk_zn2z_specs [instance, in mk_zn2z_specs]
mk_zn2z_ops_karatsuba [instance, in mk_zn2z_ops_karatsuba]
mk_zn2z_ops [instance, in mk_zn2z_ops]
modulo [definition, in modulo]
modulo [definition, in modulo]
modulo [lemma, in modulo]
modulo_gt [definition, in modulo_gt]
mod_wwB [lemma, in mod_wwB]
mod_bound_pos [lemma, in mod_bound_pos]
mod_Zmod [lemma, in mod_Zmod]
MoreInt [module, in MoreInt]
MoreInt.EImax [constructor, in EImax]
MoreInt.EIminus [constructor, in EIminus]
MoreInt.EImult [constructor, in EImult]
MoreInt.EIopp [constructor, in EIopp]
MoreInt.EIplus [constructor, in EIplus]
MoreInt.EIraw [constructor, in EIraw]
MoreInt.EI0 [constructor, in EI0]
MoreInt.EI1 [constructor, in EI1]
MoreInt.EI2 [constructor, in EI2]
MoreInt.ei2i [definition, in ei2i]
MoreInt.EI3 [constructor, in EI3]
MoreInt.EPand [constructor, in EPand]
MoreInt.EPeq [constructor, in EPeq]
MoreInt.EPequiv [constructor, in EPequiv]
MoreInt.EPge [constructor, in EPge]
MoreInt.EPgt [constructor, in EPgt]
MoreInt.EPimpl [constructor, in EPimpl]
MoreInt.EPle [constructor, in EPle]
MoreInt.EPlt [constructor, in EPlt]
MoreInt.EPneg [constructor, in EPneg]
MoreInt.EPor [constructor, in EPor]
MoreInt.EPraw [constructor, in EPraw]
MoreInt.ep2p [definition, in ep2p]
MoreInt.ExprI [inductive, in ExprI]
MoreInt.ExprP [inductive, in ExprP]
MoreInt.ExprZ [inductive, in ExprZ]
MoreInt.EZmax [constructor, in EZmax]
MoreInt.EZminus [constructor, in EZminus]
MoreInt.EZmult [constructor, in EZmult]
MoreInt.EZofI [constructor, in EZofI]
MoreInt.EZopp [constructor, in EZopp]
MoreInt.EZplus [constructor, in EZplus]
MoreInt.EZraw [constructor, in EZraw]
MoreInt.ez2z [definition, in ez2z]
MoreInt.int [abbreviation, in int]
MoreInt.norm_ei [definition, in norm_ei]
MoreInt.norm_ep_correct2 [lemma, in norm_ep_correct2]
MoreInt.norm_ez_correct [lemma, in norm_ez_correct]
MoreInt.norm_ei_correct [lemma, in norm_ei_correct]
MoreInt.norm_ep_correct [lemma, in norm_ep_correct]
MoreInt.norm_ep [definition, in norm_ep]
MoreInt.norm_ez [definition, in norm_ez]
Morphisms [library]
Morphisms_Relations [library]
Morphisms_Prop [library]
MOT_to_OT [module, in MOT_to_OT]
MOT_to_OT.eq_dec [definition, in eq_dec]
MR [definition, in MR]
MSetAVL [library]
MSetDecide [library]
MSetEqProperties [library]
MSetFacts [library]
MSetGenTree [library]
MSetInterface [library]
MSetInterface_S_Ext [module, in MSetInterface_S_Ext]
MSetList [library]
MSetPositive [library]
MSetProperties [library]
MSetRBT [library]
MSetRemoveMin [module, in MSetRemoveMin]
MSetRemoveMin.remove_min_spec1 [axiom, in remove_min_spec1]
MSetRemoveMin.remove_min_spec2 [axiom, in remove_min_spec2]
MSetRemoveMin.remove_min [axiom, in remove_min]
MSets [library]
MSetToFiniteSet [library]
MSetWeakList [library]
mul [definition, in mul]
MulAdd [section, in MulAdd]
[| _ |] [notation, in ::'[|'_x_'|]']
[|| _ ||] [notation, in ::'[||'_x_'||]']
mult [definition, in mult]
Mult [library]
multiplicity [definition, in multiplicity]
multiplicity_NoDupA [lemma, in multiplicity_NoDupA]
multiplicity_InA_S [lemma, in multiplicity_InA_S]
multiplicity_In_S [lemma, in multiplicity_In_S]
multiplicity_NoDup [lemma, in multiplicity_NoDup]
multiplicity_InA_O [lemma, in multiplicity_InA_O]
multiplicity_InA [lemma, in multiplicity_InA]
multiplicity_eqA [instance, in multiplicity_eqA]
multiplicity_In_O [lemma, in multiplicity_In_O]
multiplicity_In [lemma, in multiplicity_In]
multiset [inductive, in multiset]
Multiset [library]
multiset_defs.eqA [variable, in eqA]
multiset_twist1 [lemma, in multiset_twist1]
multiset_defs [section, in multiset_defs]
multiset_twist2 [lemma, in multiset_twist2]
multiset_defs.eqA_equiv [variable, in eqA_equiv]
multiset_defs.Aeq_dec [variable, in Aeq_dec]
multiset_defs.A [variable, in A]
mult_lt_compat_r [lemma, in mult_lt_compat_r]
mult_minus_distr_r [lemma, in mult_minus_distr_r]
mult_IZR [lemma, in mult_IZR]
mult_add_ineq [lemma, in mult_add_ineq]
mult_add_ineq [lemma, in mult_add_ineq]
mult_real_fct [definition, in mult_real_fct]
mult_succ_l [lemma, in mult_succ_l]
mult_is_one [lemma, in mult_is_one]
mult_le_compat [lemma, in mult_le_compat]
mult_plus_distr_r [lemma, in mult_plus_distr_r]
mult_fct [definition, in mult_fct]
mult_n_Sm [lemma, in mult_n_Sm]
mult_add_ineq2 [lemma, in mult_add_ineq2]
mult_le_compat_r [lemma, in mult_le_compat_r]
mult_0_r [lemma, in mult_0_r]
mult_assoc_reverse [lemma, in mult_assoc_reverse]
mult_succ_r_reverse [abbreviation, in mult_succ_r_reverse]
mult_S_le_reg_l [lemma, in mult_S_le_reg_l]
mult_succ_r [lemma, in mult_succ_r]
mult_0_l [lemma, in mult_0_l]
mult_wwB [lemma, in mult_wwB]
mult_assoc [lemma, in mult_assoc]
mult_comm [lemma, in mult_comm]
mult_1_r [lemma, in mult_1_r]
mult_is_O [lemma, in mult_is_O]
mult_add_ineq3 [lemma, in mult_add_ineq3]
mult_le_compat_l [lemma, in mult_le_compat_l]
mult_1_l [lemma, in mult_1_l]
mult_O_le [lemma, in mult_O_le]
mult_lt_compat_l [lemma, in mult_lt_compat_l]
mult_plus_distr_l [lemma, in mult_plus_distr_l]
mult_tail_mult [lemma, in mult_tail_mult]
mult_INR [lemma, in mult_INR]
mult_n_O [lemma, in mult_n_O]
mult_S_lt_compat_l [lemma, in mult_S_lt_compat_l]
mult_minus_distr_l [lemma, in mult_minus_distr_l]
mult_acc [definition, in mult_acc]
mult_0_r_reverse [abbreviation, in mult_0_r_reverse]
mult_acc_aux [lemma, in mult_acc_aux]
mul_factor_gt_f [lemma, in mul_factor_gt_f]
mul_factor [definition, in mul_factor]
mul_c [definition, in mul_c]
mul_factor_gt [lemma, in mul_factor_gt]
mul_factor_wd [lemma, in mul_factor_wd]
mul_add [definition, in mul_add]
mul31 [definition, in mul31]
mul31c [definition, in mul31c]
munion [definition, in munion]
munion_perm_left [lemma, in munion_perm_left]
munion_rotate [lemma, in munion_rotate]
munion_comm [lemma, in munion_comm]
munion_empty_left [lemma, in munion_empty_left]
munion_ass [lemma, in munion_ass]
munion_empty_right [lemma, in munion_empty_right]
MVT [lemma, in MVT]
MVT [library]
MVT_cor2 [lemma, in MVT_cor2]
MVT_cor3 [lemma, in MVT_cor3]
MVT_cor1 [lemma, in MVT_cor1]