fact: Fixpoint list_compare h k := match h,k with | nil x, nil y => compare x y | nil x, _ => Lt | _, nil x => Gt | u::h, v::k => lex (compare u v) (list_compare h k) end.
imports: Coq(Arith NArith List RelationClasses)