proposition: Lemma nth_error_none : forall A n (l : list A) , nth_error l n = None -> length l <= n.
proof: Proof. fix nth_error_none 3. intros A n [ | a l]; case n; clear n; simpl. intros _; apply le_n. intros; apply Nat.le_0_l. intros; discriminate. intros; apply le_n_S. apply nth_error_none. assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)