proposition: Lemma v_not_nil_length : forall v : list A, v <> nil -> 1 <= length v.
proof: Proof. simple induction v. intro. absurd (nil <> nil :>list A). unfold not in |- *. auto with arith. exact H. intros. simpl in |- *. apply le_n_S. auto with arith. Qed.
imports: List Arith_compl