proposition: Lemma length_pos_inv_last : forall l, (length l > 0) -> exists x l', l = l' & x.
proof: Proof. Proof using. intros. unfolds length. applys~ LibList.length_pos_inv_last. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)