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