proposition: Theorem firstn_le_length_eq : forall (n : nat) (l1 : list A), n <= length l1 -> length (firstn n l1) = n.
proof: Proof. intros n l1; generalize n; elim l1; clear n l1; simpl in |- *; auto. intros n; case n; simpl in |- *; auto. intros n1 H1; contradict H1; auto with arith. intros a l H n; case n; simpl in |- *; auto with arith. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)