proposition: Lemma insert_permutation : forall (l:list Z) (x:Z), permutation (x :: l) (insert x l).
proof: Proof. induction l as [|a l0 H]; simpl ; auto with sort. - intros x; case (Z_le_gt_dec x a); simpl; auto with sort. + intro H0; apply permutation_trans with (a :: x :: l0); auto with sort. Qed.
imports: List ZArith RelationClasses Morphisms Extraction