proposition: Lemma length_pos_inv_cons : forall l, (length l > 0%nat) -> exists x l', l = x :: l'.
proof: Proof. Proof using. introv E. destruct l; rew_list in *. { false. math. } { eauto. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)