fact: Definition mult (l1 l2 : list A) : comp := match remove_equiv eq_bool l1 l2 with | (nil, nil) => Equivalent | (l1, l2) => match list_forall (fun t2 => list_exists (fun t1 => R_bool t2 t1) l1) l2 with | true => Greater_than | false => match list_forall (fun t1 => list_exists (fun t2 => R_bool t1 t2) l2) l1 with | true => Less_than | false => Uncomparable end end end.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)