proposition: Lemma mult_is_complete : transitive _ R -> (forall a, ~ R a a) -> forall l1 l2, match mult l1 l2 with | Uncomparable => ~ permut l1 l2 /\ ~trans_clos (multiset_extension_step R) l1 l2 /\ ~trans_clos (multiset_extension_step R) l2 l1 | _ => True end.
proof: Proof. intros trans_R irrefl_R l1 l2. generalize (mult_is_sound l1 l2) (@mult_is_complete_equiv l1 l2) (@mult_is_complete_greater trans_R irrefl_R l1 l2) (@mult_is_complete_less_than trans_R irrefl_R l1 l2). case (mult l1 l2); trivial. intros _ H1 H2 H3; repeat split; intro H. generalize (H1 H); discriminate. generalize (H3 H); discriminate. generalize (H2 H); discriminate. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)