proposition: Lemma firstn_le_length n: forall l:list A, length (firstn n l) <= n.
proof: Proof. induction n as [|k iHk]; simpl; [auto | intro l; destruct l as [|x xs]; simpl]. - now apply Nat.le_0_l. - now rewrite <- Nat.succ_le_mono. Qed.
imports: PeanoNat