fact: Parameter in_remove_list : forall l la, is_sorted la -> is_sorted l -> match remove_list la l with | None => forall rmv, ~ (permut (la ++ rmv) l) | Some rmv => permut (la ++ rmv) l end.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)