proposition: Lemma removelast_firstn_len : forall l, removelast l = firstn (pred (length l)) l.
proof: Proof. intro l; induction l as [|a l IHl]; [ reflexivity | simpl ]. destruct l; [ | rewrite IHl ]; reflexivity. Qed.
imports: PeanoNat