Theoremsdual, dual_left, dual_right, eq_of_ge_of_le, ne_of_lt_of_lt_int, ne_of_lt_of_lt_nat, strictAnti_iff_injective, dual, dual_left, dual_right, strictAntiOn_of_injOn, strictAnti_iff_injOn, exists_strictAnti, exists_strictMono, rel_of_forall_rel_succ_of_le, rel_of_forall_rel_succ_of_lt, foldl_monotone, foldl_strictMono, foldr_monotone, foldr_strictMono, dual, dual_left, dual_right, eq_of_ge_of_le, ne_of_lt_of_lt_int, ne_of_lt_of_lt_nat, strictMono_iff_injective, dual, dual_left, dual_right, strictMonoOn_iff_injOn, strictMonoOn_of_injOn, exists_strictAnti, exists_strictAnti', exists_strictMono, exists_strictMono', exists_strictMono_subsequence, pow_monotoneOn, pow_self_mono, pow_self_strictMonoOn, rel_of_forall_rel_succ_of_le, rel_of_forall_rel_succ_of_le_of_le, rel_of_forall_rel_succ_of_le_of_lt, rel_of_forall_rel_succ_of_lt, stabilises_of_monotone, cmp_map_eq, compares, dual, dual_left, dual_right, injective, isMax_of_apply, isMin_of_apply, ite, ite', le_iff_ge, lt_iff_gt, maximal_of_minimal_image, minimal_of_maximal_image, wellFoundedGT, wellFoundedLT, cmp_map_eq, compares, dual, dual_left, dual_right, eq_iff_eq, injOn, le_iff_ge, lt_iff_gt, add_le_nat, cmp_map_eq, compares, dual, dual_left, dual_right, injective, isMax_of_apply, isMin_of_apply, ite, ite', le_iff_le, lt_iff_lt, maximal_of_maximal_image, minimal_of_minimal_image, wellFoundedGT, wellFoundedLT, cmp_map_eq, compares, dual, dual_left, dual_right, eq_iff_eq, injOn, le_iff_le, lt_iff_lt, antitoneOn_comp_ofDual_iff, antitoneOn_dual_iff, antitoneOn_nat_Ici_of_succ_le, antitoneOn_toDual_comp_iff, antitone_add_nat_iff_antitoneOn_nat_Ici, antitone_add_nat_of_succ_le, antitone_comp_ofDual_iff, antitone_dual_iff, antitone_int_of_succ_le, antitone_nat_of_succ_le, antitone_toDual_comp_iff, converges_of_monotone_of_bounded, monotoneOn_comp_ofDual_iff, monotoneOn_dual_iff, monotoneOn_nat_Ici_of_le_succ, monotoneOn_toDual_comp_iff, monotone_add_nat_iff_monotoneOn_nat_Ici, monotone_add_nat_of_le_succ, monotone_comp_ofDual_iff, monotone_dual_iff, monotone_int_of_le_succ, monotone_nat_of_le_succ, monotone_toDual_comp_iff, not_monotone_not_antitone_iff_exists_le_le, not_monotone_not_antitone_iff_exists_lt_lt, strictAntiOn_comp_ofDual_iff, strictAntiOn_dual_iff, strictAntiOn_toDual_comp_iff, strictAnti_comp_ofDual_iff, strictAnti_dual_iff, strictAnti_int_of_succ_lt, strictAnti_nat_of_succ_lt, strictAnti_toDual_comp_iff, strictMonoOn_comp_ofDual_iff, strictMonoOn_dual_iff, strictMonoOn_toDual_comp_iff, strictMono_comp_ofDual_iff, strictMono_dual_iff, strictMono_int_of_lt_succ, strictMono_nat_of_lt_succ, strictMono_toDual_comp_iff | 137 |