M (lemma)
Machin_2_3 [in Machin_2_3]
Machin_2_3_7 [in Machin_2_3_7]
Machin_4_5_239 [in Machin_4_5_239]
Majxy_cv_R0 [in Majxy_cv_R0]
maj_term4 [in maj_term4]
maj_Reste_cv_R0 [in maj_Reste_cv_R0]
maj_cv [in maj_cv]
maj_ss [in maj_ss]
maj_term1 [in maj_term1]
maj_by_pos [in maj_by_pos]
maj_min [in maj_min]
maj_term3 [in maj_term3]
maj_term2 [in maj_term2]
MakeListOrdering.cons_CompSpec [in cons_CompSpec]
MakeListOrdering.eq_cons [in eq_cons]
MakeRaw.add_spec' [in add_spec']
MakeRaw.add_spec [in add_spec]
MakeRaw.add_spec [in add_spec]
MakeRaw.add_spec [in add_spec]
MakeRaw.add_inf [in add_inf]
MakeRaw.append_ok [in append_ok]
MakeRaw.append_bb_match [in append_bb_match]
MakeRaw.append_spec [in append_spec]
MakeRaw.append_rr_match [in append_rr_match]
MakeRaw.cardinal_spec [in cardinal_spec]
MakeRaw.cardinal_spec [in cardinal_spec]
MakeRaw.choose_spec3 [in choose_spec3]
MakeRaw.compare_spec [in compare_spec]
MakeRaw.compare_spec_aux [in compare_spec_aux]
MakeRaw.delmin_spec [in delmin_spec]
MakeRaw.del_spec [in del_spec]
MakeRaw.diff_spec [in diff_spec]
MakeRaw.diff_spec [in diff_spec]
MakeRaw.diff_spec [in diff_spec]
MakeRaw.diff_inf [in diff_inf]
MakeRaw.diff_list_spec [in diff_list_spec]
MakeRaw.diff_list_ok [in diff_list_ok]
MakeRaw.elements_spec2w [in elements_spec2w]
MakeRaw.elements_spec2w [in elements_spec2w]
MakeRaw.elements_spec2 [in elements_spec2]
MakeRaw.elements_spec1 [in elements_spec1]
MakeRaw.elements_spec1 [in elements_spec1]
MakeRaw.empty_spec [in empty_spec]
MakeRaw.empty_spec [in empty_spec]
MakeRaw.empty_ok [in empty_ok]
MakeRaw.equal_spec [in equal_spec]
MakeRaw.equal_spec [in equal_spec]
MakeRaw.exists_spec [in exists_spec]
MakeRaw.exists_spec [in exists_spec]
MakeRaw.filter_aux_elements [in filter_aux_elements]
MakeRaw.filter_spec [in filter_spec]
MakeRaw.filter_spec [in filter_spec]
MakeRaw.filter_spec [in filter_spec]
MakeRaw.filter_inf [in filter_inf]
MakeRaw.filter_app [in filter_app]
MakeRaw.filter_spec' [in filter_spec']
MakeRaw.filter_elements [in filter_elements]
MakeRaw.fold_add_spec [in fold_add_spec]
MakeRaw.fold_remove_spec [in fold_remove_spec]
MakeRaw.fold_spec [in fold_spec]
MakeRaw.fold_spec [in fold_spec]
MakeRaw.for_all_spec [in for_all_spec]
MakeRaw.for_all_spec [in for_all_spec]
MakeRaw.inf_iff [in inf_iff]
MakeRaw.ins_spec [in ins_spec]
MakeRaw.inter_inf [in inter_inf]
MakeRaw.inter_spec [in inter_spec]
MakeRaw.inter_spec [in inter_spec]
MakeRaw.inter_spec [in inter_spec]
MakeRaw.inter_list_ok [in inter_list_ok]
MakeRaw.inter_list_spec [in inter_list_spec]
MakeRaw.INV_lt [in INV_lt]
MakeRaw.INV_eq [in INV_eq]
MakeRaw.INV_rev [in INV_rev]
MakeRaw.INV_drop [in INV_drop]
MakeRaw.INV_sym [in INV_sym]
MakeRaw.INV_init [in INV_init]
MakeRaw.In_compat [in In_compat]
MakeRaw.isok_iff [in isok_iff]
MakeRaw.isok_iff [in isok_iff]
MakeRaw.is_empty_spec [in is_empty_spec]
MakeRaw.is_empty_spec [in is_empty_spec]
MakeRaw.lbalS_spec [in lbalS_spec]
MakeRaw.lbalS_match [in lbalS_match]
MakeRaw.lbal_match [in lbal_match]
MakeRaw.lbal_spec [in lbal_spec]
MakeRaw.linear_diff_spec [in linear_diff_spec]
MakeRaw.linear_inter_spec [in linear_inter_spec]
MakeRaw.linear_union_spec [in linear_union_spec]
MakeRaw.makeBlack_spec [in makeBlack_spec]
MakeRaw.makeRed_spec [in makeRed_spec]
MakeRaw.max_elt_spec3 [in max_elt_spec3]
MakeRaw.max_elt_spec2 [in max_elt_spec2]
MakeRaw.max_elt_spec1 [in max_elt_spec1]
MakeRaw.mem_spec [in mem_spec]
MakeRaw.mem_spec [in mem_spec]
MakeRaw.min_elt_spec2 [in min_elt_spec2]
MakeRaw.min_elt_spec3 [in min_elt_spec3]
MakeRaw.min_elt_spec1 [in min_elt_spec1]
MakeRaw.partition_spec2 [in partition_spec2]
MakeRaw.partition_spec2 [in partition_spec2]
MakeRaw.partition_spec2 [in partition_spec2]
MakeRaw.partition_spec1 [in partition_spec1]
MakeRaw.partition_spec1 [in partition_spec1]
MakeRaw.partition_spec1 [in partition_spec1]
MakeRaw.partition_ok2' [in partition_ok2']
MakeRaw.partition_ok1' [in partition_ok1']
MakeRaw.partition_aux_spec [in partition_aux_spec]
MakeRaw.partition_spec [in partition_spec]
MakeRaw.partition_inf1 [in partition_inf1]
MakeRaw.partition_inf2 [in partition_inf2]
MakeRaw.plength_aux_spec [in plength_aux_spec]
MakeRaw.plength_spec [in plength_spec]
MakeRaw.rbalS_match [in rbalS_match]
MakeRaw.rbalS_spec [in rbalS_spec]
MakeRaw.rbal_spec [in rbal_spec]
MakeRaw.rbal_match [in rbal_match]
MakeRaw.rbal'_spec [in rbal'_spec]
MakeRaw.rbal'_match [in rbal'_match]
MakeRaw.remove_min_spec1 [in remove_min_spec1]
MakeRaw.remove_spec [in remove_spec]
MakeRaw.remove_spec [in remove_spec]
MakeRaw.remove_spec [in remove_spec]
MakeRaw.remove_inf [in remove_inf]
MakeRaw.remove_min_ok [in remove_min_ok]
MakeRaw.remove_min_spec2 [in remove_min_spec2]
MakeRaw.rmatch [in rmatch]
MakeRaw.rrmatch [in rrmatch]
MakeRaw.rrmatch' [in rrmatch']
MakeRaw.singleton_spec [in singleton_spec]
MakeRaw.singleton_spec [in singleton_spec]
MakeRaw.singleton_spec [in singleton_spec]
MakeRaw.singleton_ok [in singleton_ok]
MakeRaw.subset_spec [in subset_spec]
MakeRaw.subset_spec [in subset_spec]
MakeRaw.treeify_one_spec [in treeify_one_spec]
MakeRaw.treeify_elements [in treeify_elements]
MakeRaw.treeify_ok [in treeify_ok]
MakeRaw.treeify_cont_spec [in treeify_cont_spec]
MakeRaw.treeify_aux_spec [in treeify_aux_spec]
MakeRaw.treeify_zero_spec [in treeify_zero_spec]
MakeRaw.treeify_spec [in treeify_spec]
MakeRaw.union_list_ok [in union_list_ok]
MakeRaw.union_spec [in union_spec]
MakeRaw.union_spec [in union_spec]
MakeRaw.union_spec [in union_spec]
MakeRaw.union_spec' [in union_spec']
MakeRaw.union_inf [in union_inf]
MakeRaw.union_list_spec [in union_list_spec]
MakeSetOrdering.lt_empty_r [in lt_empty_r]
MakeSetOrdering.lt_empty_l [in lt_empty_l]
MakeSetOrdering.lt_add_lt [in lt_add_lt]
MakeSetOrdering.lt_add_eq [in lt_add_eq]
MakeWithLeibniz.eq_leibniz [in eq_leibniz]
MakeWithLeibniz.eq_leibniz_list [in eq_leibniz_list]
Make_ord.eq_refl [in eq_refl]
Make_ord.eq_1 [in eq_1]
make_kzop [in make_kzop]
make_zop [in make_zop]
Make_ord.eq_equal [in eq_equal]
make_new_approximant [in make_new_approximant]
Make_ord.eq_2 [in eq_2]
Make_ord.eq_sym [in eq_sym]
Make_ord.lt_not_eq [in lt_not_eq]
Make_ord.lt_trans [in lt_trans]
Make_ord.eq_trans [in eq_trans]
Make.add_1 [in add_1]
Make.add_1 [in add_1]
Make.add_2 [in add_2]
Make.add_2 [in add_2]
Make.add_3 [in add_3]
Make.add_3 [in add_3]
Make.add_fold [in add_fold]
Make.cardinal_1 [in cardinal_1]
Make.cardinal_1 [in cardinal_1]
Make.compare_fold [in compare_fold]
Make.destr_t [in destr_t]
Make.digits_dom_op_incr [in digits_dom_op_incr]
Make.digits_level [in digits_level]
Make.digits_dom_op [in digits_dom_op]
Make.digits_nmake [in digits_nmake]
Make.digits_make_op_0 [in digits_make_op_0]
Make.digits_fold [in digits_fold]
Make.digits_dom_op_nmake [in digits_dom_op_nmake]
Make.digits_make_op [in digits_make_op]
Make.digits_nmake_S [in digits_nmake_S]
Make.div_gt_fold [in div_gt_fold]
Make.div_pow2_bound [in div_pow2_bound]
Make.double_size_fold [in double_size_fold]
Make.double_size_level [in double_size_level]
Make.elements_3w [in elements_3w]
Make.elements_3w [in elements_3w]
Make.elements_3 [in elements_3]
Make.elements_1 [in elements_1]
Make.elements_1 [in elements_1]
Make.elements_2 [in elements_2]
Make.elements_2 [in elements_2]
Make.empty_1 [in empty_1]
Make.empty_1 [in empty_1]
Make.equal_2 [in equal_2]
Make.equal_2 [in equal_2]
Make.equal_1 [in equal_1]
Make.equal_1 [in equal_1]
Make.even_fold [in even_fold]
Make.find_2 [in find_2]
Make.find_2 [in find_2]
Make.find_1 [in find_1]
Make.find_1 [in find_1]
Make.fold_1 [in fold_1]
Make.fold_1 [in fold_1]
Make.head0_fold [in head0_fold]
Make.head0_zdigits [in head0_zdigits]
Make.is_empty_1 [in is_empty_1]
Make.is_empty_1 [in is_empty_1]
Make.is_empty_2 [in is_empty_2]
Make.is_empty_2 [in is_empty_2]
Make.iter_mk_t [in iter_mk_t]
Make.log2_fold [in log2_fold]
Make.log2_digits_head0 [in log2_digits_head0]
Make.make_op_omake [in make_op_omake]
Make.make_op_S [in make_op_S]
Make.mapi_2 [in mapi_2]
Make.mapi_2 [in mapi_2]
Make.mapi_1 [in mapi_1]
Make.mapi_1 [in mapi_1]
Make.MapsTo_1 [in MapsTo_1]
Make.MapsTo_1 [in MapsTo_1]
Make.map_1 [in map_1]
Make.map_1 [in map_1]
Make.map_2 [in map_2]
Make.map_2 [in map_2]
Make.map2_2 [in map2_2]
Make.map2_2 [in map2_2]
Make.map2_1 [in map2_1]
Make.map2_1 [in map2_1]
Make.mem_1 [in mem_1]
Make.mem_1 [in mem_1]
Make.mem_2 [in mem_2]
Make.mem_2 [in mem_2]
Make.mk_t_S_level [in mk_t_S_level]
Make.mod_gt_fold [in mod_gt_fold]
Make.mul_fold [in mul_fold]
Make.Ndigits_fold [in Ndigits_fold]
Make.nmake_op_S [in nmake_op_S]
Make.nmake_WW [in nmake_WW]
Make.nmake_double [in nmake_double]
Make.N_to_Z_pos [in N_to_Z_pos]
Make.pheight_correct [in pheight_correct]
Make.plus_t_equiv [in plus_t_equiv]
Make.pow2_pos_minus_1 [in pow2_pos_minus_1]
Make.pred_fold [in pred_fold]
Make.reduce_equiv [in reduce_equiv]
Make.remove_min_spec1 [in remove_min_spec1]
Make.remove_2 [in remove_2]
Make.remove_2 [in remove_2]
Make.remove_min_spec2 [in remove_min_spec2]
Make.remove_1 [in remove_1]
Make.remove_1 [in remove_1]
Make.remove_3 [in remove_3]
Make.remove_3 [in remove_3]
Make.shiftr_fold [in shiftr_fold]
Make.spec_double_size_head0_pos [in spec_double_size_head0_pos]
Make.spec_oppc_bis [in spec_oppc_bis]
Make.spec_shiftl_aux_body [in spec_shiftl_aux_body]
Make.spec_norm_pos [in spec_norm_pos]
Make.spec_switch [in spec_switch]
Make.spec_comparec [in spec_comparec]
Make.spec_of_pos [in spec_of_pos]
Make.spec_of_Z [in spec_of_Z]
Make.spec_ltb [in spec_ltb]
Make.spec_ltb [in spec_ltb]
Make.spec_shiftl [in spec_shiftl]
Make.spec_shiftl [in spec_shiftl]
Make.spec_log2_pos [in spec_log2_pos]
Make.spec_of_Q [in spec_of_Q]
Make.spec_pos [in spec_pos]
Make.spec_pred [in spec_pred]
Make.spec_pred [in spec_pred]
Make.spec_sub_norm [in spec_sub_norm]
Make.spec_norm [in spec_norm]
Make.spec_head00 [in spec_head00]
Make.spec_div_normc [in spec_div_normc]
Make.spec_sub_normc_bis [in spec_sub_normc_bis]
Make.spec_plus_t [in spec_plus_t]
Make.spec_shiftr_pow2 [in spec_shiftr_pow2]
Make.spec_max [in spec_max]
Make.spec_max [in spec_max]
Make.spec_max [in spec_max]
Make.spec_mk_t [in spec_mk_t]
Make.spec_power_posc [in spec_power_posc]
Make.spec_sgn [in spec_sgn]
Make.spec_leb [in spec_leb]
Make.spec_leb [in spec_leb]
Make.spec_add [in spec_add]
Make.spec_add [in spec_add]
Make.spec_add [in spec_add]
Make.spec_sqrt_aux [in spec_sqrt_aux]
Make.spec_log2_0 [in spec_log2_0]
Make.spec_land [in spec_land]
Make.spec_land [in spec_land]
Make.spec_oppc [in spec_oppc]
Make.spec_double_size [in spec_double_size]
Make.spec_odd [in spec_odd]
Make.spec_odd [in spec_odd]
Make.spec_digits [in spec_digits]
Make.spec_shiftr [in spec_shiftr]
Make.spec_shiftr [in spec_shiftr]
Make.spec_inv_normc_bis [in spec_inv_normc_bis]
Make.spec_reduce_n [in spec_reduce_n]
Make.spec_add_normc [in spec_add_normc]
Make.spec_div_norm [in spec_div_norm]
Make.spec_same_level_dep [in spec_same_level_dep]
Make.spec_2 [in spec_2]
Make.spec_2 [in spec_2]
Make.spec_div_normc_bis [in spec_div_normc_bis]
Make.spec_even_aux [in spec_even_aux]
Make.spec_eval_size [in spec_eval_size]
Make.spec_mk_t_w [in spec_mk_t_w]
Make.spec_mod_gt [in spec_mod_gt]
Make.spec_div2 [in spec_div2]
Make.spec_div2 [in spec_div2]
Make.spec_wn_mul [in spec_wn_mul]
Make.spec_shiftl_aux [in spec_shiftl_aux]
Make.spec_double_size_head0 [in spec_double_size_head0]
Make.spec_mul [in spec_mul]
Make.spec_mul [in spec_mul]
Make.spec_mul [in spec_mul]
Make.spec_mul_normc_bis [in spec_mul_normc_bis]
Make.spec_inv [in spec_inv]
Make.spec_head0 [in spec_head0]
Make.spec_testbit [in spec_testbit]
Make.spec_testbit [in spec_testbit]
Make.spec_tail00 [in spec_tail00]
Make.spec_rem [in spec_rem]
Make.spec_double_size_digits [in spec_double_size_digits]
Make.spec_divc [in spec_divc]
Make.spec_plus_t' [in spec_plus_t']
Make.spec_power_pos [in spec_power_pos]
Make.spec_extend_size [in spec_extend_size]
Make.spec_1 [in spec_1]
Make.spec_1 [in spec_1]
Make.spec_1 [in spec_1]
Make.spec_mulc [in spec_mulc]
Make.spec_quot [in spec_quot]
Make.spec_irred [in spec_irred]
Make.spec_add_normc_bis [in spec_add_normc_bis]
Make.spec_m1 [in spec_m1]
Make.spec_m1 [in spec_m1]
Make.spec_eqb [in spec_eqb]
Make.spec_eqb [in spec_eqb]
Make.spec_mul_norm [in spec_mul_norm]
Make.spec_tail0 [in spec_tail0]
Make.spec_lxor [in spec_lxor]
Make.spec_lxor [in spec_lxor]
Make.spec_irred_zero [in spec_irred_zero]
Make.spec_squarec [in spec_squarec]
Make.spec_modulo [in spec_modulo]
Make.spec_modulo [in spec_modulo]
Make.spec_zeron [in spec_zeron]
Make.spec_extend [in spec_extend]
Make.spec_unsafe_shiftl [in spec_unsafe_shiftl]
Make.spec_compare [in spec_compare]
Make.spec_compare [in spec_compare]
Make.spec_compare [in spec_compare]
Make.spec_muln [in spec_muln]
Make.spec_subc [in spec_subc]
Make.spec_iter [in spec_iter]
Make.spec_same_level [in spec_same_level]
Make.spec_pow [in spec_pow]
Make.spec_pow [in spec_pow]
Make.spec_add_norm [in spec_add_norm]
Make.spec_mul_norm_Qz_Qq [in spec_mul_norm_Qz_Qq]
Make.spec_even [in spec_even]
Make.spec_even [in spec_even]
Make.spec_ldiff [in spec_ldiff]
Make.spec_ldiff [in spec_ldiff]
Make.spec_mul_add_n1 [in spec_mul_add_n1]
Make.spec_mk_t_w' [in spec_mk_t_w']
Make.spec_mul_normc [in spec_mul_normc]
Make.spec_div [in spec_div]
Make.spec_div [in spec_div]
Make.spec_div_eucl [in spec_div_eucl]
Make.spec_div_eucl [in spec_div_eucl]
Make.spec_pow_pos [in spec_pow_pos]
Make.spec_pow_pos [in spec_pow_pos]
Make.spec_iter_sym [in spec_iter_sym]
Make.spec_pred0 [in spec_pred0]
Make.spec_lor [in spec_lor]
Make.spec_lor [in spec_lor]
Make.spec_eq_bool [in spec_eq_bool]
Make.spec_sub [in spec_sub]
Make.spec_sub [in spec_sub]
Make.spec_sub [in spec_sub]
Make.spec_mk_t_S [in spec_mk_t_S]
Make.spec_succ [in spec_succ]
Make.spec_succ [in spec_succ]
Make.spec_unsafe_shiftl_aux [in spec_unsafe_shiftl_aux]
Make.spec_gcd_gt [in spec_gcd_gt]
Make.spec_succ_t [in spec_succ_t]
Make.spec_abs [in spec_abs]
Make.spec_same_level_0 [in spec_same_level_0]
Make.spec_div_gt_aux [in spec_div_gt_aux]
Make.spec_power [in spec_power]
Make.spec_sub_pos [in spec_sub_pos]
Make.spec_power_norm [in spec_power_norm]
Make.spec_sqrt [in spec_sqrt]
Make.spec_sqrt [in spec_sqrt]
Make.spec_shiftl_pow2 [in spec_shiftl_pow2]
Make.spec_sub_normc [in spec_sub_normc]
Make.spec_norm_pos_pos [in spec_norm_pos_pos]
Make.spec_norm_denum [in spec_norm_denum]
Make.spec_inv_normc [in spec_inv_normc]
Make.spec_min [in spec_min]
Make.spec_min [in spec_min]
Make.spec_min [in spec_min]
Make.spec_opp [in spec_opp]
Make.spec_opp [in spec_opp]
Make.spec_log2 [in spec_log2]
Make.spec_log2 [in spec_log2]
Make.spec_gcd [in spec_gcd]
Make.spec_gcd [in spec_gcd]
Make.spec_reduce [in spec_reduce]
Make.spec_inv_norm [in spec_inv_norm]
Make.spec_pred_pos [in spec_pred_pos]
Make.spec_pow_N [in spec_pow_N]
Make.spec_pow_N [in spec_pow_N]
Make.spec_square [in spec_square]
Make.spec_square [in spec_square]
Make.spec_square [in spec_square]
Make.spec_red_t [in spec_red_t]
Make.spec_Ndigits [in spec_Ndigits]
Make.spec_get_endn [in spec_get_endn]
Make.spec_addc [in spec_addc]
Make.spec_invc [in spec_invc]
Make.spec_of_Qc [in spec_of_Qc]
Make.spec_sub0 [in spec_sub0]
Make.spec_of_N [in spec_of_N]
Make.spec_0 [in spec_0]
Make.spec_0 [in spec_0]
Make.spec_0 [in spec_0]
Make.spec_red [in spec_red]
Make.spec_div_gt [in spec_div_gt]
Make.sqrt_fold [in sqrt_fold]
Make.square_fold [in square_fold]
Make.strong_spec_of_Q [in strong_spec_of_Q]
Make.strong_spec_red [in strong_spec_red]
Make.strong_spec_of_Qc [in strong_spec_of_Qc]
Make.strong_spec_check_int [in strong_spec_check_int]
Make.strong_spec_irred [in strong_spec_irred]
Make.strong_spec_opp [in strong_spec_opp]
Make.strong_spec_norm [in strong_spec_norm]
Make.sub_fold [in sub_fold]
Make.succ_pred_t [in succ_pred_t]
Make.succ_fold [in succ_fold]
Make.tail0_fold [in tail0_fold]
Make.unsafe_shiftl_fold [in unsafe_shiftl_fold]
Make.Zlnot_alt3 [in Zlnot_alt3]
Make.Zlnot_alt2 [in Zlnot_alt2]
Make.Zlnot_alt1 [in Zlnot_alt1]
Make.zn2z_map_id [in zn2z_map_id]
Make.Zspec_gcd_gt_aux [in Zspec_gcd_gt_aux]
Make.Zspec_gcd_gt_body [in Zspec_gcd_gt_body]
map_eq_nil [in map_eq_nil]
map_nth [in map_nth]
map_length [in map_length]
map_rev [in map_rev]
map_app [in map_app]
map_id [in map_id]
map_ext [in map_ext]
map_nth_error [in map_nth_error]
map_map [in map_map]
match_eq_rewrite [in match_eq_rewrite]
MaxLogicalProperties.le_max_l [in le_max_l]
MaxLogicalProperties.le_max_r [in le_max_r]
MaxLogicalProperties.max_le_compat_l [in max_le_compat_l]
MaxLogicalProperties.max_r_iff [in max_r_iff]
MaxLogicalProperties.max_unicity [in max_unicity]
MaxLogicalProperties.max_lub_iff [in max_lub_iff]
MaxLogicalProperties.max_id [in max_id]
MaxLogicalProperties.max_comm [in max_comm]
MaxLogicalProperties.max_le [in max_le]
MaxLogicalProperties.max_le_iff [in max_le_iff]
MaxLogicalProperties.max_lub_lt_iff [in max_lub_lt_iff]
MaxLogicalProperties.max_lub_lt [in max_lub_lt]
MaxLogicalProperties.max_lub_r [in max_lub_r]
MaxLogicalProperties.max_spec [in max_spec]
MaxLogicalProperties.max_spec_le [in max_spec_le]
MaxLogicalProperties.max_lt_iff [in max_lt_iff]
MaxLogicalProperties.max_le_compat_r [in max_le_compat_r]
MaxLogicalProperties.max_lub_l [in max_lub_l]
MaxLogicalProperties.max_le_compat [in max_le_compat]
MaxLogicalProperties.max_mono [in max_mono]
MaxLogicalProperties.max_lub [in max_lub]
MaxLogicalProperties.max_l_iff [in max_l_iff]
MaxLogicalProperties.max_assoc [in max_assoc]
MaxLogicalProperties.max_unicity_ext [in max_unicity_ext]
maxN [in maxN]
MaxRlist_P1 [in MaxRlist_P1]
MaxRlist_P2 [in MaxRlist_P2]
max_r [in max_r]
max_l [in max_l]
measure_wf [in measure_wf]
memo_get_correct [in memo_get_correct]
meq_congr [in meq_congr]
meq_right [in meq_right]
meq_refl [in meq_refl]
meq_trans [in meq_trans]
meq_left [in meq_left]
meq_sym [in meq_sym]
meq_singleton [in meq_singleton]
merge [in merge]
MinMaxDecProperties.max_dec [in max_dec]
MinMaxDecProperties.max_case_strong [in max_case_strong]
MinMaxDecProperties.max_case [in max_case]
MinMaxDecProperties.min_case [in min_case]
MinMaxDecProperties.min_case_strong [in min_case_strong]
MinMaxDecProperties.min_dec [in min_dec]
MinMaxLogicalProperties.le_min_l [in le_min_l]
MinMaxLogicalProperties.le_min_r [in le_min_r]
MinMaxLogicalProperties.max_min_antimono [in max_min_antimono]
MinMaxLogicalProperties.max_min_absorption [in max_min_absorption]
MinMaxLogicalProperties.max_min_modular [in max_min_modular]
MinMaxLogicalProperties.max_min_distr [in max_min_distr]
MinMaxLogicalProperties.max_min_disassoc [in max_min_disassoc]
MinMaxLogicalProperties.min_spec [in min_spec]
MinMaxLogicalProperties.min_comm [in min_comm]
MinMaxLogicalProperties.min_max_modular [in min_max_modular]
MinMaxLogicalProperties.min_le_compat_r [in min_le_compat_r]
MinMaxLogicalProperties.min_le_compat [in min_le_compat]
MinMaxLogicalProperties.min_r_iff [in min_r_iff]
MinMaxLogicalProperties.min_lt_iff [in min_lt_iff]
MinMaxLogicalProperties.min_mono [in min_mono]
MinMaxLogicalProperties.min_le [in min_le]
MinMaxLogicalProperties.min_max_antimono [in min_max_antimono]
MinMaxLogicalProperties.min_spec_le [in min_spec_le]
MinMaxLogicalProperties.min_le_iff [in min_le_iff]
MinMaxLogicalProperties.min_unicity [in min_unicity]
MinMaxLogicalProperties.min_assoc [in min_assoc]
MinMaxLogicalProperties.min_glb_lt_iff [in min_glb_lt_iff]
MinMaxLogicalProperties.min_glb_iff [in min_glb_iff]
MinMaxLogicalProperties.min_le_compat_l [in min_le_compat_l]
MinMaxLogicalProperties.min_glb [in min_glb]
MinMaxLogicalProperties.min_glb_r [in min_glb_r]
MinMaxLogicalProperties.min_glb_l [in min_glb_l]
MinMaxLogicalProperties.min_unicity_ext [in min_unicity_ext]
MinMaxLogicalProperties.min_glb_lt [in min_glb_lt]
MinMaxLogicalProperties.min_id [in min_id]
MinMaxLogicalProperties.min_max_distr [in min_max_distr]
MinMaxLogicalProperties.min_l_iff [in min_l_iff]
MinMaxLogicalProperties.min_max_absorption [in min_max_absorption]
MinRlist_P2 [in MinRlist_P2]
MinRlist_P1 [in MinRlist_P1]
minus_plus [in minus_plus]
minus_le_compat_l [in minus_le_compat_l]
minus_INR [in minus_INR]
minus_diag_reverse [in minus_diag_reverse]
minus_le_compat_r [in minus_le_compat_r]
minus_Sn_m [in minus_Sn_m]
minus_diag [in minus_diag]
minus_sum [in minus_sum]
minus_plus_simpl_l_reverse [in minus_plus_simpl_l_reverse]
minus_n_O [in minus_n_O]
minus_IZR [in minus_IZR]
minus_neq_O [in minus_neq_O]
min_cv [in min_cv]
min_r [in min_r]
min_l [in min_l]
min_maj [in min_maj]
min_ss [in min_ss]
modulo [in modulo]
mod_wwB [in mod_wwB]
mod_bound_pos [in mod_bound_pos]
mod_Zmod [in mod_Zmod]
MoreInt.norm_ep_correct2 [in norm_ep_correct2]
MoreInt.norm_ez_correct [in norm_ez_correct]
MoreInt.norm_ei_correct [in norm_ei_correct]
MoreInt.norm_ep_correct [in norm_ep_correct]
multiplicity_NoDupA [in multiplicity_NoDupA]
multiplicity_InA_S [in multiplicity_InA_S]
multiplicity_In_S [in multiplicity_In_S]
multiplicity_NoDup [in multiplicity_NoDup]
multiplicity_InA_O [in multiplicity_InA_O]
multiplicity_InA [in multiplicity_InA]
multiplicity_In_O [in multiplicity_In_O]
multiplicity_In [in multiplicity_In]
multiset_twist1 [in multiset_twist1]
multiset_twist2 [in multiset_twist2]
mult_lt_compat_r [in mult_lt_compat_r]
mult_minus_distr_r [in mult_minus_distr_r]
mult_IZR [in mult_IZR]
mult_add_ineq [in mult_add_ineq]
mult_add_ineq [in mult_add_ineq]
mult_succ_l [in mult_succ_l]
mult_is_one [in mult_is_one]
mult_le_compat [in mult_le_compat]
mult_plus_distr_r [in mult_plus_distr_r]
mult_n_Sm [in mult_n_Sm]
mult_add_ineq2 [in mult_add_ineq2]
mult_le_compat_r [in mult_le_compat_r]
mult_0_r [in mult_0_r]
mult_assoc_reverse [in mult_assoc_reverse]
mult_S_le_reg_l [in mult_S_le_reg_l]
mult_succ_r [in mult_succ_r]
mult_0_l [in mult_0_l]
mult_wwB [in mult_wwB]
mult_assoc [in mult_assoc]
mult_comm [in mult_comm]
mult_1_r [in mult_1_r]
mult_is_O [in mult_is_O]
mult_add_ineq3 [in mult_add_ineq3]
mult_le_compat_l [in mult_le_compat_l]
mult_1_l [in mult_1_l]
mult_O_le [in mult_O_le]
mult_lt_compat_l [in mult_lt_compat_l]
mult_plus_distr_l [in mult_plus_distr_l]
mult_tail_mult [in mult_tail_mult]
mult_INR [in mult_INR]
mult_n_O [in mult_n_O]
mult_S_lt_compat_l [in mult_S_lt_compat_l]
mult_minus_distr_l [in mult_minus_distr_l]
mult_acc_aux [in mult_acc_aux]
mul_factor_gt_f [in mul_factor_gt_f]
mul_factor_gt [in mul_factor_gt]
mul_factor_wd [in mul_factor_wd]
munion_perm_left [in munion_perm_left]
munion_rotate [in munion_rotate]
munion_comm [in munion_comm]
munion_empty_left [in munion_empty_left]
munion_ass [in munion_ass]
munion_empty_right [in munion_empty_right]
MVT [in MVT]
MVT_cor2 [in MVT_cor2]
MVT_cor3 [in MVT_cor3]
MVT_cor1 [in MVT_cor1]