proposition: Lemma Permutation_app_rot : forall l1 l2 l3: list A, Permutation (l1 ++ l2 ++ l3) (l2 ++ l3 ++ l1).
proof: Proof. intros l1 l2 l3; now rewrite (app_assoc l2). Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat