proposition: Lemma sub_transp_trans_2_mOrd_trans: forall P, (forall p, p in P -> forall x y, x >A p -> y >A x -> y >A p) -> forall M N, MultisetGT M N -> MultisetGT N P -> MultisetGT M P.
proof: Proof. intros P Hsub. destruct 1 as [X1 Y1 Z1 X1_ne M1_def N1_def Ord1]. destruct 1 as [X2 Y2 Z2 X2_ne N2_def P2_def Ord2]. constructor 1 with (union X1 (diff X2 Y1)) (union Y2 (diff Y1 X2)) (intersection Z1 Z2). auto with multisets. rewrite M1_def, (union_assoc (Z1#Z2) X1 (X2-Y1)), (union_perm (Z1#Z2) X1 (X2-Y1)). apply meq_meq_union. apply double_split. rewrite (union_comm Y1 Z1), (union_comm X2 Z2), <- N1_def, <- N2_def; auto with multisets. rewrite P2_def, (union_assoc (Z1#Z2) Y2 (Y1-X2)), (union_perm (Z1#Z2) Y2 (Y1-X2)). apply meq_meq_union. rewrite (intersection_comm Z1 Z2). apply double_split. rewrite (union_comm X2 Z2), (union_comm Y1 Z1), <- N1_def, <- N2_def; auto with multisets. intros y y_in_union; case (member_union y_in_union); intro y_in. destruct (Ord2 y y_in) as [x x_in_X2 x_gt_y]. case (member_dec x Y1); intro x_in_Y1. destruct (Ord1 x x_in_Y1) as [x' x'_in_X1 x'_gt_x]. exists x'. apply member_member_union; trivial. cut (y in P); [intro y_in_P | rewrite P2_def, (union_comm Z2 Y2); auto with multisets]. apply (Hsub y y_in_P x x'); trivial. exists x. rewrite (union_comm X1 (X2-Y1)); apply member_member_union. unfold member in *; rewrite (diff_mult X2 Y1); lia. trivial. destruct (Ord1 y). eauto with multisets. exists x. auto with multisets. trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)