What Isabelle library to reuse for expressing that some function is a linear order (on some set) -

in isabelle formalisation i'm dealing finite sets of natural numbers, , on these sets i'd consider functions have property of being linear order.

i see there several different formalisations of orders in library, i'm not sure 1 reuse. in cases functions of i'd check whether linear orders defined using library operators such < (less), in cases might defined more complex combinations of library functions.

i tried hol/library/order_relation, doesn't seem connected <; e.g. i'm unable have following lemma proved automatically:

lemma "linear_order_on {1::nat, 2} {(a::nat, b) . {a, b} ⊆ {1::nat, 2} ∧ < b}" 

(i'm sure there nicer ways of converting function relation, that's not main point here.)

if there ready-to-reuse library i'd appreciate if let me know. modelling in mathematically elegant way not of utmost importance me right now, i'm considering resort functions assign rational or real numbers natural numbers in sets, , using < on these rational/real numbers.

i don't know if there better theories use, lemma have given (still after fix) false (the given relation irreflexive while expected 1 should reflexive). here 2 versions correct:

lemma "linear_order_on {1::nat, 2} {(a::nat, b) . {a, b} ⊆ {1::nat, 2} ∧ ≤ b}"   unfolding linear_order_on_def partial_order_on_def preorder_on_def     refl_on_def total_on_def trans_def antisym_def   auto  lemma "strict_linear_order_on {1::nat, 2} {(a::nat, b) . {a, b} ⊆ {1::nat, 2} ∧ < b}"   unfolding strict_linear_order_on_def partial_order_on_def preorder_on_def     irrefl_def total_on_def trans_def antisym_def   auto