proposition: Lemma PermutationA_cons_append l x : PermutationA (x :: l) (l ++ x :: nil).
proof: Proof. induction l. easy. simpl. rewrite <-IHl. intuition. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads