proposition: Lemma PermutationA_cons_app l l₁ l₂ x : PermutationA l (l₁ ++ l₂) → PermutationA (x :: l) (l₁ ++ x :: l₂).
proof: Proof. intros E. rewrite E. now rewrite app_comm_cons, PermutationA_cons_append, <-app_assoc. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads