proposition: Lemma nth_in : forall (l : list A) i, nth_error l i <> None <-> i < length l.
proof: Proof. induction l; simpl; intro i. split. destruct i; intro; exfalso; auto. intro; lia. destruct i; simpl. split; intro. auto with arith. discr. split; intro. assert (i < length l). apply (proj1 (IHl i)); trivial. auto with arith. apply (proj2 (IHl i)); auto with arith. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)