proposition: Lemma Permutation_ind_transp : forall P : list A -> list A -> Prop, (forall l, P l l) -> (forall x y l1 l2, P (l1 ++ y :: x :: l2) (l1 ++ x :: y :: l2)) -> (forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') -> forall l1 l2, Permutation l1 l2 -> P l1 l2.
proof: Proof. intros P Hr Ht Htr l1 l2 HP; apply Permutation_Permutation_transp in HP. revert Hr Ht Htr; induction HP; intros Hr Ht Htr; auto. apply (Htr _ l'); intuition; now apply Permutation_Permutation_transp. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat