well_ord_iso_predE replaces not_well_ord_iso_pred
well_ord_iso_predE replaces not_well_ord_iso_pred

well_ord_iso_unique: eliminated a premise using well_ord_ord_iso

Proved well_ord_iso_pred_eq, ord_iso_image_pred, ord_iso_restrict_pred,
part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso, well_ord_ord_iso,
well_ord_iso_preserving, mono_map_is_fun, mono_map_is_inj, mono_map_trans,
mono_ord_isoI, well_ord_mono_ord_isoI, ord_iso_is_mono_map,
ord_iso_map_mono_map, ord_iso_map_ord_iso, domain_ord_iso_map_subset,
domain_ord_iso_map_cases, range_ord_iso_map_cases, well_ord_trichotomy

deleted bij_ss in favour of bij_inverse_ss

MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle,MerelyAPseudonym/isabelle