proposition: Lemma one_less2mult : forall r : relation A, (forall x x' y y', x =A=x' -> y=A=y' -> r x y -> r x' y') -> forall l l', one_less r l l' -> mult (transp r) l l'.
proof: Proof. intros r r_eqA_compat l l' H1; inversion H1; subst. generalize dependent l; induction p as [ | p]; intros l Hl H1. destruct l as [|h l];inversion H1. subst; simpl; simpl in H1. unfold mult, MultisetLT, transp; simpl. constructor 1 with (X := {{a'}}) (Y :={{a}}) (Z := (list2multiset l)); [auto with multisets|..]. unfold insert; simpl. rewrite union_comm; auto with multisets. unfold insert; simpl. rewrite union_comm; auto with multisets. intros y Hy; assert (HY : y =A= a). apply (member_singleton Hy). exists a'; auto with multisets. apply r_eqA_compat with a a'; auto with sets multisets. destruct l as [|h l]; inversion H1. subst; simpl. assert (Hml : mult (transp r) l (l [p := a'])). apply IHp; trivial. apply (@one_less_cons _ r l (l [p := a']) p a a'); trivial. apply mult_insert; trivial. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)