proposition: Lemma mult_is_complete_greater_aux : transitive _ R -> (forall a, ~ R a a) -> forall l l1 l2, (forall a, mem eq_A a l1 -> mem eq_A a l2 -> False) -> trans_clos (multiset_extension_step R) (l ++ l2) (l ++ l1) -> (list_forall (fun t2 => list_exists (fun t1 => R_bool t2 t1) l1) l2) = true.
proof: Proof. intros trans_R irrefl_R l l1 l2 l2_disj_l1 ll2_lt_ll1. assert (l2_lt_l1 := remove_context_trans_clos_multiset_extension_step_app1 trans_R irrefl_R l2 l1 l ll2_lt_ll1). clear l ll2_lt_ll1. generalize (multiset_closure trans_R l2_lt_l1). intros [ll [lc [P2 [P1 [ll_diff_nil [app_lt_cns cns_disj_app]]]]]]. generalize (cns_disj_app irrefl_R); clear cns_disj_app; intro cns_disj_app. assert (lc_eq_nil : lc = nil). revert P2 P1 cns_disj_app. case lc; clear lc; [intros _ _ _; apply eq_refl | intros c lc P2 P1 cns_disj_app]. apply False_rect. apply (l2_disj_l1 c). rewrite (mem_permut_mem c P1); rewrite <- mem_or_app; right; left; apply (equiv_refl _ _ eq_proof). rewrite (mem_permut_mem c P2); rewrite <- mem_or_app; right; left; apply (equiv_refl _ _ eq_proof). subst lc; rewrite <- app_nil_end in P1; rewrite <- app_nil_end in P2. assert (Compat : forall ta ta' tb tb' : A, eq_A ta tb -> eq_A ta' tb' -> R_bool ta ta' = R_bool tb tb'). unfold eq_A; intros a a' b b' a_eq_a' b_eq_b'; subst; apply eq_refl. rewrite (permut_list_forall_exists R_bool R_bool Compat P2 P1); clear Compat cns_disj_app P1 P2 ll_diff_nil; induction ll as [ | [a la] ll]; simpl; trivial. rewrite list_forall_app; rewrite Bool.andb_true_iff; split. generalize la (app_lt_cns a la (or_introl _ (eq_refl _))); clear la app_lt_cns; intros la la_lt_a; induction la as [ | b la]; trivial. simpl; generalize (R_bool_ok b a); case (R_bool b a); [intro b_R_a | intro not_b_R_a]; simpl. apply IHla; intros; apply la_lt_a; right; assumption. apply False_rect; apply not_b_R_a; apply la_lt_a; left; apply (equiv_refl _ _ eq_proof). rewrite (list_forall_impl (fun t1 : A => list_exists (fun t2 : A => R_bool t1 t2) (consn ll)) (fun t1 : A => Bool.ifb (R_bool t1 a) true (list_exists (fun t2 : A => R_bool t1 t2) (consn ll))) (appendn ll)). apply eq_refl. intros b b_in_all H; case (R_bool b a); simpl; [apply eq_refl | assumption]. apply IHll; intros b lb blb_in_ll; apply app_lt_cns; right; assumption. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)