proposition: Lemma mult_is_complete_equiv : forall l1 l2, permut l1 l2 -> mult l1 l2 = Equivalent.
proof: Proof. intros l1 l2 P; assert (P1 : permut l1 (l1 ++ nil)). rewrite <- app_nil_end; apply permut_refl. assert (P2 : permut l2 (l1 ++ nil)). rewrite <- app_nil_end; apply permut_sym; assumption. assert (E : forall x : A, mem eq_A x nil -> mem eq_A x nil -> False). intros; contradiction. generalize (@remove_equiv_is_complete l1 l2 l1 nil nil P1 P2 E). unfold mult; unfold A in *; case (@remove_equiv DS1.A eq_bool l1 l2); intros k1 k2 [Q1 Q2]. simpl in Q1; rewrite (permut_nil Q1). simpl in Q2; rewrite (permut_nil Q2). apply eq_refl. Defined.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)