proposition: Lemma mult_is_complete_greater : transitive _ R -> (forall a, ~ R a a) -> forall l1 l2, trans_clos (multiset_extension_step R) l2 l1 -> mult l1 l2 = Greater_than.
proof: Proof. intros trans_R irrefl_R l1 l2 l2_lt_l1. generalize (remove_equiv_is_sound l1 l2); unfold mult; unfold A in *; case_eq (remove_equiv eq_bool l1 l2); intros k1 k2 H [l [P1 [P2 k1_disj_k2]]]. assert (lk2_lt_lk1 : trans_clos (multiset_extension_step R) (l ++ k2) (l ++ k1)). apply list_permut_trans_clos_multiset_extension_step_1 with l2; [assumption | idtac]. apply list_permut_trans_clos_multiset_extension_step_2 with l1; assumption. assert (Dummy := @mult_is_complete_greater_aux trans_R irrefl_R l _ _ k1_disj_k2 lk2_lt_lk1). unfold A in Dummy; rewrite Dummy; clear Dummy. revert lk2_lt_lk1; case k1; [idtac | intros _ _ _; apply eq_refl]. case k2; [idtac | intros _ _ _; apply eq_refl]. intro T; apply False_rect. apply (mult_irrefl trans_R irrefl_R T). Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)