proposition: Lemma firstn_all2 n: forall (l:list A), (length l) <= n -> firstn n l = l.
proof: Proof. induction n as [|k iHk]. - intro l. inversion 1 as [H1|?]. rewrite (length_zero_iff_nil l) in H1. subst. now simpl. - intro l; destruct l as [|x xs]; simpl. * now reflexivity. * simpl. intro H. f_equal. apply iHk. now apply Nat.succ_le_mono. Qed.
imports: PeanoNat