proposition: Lemma firstn_length_le: forall l:list A, forall n:nat, n <= length l -> length (firstn n l) = n.
proof: Proof. intro l; induction l as [|x xs Hrec]. - simpl. intros n H. apply Nat.le_0_r in H. now subst. - intro n; destruct n as [|n]. * now simpl. * simpl. intro H. f_equal. apply Hrec. now apply Nat.succ_le_mono. Qed.
imports: PeanoNat