proposition: Theorem Permutation_cons_app : forall (l l1 l2:list A) a, Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
proof: Proof. intros l l1 l2 a H. rewrite H. rewrite app_comm_cons, Permutation_cons_append. now rewrite <- app_assoc. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat