proposition: Lemma remove_last_inv : forall (a:A) (l m:list A), remove_last a m l -> m = l ++ a :: nil.
proof: Proof. intros a l m H; elim H; simpl; auto with datatypes. intros b l0 m0 H0 e; rewrite e; trivial. Qed.
imports: List Arith Lia