proposition: Lemma mult_is_complete_less_than : transitive _ R -> (forall a, ~ R a a) -> forall l1 l2, trans_clos (multiset_extension_step R) l1 l2 -> mult l1 l2 = Less_than.
proof: Proof. intros trans_R irrefl_R l1 l2 l1_lt_l2. generalize (multiset_closure trans_R l1_lt_l2). intros [ll [lc [P1 [P2 [ll_diff_nil [app_lt_cns disj]]]]]]. assert (cns_disj_app := disj irrefl_R); clear disj. assert (Q1 : permut l1 (lc ++ appendn ll)). apply permut_trans with (appendn ll ++ lc). assumption. apply permut_swapp; apply permut_refl. assert (Q2 : permut l2 (lc ++ consn ll)). apply permut_trans with (consn ll ++ lc). assumption. apply permut_swapp; apply permut_refl. assert (app_disj_cns : forall x : A, mem eq_A x (appendn ll) -> mem eq_A x (consn ll) -> False). intros x x_in_app x_in_cns; apply (cns_disj_app x); assumption. generalize (remove_equiv_is_complete _ _ _ Q1 Q2 app_disj_cns) (mult_is_sound l1 l2). unfold mult; unfold A in *; case (@remove_equiv DS1.A eq_bool l1 l2); simpl; intros k1 k2 [Q1' Q2']. assert (Dummy := mult_is_complete_greater_aux trans_R irrefl_R lc k2 k1). unfold A in Dummy; rewrite Dummy; clear Dummy. revert ll_diff_nil Q1' Q2'; case k1. case k2. case ll. intro ll_diff_nil; apply False_rect; apply ll_diff_nil; apply eq_refl. intros [a la] ll' _ _ Q2'; apply False_rect. assert (L := permut_length Q2'); discriminate. intros; apply eq_refl. clear k1; intros a1 k1 ll_diff_nil Q1' Q2'. case (list_forall (fun t2 : DS1.A => list_exists (fun t1 : DS1.A => R_bool t2 t1) (a1 :: k1)) k2). intro l2_lt_l1; apply False_rect. apply (@mult_irrefl trans_R irrefl_R l1). apply trans_clos_is_trans with l2; assumption. intros; apply eq_refl. intros x x_in_k2 x_in_k1; apply (cns_disj_app x). rewrite <- (mem_permut_mem x Q2'); assumption. rewrite <- (mem_permut_mem x Q1'); assumption. apply list_permut_trans_clos_multiset_extension_step_1 with l1. apply permut_trans with (k1 ++ lc). apply permut_trans with (appendn ll ++ lc). assumption. rewrite <- permut_app2; apply permut_sym; assumption. apply permut_swapp; apply permut_refl. apply list_permut_trans_clos_multiset_extension_step_2 with l2. apply permut_trans with (k2 ++ lc). apply permut_trans with (consn ll ++ lc). assumption. rewrite <- permut_app2; apply permut_sym; assumption. apply permut_swapp; apply permut_refl. assumption. Defined.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)