proposition: Fact incl_app_rinv l m p : incl m (l++p) -> exists m1 m2, m ~p m1++m2 /\ incl m1 l /\ incl m2 p.
proof: Proof. induction m as [ | x m IHm ]. + exists nil, nil; simpl; repeat split; auto; intros ? []. + intros H. apply incl_cons_linv in H. destruct H as (H1 & H2). destruct (IHm H2) as (m1 & m2 & H3 & H4 & H5). apply in_app_or in H1; destruct H1. * exists (x::m1), m2; repeat split; auto. - constructor 2; auto. - intros ? [|]; subst; auto. * exists m1, (x::m2); repeat split; auto. - apply Permutation_cons_app; auto. - intros ? [|]; subst; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)