proposition: Theorem Permutation_app_comm : forall (l l' : list A), Permutation (l ++ l') (l' ++ l).
proof: Proof. induction l as [|x l]; simpl; intro l'. - rewrite app_nil_r; trivial. - rewrite IHl. rewrite app_comm_cons, Permutation_cons_append. now rewrite <- app_assoc. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat