proposition: Theorem skipn_le_app2 : forall (n : nat) (l1 l2 : list A), n <= length l1 -> skipn n (l1 ++ l2) = skipn n l1 ++ l2.
proof: Proof. intros n; elim n; simpl in |- *; auto. intros n0 H l1; case l1; simpl in |- *; auto with arith. intros l2 H1; contradict H1; auto with arith. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)