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