monotonicity_theorems : thm list ref
# let LEX = define `(LEX(<<) [] l <=> F) /\ (LEX(<<) l [] <=> F) /\ (LEX(<<) (CONS h1 t1) (CONS h2 t2) <=> if h1 << h2 then LENGTH t1 = LENGTH t2 else (h1 = h2) /\ LEX(<<) t1 t2)`;;
# let LEX_LENGTH = prove (`!l1 l2 R. LEX(R) l1 l2 ==> (LENGTH l1 = LENGTH l2)`, REPEAT(LIST_INDUCT_TAC THEN SIMP_TAC[LEX]) THEN ASM_MESON_TAC[LENGTH]);;
# let MONO_LEX = prove (`(!x:A y:A. R x y ==> S x y) ==> LEX R x y ==> LEX S x y`, DISCH_TAC THEN MAP_EVERY (fun t -> SPEC_TAC(t,t)) [`x:A list`; `y:A list`] THEN REPEAT(LIST_INDUCT_TAC THEN REWRITE_TAC[LEX]) THEN ASM_MESON_TAC[LEX_LENGTH]);;
# monotonicity_theorems := MONO_LEX::(!monotonicity_theorems);;