proposition: Lemma permut_inv_right : forall (A : Type) (R : relation A) b l1 l2, permut0 R l1 (b :: l2) -> exists a, exists l1', exists l1'', (R a b /\ l1 = l1' ++ a :: l1'' /\ permut0 R (l1' ++ l1'') l2).
proof: Proof. intros A R b l1; generalize b; clear b; induction l1 as [ | a1 l1]; intros b l2 P; inversion P as [ | a b' l' l1' l2' a_R_b' Q H]; subst. destruct l1' as [ | a1' l1']; injection H1; clear H1; intros; subst. exists a1; exists (@nil A); exists l1; repeat split; trivial. simpl in Q; destruct (IHl1 _ _ Q) as [a [k1' [k1'' [a_R_b [H Q']]]]]; subst. exists a; exists (a1 :: k1'); exists k1''; repeat split; trivial. simpl; apply (@Pcons _ _ R a1 b' (k1' ++ k1'') l1' l2'); trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)