proposition: Lemma PermutationA_middle l₁ l₂ x : PermutationA (x :: l₁ ++ l₂) (l₁ ++ x :: l₂).
proof: Proof. now apply PermutationA_cons_app. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads