proposition: Lemma permutation_transpose : forall (a b:Z) (l l':list Z), permutation l l' -> permutation (a :: b :: l) (b :: a :: l').
proof: Proof. intros a b l l' H z; simpl. case (Z.eq_dec z a); case (Z.eq_dec z b); simpl; case (H z); auto. Qed.
imports: List ZArith RelationClasses Morphisms Extraction