proposition: Lemma last_intro : forall l : list A, length l > 0 -> exists m, exists a, l = m ++ a :: nil /\ length m = length l - 1.
proof: Proof. induction l; simpl; intros. apply False_ind. lia. destruct l. exists nil. exists a. intuition. assert (length (a0::l) > 0). simpl. lia. ded (IHl H0). do 3 destruct H1. exists (a::x). exists x0. split. rewrite H1. refl. simpl. simpl in H2. lia. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)