proposition: Lemma nth_beyond : forall (l : list A) i, i >= length l -> nth_error l i = None.
proof: Proof. induction l; simpl; intro i. destruct i; trivial. destruct i; simpl. intros. lia. intro. rewrite (IHl i); trivial. auto with arith. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)