proposition: Lemma removelast_app : forall l l', l' <> [] -> removelast (l++l') = l ++ removelast l'.
proof: Proof. intro l; induction l as [|? l IHl]; [easy|]. intros l' H. cbn. rewrite <- IHl by assumption. now destruct l, l'. Qed.
imports: PeanoNat