proposition: Lemma permut_rev : forall l, permutation l (rev l).
proof: Proof. induction l. - simpl; trivial using permut_refl. - simpl. apply permut_add_cons_inside. rewrite app_nil_r. trivial. Qed.
imports: Lia Relations Multiset SetoidList