proposition: Lemma length_pos_inv_last : forall l, (length l > 0%nat) -> exists x l', l = l' & x.
proof: Proof. Proof using. intros l. induction l; rew_list; introv H. { false. math. } { destruct l. { exists~ a (@nil A). } { destruct IHl as (x&l'&E). { rew_list in *. math. } { exists x (a::l'). rewrite~ E. } } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)