proposition: Theorem permutation_app_cons : forall (l:list A) (a:A) (l':list A), permutation (l ++ a :: l') (a :: l ++ l').
proof: Proof. intros l; elim l. simpl in |- *; intros; apply permutation_reflexive. simpl in |- *; intros a' tl Hrec a l'. apply permutation_transitive with (a' :: a :: tl ++ l'); constructor; auto. Qed.
imports: List Lia