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