proposition: Lemma app_removelast_last : forall l d, l <> [] -> l = removelast l ++ [last l d].
proof: Proof. intro l; induction l as [|? l IHl]. - destruct 1; auto. - intros d _. destruct l as [|a0 l]; auto. pattern (a0::l) at 1; rewrite IHl with d; auto; discriminate. Qed.
imports: PeanoNat