proposition: Theorem cons_to_app_end : forall {A:Type} (l:list A) (a:A), exists b : A, exists l' : list A, a :: l = l' ++ b :: nil.
proof: Proof. intros A l a. rewrite <- (rev_involutive (a :: l)). assert (H : 0 < length (rev (a :: l))) by (rewrite <- length_rev; simpl ; auto with arith). destruct (rev (a :: l)) as [ | a0 l0]. - simpl ; elim (Nat.nlt_0_r 0); auto. - exists a0, (rev l0); simpl ; auto. Qed.
imports: List Arith