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