proposition: Lemma len_cons_not_O : forall (b : A) (v : list A) (l : nat), len (b :: v) l -> l <> 0.
proof: Proof. simple induction v. intros. inversion H. discriminate. intros. inversion H0. discriminate. Qed.
imports: List Arith_compl