proposition: Lemma Permutation_elt : forall l1 l2 l1' l2' (a:A), Permutation (l1 ++ l2) (l1' ++ l2') -> Permutation (l1 ++ a :: l2) (l1' ++ a :: l2').
proof: Proof. intros l1 l2 l1' l2' a HP. transitivity (a :: l1 ++ l2); auto. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat