proposition: Lemma ls_last_exists : forall (A : Type)(ls : list A) n, length ls = (S n) -> exists a ls', (length ls' = n /\ ls = ls' ++ (a :: nil)).
proof: Proof. induction ls; intuition; simpl in *. lia. destruct n. destruct ls; simpl in *; try lia. exists a. exists nil. simpl. intuition. inversion H; clear H. edestruct IHls; intuition. eauto. destruct H. intuition. exists x. exists (a :: x0). subst. simpl. intuition. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation